Fine-grained frame expressions for arrays

[RustanLeino]

Frames (modifies and reads clauses) in Dafny usually operate at the granularity of objects. For example,

modifies obj

says that the enclosing method is allowed to modify the state of object obj (that is, any field of obj may be modified). But Dafny also has syntax that allow the frame to be specific about which fields of an object can be modified/read. That syntax uses a back-tick:

`

For example,

modifies obj`f

says that the enclosing method is allowed to modify the f field of object obj.

Missing in the language is the ability to do the same with the elements of an array. I propose extending frame expressions to also allow the back-tick syntax for arrays in modifies/reads clauses. For example, for a 1-dimensional array reference arr and a 2-dimensional array reference m,

modifies arr`[5]  // element 5 of arr may be modified
modifies m`[20, 30]  // element 20,30 of m may be modified
modifies arr`[..n]  // the first n elements of arr may be modified
modifies arr`[k..]`  // any element of arr with index k or higher may be modified
modifies arr`[k..n]  // any element of arr with index from k to n may be modified

In other words, what follows the back-tick in square brackets are legal indices/ranges of arrays today.

With the proposed syntax, a method

method AssignRange<X>(arr: array<X>, lo: int, hi: int, x: X)
  requires 0 <= lo <= hi <= arr.Length
  modifies arr
  ensures forall i :: 0 <= i < lo ==> arr[i] == old(arr[i])
  ensures forall i :: lo <= i < hi ==> arr[i] == x
  ensures ofrall i :: hi <= i < arr.Length ==> arr[i] == old(arr[i])

can more straightforwardly be specified by

method AssignRange<X>(arr: array<X>, lo: int, hi: int, x: X)
  requires 0 <= lo <= hi <= arr.Length
  modifies arr`[lo..hi]
  ensures forall i :: lo <= i < hi ==> arr[i] == x