title: Specifying modification of part of an array in Dafny
body: <p>I am writing a partition method in Dafny as part of a quicksort implementation, and I want to specify that this method only modifies part of the backing array.</p>
  
  <p>Here is the header for my method:</p>
  
  <pre><code>method partitionSegment (a : array&lt;int&gt;, first : int, len : int) returns (p : int)
    modifies a
  ...
  </code></pre>
  
  <p>The idea is that the first and len parameters specify a segment of array a (elements a[first] ... a[first+len-1]); partitionSegment partitions this array, returning the index of the pivot, which will be between first and first+len-1.</p>
  
  <p>In my modifies clause I would like to indicate that only a[first] ... a[first+len-1] can be modified, rather than all of a.  However, when I try using a set comprehension such as:</p>
  
  <pre><code>method partitionSegment (a : array&lt;int&gt;, first : int, len : int) returns (p : int)
  modifies (set x | first &lt;= x &lt; first+len :: a[x])
  </code></pre>
  
  <p>the type checker balks, saying this is a set of integers rather than a set of memory locations.  (So a[x] is being interpreted as the value stored at a[x], and not the memory location a[x].)</p>
  
  <p>Is there any way I can do this in dafny:  specify part of an array in a modifies annotation?</p>