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 | 2b1732bf84b88b5656a305b781fdb818e5738ea6 (patch) | |
tree | 6ac9acb21b8276d9220c7d0c714375973754ef23 /Binaries | |
parent | 736bffc734c9c5d0245d6c483647b43add1ce13a (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 ---------------------------------------------------
// ---------------------------------------------------------------
|