diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-26 20:55:53 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-26 20:55:53 -0700 |
| commit | f5b9f70c1da3279581cd910ce56a3d840e151f14 (patch) | |
| tree | 727ca2ea32bf1abc43fb66df224f455811a6278a /Binaries | |
| parent | 0554f4e6085f63f5d171abae76a0010fb177a4b5 (diff) | |
Dafny: removed support for assigning to an array-range (that is, an assignment statement where the LHS has the form a[lo..hi])
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 32430fd3..1fe21204 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -489,13 +489,6 @@ axiom (forall r: ref, h: HeapType :: function array.Length(a: ref): int;
axiom (forall o: ref :: 0 <= array.Length(o));
-procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType);
- modifies $Heap;
- ensures $HeapSucc(old($Heap), $Heap);
- ensures (forall i: int :: { read($Heap, arr, IndexField(i)) } low <= i && i < high ==> read($Heap, arr, IndexField(i)) == rhs);
- ensures (forall<alpha> o: ref, f: Field alpha :: { read($Heap, o, f) } read($Heap, o, f) == read(old($Heap), o, f) ||
- (o == arr && FDim(f) == 1 && low <= IndexField_Inverse(f) && IndexField_Inverse(f) < high));
-
// ---------------------------------------------------------------
// -- The heap ---------------------------------------------------
// ---------------------------------------------------------------
|