diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 649 |
1 files changed, 0 insertions, 649 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl deleted file mode 100644 index 342b72c1..00000000 --- a/Binaries/DafnyPrelude.bpl +++ /dev/null @@ -1,649 +0,0 @@ -// Dafny prelude
-// Created 9 February 2008 by Rustan Leino.
-// Converted to Boogie 2 on 28 June 2008.
-// Edited sequence axioms 20 October 2009 by Alex Summers.
-// Copyright (c) 2008-2010, Microsoft.
-
-const $$Language$Dafny: bool; // To be recognizable to the ModelViewer as
-axiom $$Language$Dafny; // coming from a Dafny program.
-
-// ---------------------------------------------------------------
-// -- References -------------------------------------------------
-// ---------------------------------------------------------------
-
-type ref;
-const null: ref;
-
-// ---------------------------------------------------------------
-// -- Axiomatization of sets -------------------------------------
-// ---------------------------------------------------------------
-
-type Set T = [T]bool;
-
-function Set#Empty<T>(): Set T;
-axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
-
-function Set#Singleton<T>(T): Set T;
-axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
-axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
-
-function Set#UnionOne<T>(Set T, T): Set T;
-axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }
- Set#UnionOne(a,x)[o] <==> o == x || a[o]);
-axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }
- Set#UnionOne(a, x)[x]);
-axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }
- a[y] ==> Set#UnionOne(a, x)[y]);
-
-function Set#Union<T>(Set T, Set T): Set T;
-axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }
- Set#Union(a,b)[o] <==> a[o] || b[o]);
-axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), a[y] }
- a[y] ==> Set#Union(a, b)[y]);
-axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), b[y] }
- b[y] ==> Set#Union(a, b)[y]);
-axiom (forall<T> a, b: Set T :: { Set#Union(a, b) }
- Set#Disjoint(a, b) ==>
- Set#Difference(Set#Union(a, b), a) == b &&
- Set#Difference(Set#Union(a, b), b) == a);
-
-function Set#Intersection<T>(Set T, Set T): Set T;
-axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }
- Set#Intersection(a,b)[o] <==> a[o] && b[o]);
-
-axiom (forall<T> a, b: Set T :: { Set#Union(Set#Union(a, b), b) }
- Set#Union(Set#Union(a, b), b) == Set#Union(a, b));
-axiom (forall<T> a, b: Set T :: { Set#Union(a, Set#Union(a, b)) }
- Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));
-axiom (forall<T> a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) }
- Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));
-axiom (forall<T> a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }
- Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));
-
-function Set#Difference<T>(Set T, Set T): Set T;
-axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }
- Set#Difference(a,b)[o] <==> a[o] && !b[o]);
-axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }
- b[y] ==> !Set#Difference(a, b)[y] );
-
-function Set#Subset<T>(Set T, Set T): bool;
-axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }
- Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));
-
-function Set#Equal<T>(Set T, Set T): bool;
-axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }
- Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o]));
-axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) } // extensionality axiom for sets
- Set#Equal(a,b) ==> a == b);
-
-function Set#Disjoint<T>(Set T, Set T): bool;
-axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }
- Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));
-
-function Set#Choose<T>(Set T, TickType): T;
-axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
- a != Set#Empty() ==> a[Set#Choose(a, tick)]);
-
-
-// ---------------------------------------------------------------
-// -- Axiomatization of multisets --------------------------------
-// ---------------------------------------------------------------
-
-function Math#min(a: int, b: int): int;
-axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a);
-axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b);
-axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b);
-
-function Math#clip(a: int): int;
-axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a);
-axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0);
-
-type MultiSet T = [T]int;
-
-function $IsGoodMultiSet<T>(ms: MultiSet T): bool;
-// ints are non-negative, used after havocing, and for conversion from sequences to multisets.
-axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) }
- $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o]));
-
-function MultiSet#Empty<T>(): MultiSet T;
-axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
-
-function MultiSet#Singleton<T>(T): MultiSet T;
-axiom (forall<T> r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) &&
- (MultiSet#Singleton(r)[o] == 0 <==> r != o));
-axiom (forall<T> r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r));
-
-function MultiSet#UnionOne<T>(MultiSet T, T): MultiSet T;
-// pure containment axiom (in the original multiset or is the added element)
-axiom (forall<T> a: MultiSet T, x: T, o: T :: { MultiSet#UnionOne(a,x)[o] }
- 0 < MultiSet#UnionOne(a,x)[o] <==> o == x || 0 < a[o]);
-// union-ing increases count by one
-axiom (forall<T> a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) }
- MultiSet#UnionOne(a, x)[x] == a[x] + 1);
-// non-decreasing
-axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }
- 0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]);
-// other elements unchanged
-axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }
- x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);
-
-function MultiSet#Union<T>(MultiSet T, MultiSet T): MultiSet T;
-// union-ing is the sum of the contents
-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o] }
- MultiSet#Union(a,b)[o] == a[o] + b[o]);
-
-// two containment axioms
-axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] }
- 0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]);
-axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] }
- 0 < b[y] ==> 0 < MultiSet#Union(a, b)[y]);
-
-// symmetry axiom
-axiom (forall<T> a, b: MultiSet T :: { MultiSet#Union(a, b) }
- MultiSet#Difference(MultiSet#Union(a, b), a) == b &&
- MultiSet#Difference(MultiSet#Union(a, b), b) == a);
-
-function MultiSet#Intersection<T>(MultiSet T, MultiSet T): MultiSet T;
-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] }
- MultiSet#Intersection(a,b)[o] == Math#min(a[o], b[o]));
-
-// left and right pseudo-idempotence
-axiom (forall<T> a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) }
- MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b));
-axiom (forall<T> a, b: MultiSet T :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) }
- MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b));
-
-// multiset difference, a - b. clip() makes it positive.
-function MultiSet#Difference<T>(MultiSet T, MultiSet T): MultiSet T;
-axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Difference(a,b)[o] }
- MultiSet#Difference(a,b)[o] == Math#clip(a[o] - b[o]));
-axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), b[y], a[y] }
- a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0 );
-
-// multiset subset means a must have at most as many of each element as b
-function MultiSet#Subset<T>(MultiSet T, MultiSet T): bool;
-axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Subset(a,b) }
- MultiSet#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <= b[o]));
-
-function MultiSet#Equal<T>(MultiSet T, MultiSet T): bool;
-axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }
- MultiSet#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == b[o]));
-// extensionality axiom for multisets
-axiom(forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) }
- MultiSet#Equal(a,b) ==> a == b);
-
-function MultiSet#Disjoint<T>(MultiSet T, MultiSet T): bool;
-axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) }
- MultiSet#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] == 0 || b[o] == 0));
-
-// conversion to a multiset. each element in the original set has duplicity 1.
-function MultiSet#FromSet<T>(Set T): MultiSet T;
-axiom (forall<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] }
- (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) &&
- (MultiSet#FromSet(s)[a] == 1 <==> s[a]));
-
-// conversion to a multiset, from a sequence.
-function MultiSet#FromSeq<T>(Seq T): MultiSet T;
-// conversion produces a good map.
-axiom (forall<T> s: Seq T :: { MultiSet#FromSeq(s) } $IsGoodMultiSet(MultiSet#FromSeq(s)) );
-// building axiom
-axiom (forall<T> s: Seq T, v: T ::
- { MultiSet#FromSeq(Seq#Build(s, v)) }
- MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v)
- );
-axiom (forall<T> :: MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T);
-
-// concatenation axiom
-axiom (forall<T> a: Seq T, b: Seq T ::
- { MultiSet#FromSeq(Seq#Append(a, b)) }
- MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)) );
-
-// update axiom
-axiom (forall<T> s: Seq T, i: int, v: T, x: T ::
- { MultiSet#FromSeq(Seq#Update(s, i, v))[x] }
- 0 <= i && i < Seq#Length(s) ==>
- MultiSet#FromSeq(Seq#Update(s, i, v))[x] ==
- MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s,i))), MultiSet#Singleton(v))[x] );
- // i.e. MS(Update(s, i, v)) == MS(s) - {{s[i]}} + {{v}}
-axiom (forall<T> s: Seq T, x: T :: { MultiSet#FromSeq(s)[x] }
- (exists i : int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && x == Seq#Index(s,i)) <==> 0 < MultiSet#FromSeq(s)[x] );
-
-// ---------------------------------------------------------------
-// -- Axiomatization of sequences --------------------------------
-// ---------------------------------------------------------------
-
-type Seq T;
-
-function Seq#Length<T>(Seq T): int;
-axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
-
-function Seq#Empty<T>(): Seq T;
-axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
-axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
-
-function Seq#Singleton<T>(T): Seq T;
-axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
-
-function Seq#Build<T>(s: Seq T, val: T): Seq T;
-axiom (forall<T> s: Seq T, v: T :: { Seq#Length(Seq#Build(s,v)) }
- Seq#Length(Seq#Build(s,v)) == 1 + Seq#Length(s));
-axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Index(Seq#Build(s,v), i) }
- (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == v) &&
- (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == Seq#Index(s, i)));
-
-function Seq#Append<T>(Seq T, Seq T): Seq T;
-axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
- Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));
-
-function Seq#Index<T>(Seq T, int): T;
-axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);
-axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }
- (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&
- (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
-
-function Seq#Update<T>(Seq T, int, T): Seq T;
-axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) }
- 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s));
-axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) }
- 0 <= n && n < Seq#Length(s) ==>
- (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) &&
- (i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n)));
-
-function Seq#Contains<T>(Seq T, T): bool;
-axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
- Seq#Contains(s,x) <==>
- (exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
-axiom (forall x: ref ::
- { Seq#Contains(Seq#Empty(), x) }
- !Seq#Contains(Seq#Empty(), x));
-axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
- { Seq#Contains(Seq#Append(s0, s1), x) }
- Seq#Contains(Seq#Append(s0, s1), x) <==>
- Seq#Contains(s0, x) || Seq#Contains(s1, x));
-
-axiom (forall<T> s: Seq T, v: T, x: T ::
- { Seq#Contains(Seq#Build(s, v), x) }
- Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x)));
-
-axiom (forall<T> s: Seq T, n: int, x: T ::
- { Seq#Contains(Seq#Take(s, n), x) }
- Seq#Contains(Seq#Take(s, n), x) <==>
- (exists i: int :: { Seq#Index(s, i) }
- 0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x));
-axiom (forall<T> s: Seq T, n: int, x: T ::
- { Seq#Contains(Seq#Drop(s, n), x) }
- Seq#Contains(Seq#Drop(s, n), x) <==>
- (exists i: int :: { Seq#Index(s, i) }
- 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
-
-function Seq#Equal<T>(Seq T, Seq T): bool;
-axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
- Seq#Equal(s0,s1) <==>
- Seq#Length(s0) == Seq#Length(s1) &&
- (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
- 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
-axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences
- Seq#Equal(a,b) ==> a == b);
-
-function Seq#SameUntil<T>(Seq T, Seq T, int): bool;
-axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }
- Seq#SameUntil(s0,s1,n) <==>
- (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
- 0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
-
-function Seq#Take<T>(s: Seq T, howMany: int): Seq T;
-axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
- 0 <= n ==>
- (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
- (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));
-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}
- 0 <= j && j < n && j < Seq#Length(s) ==>
- Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
-
-function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;
-axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
- 0 <= n ==>
- (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
- (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));
-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}
- 0 <= n && 0 <= j && j < Seq#Length(s)-n ==>
- Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));
-
-axiom (forall<T> s, t: Seq T ::
- { Seq#Append(s, t) }
- Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&
- Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);
-
-function Seq#FromArray(h: HeapType, a: ref): Seq BoxType;
-axiom (forall h: HeapType, a: ref ::
- { Seq#Length(Seq#FromArray(h,a)) }
- Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
-axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType }
- (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
-axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::
- { Seq#FromArray(update(h, o, f, v), a) }
- o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) );
-axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::
- { Seq#FromArray(update(h, a, IndexField(i), v), a) }
- 0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );
-/**** Someday:
-axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) }
- $IsGoodHeap(h) &&
- a != null && read(h, a, alloc) && dtype(a) == class._System.array && TypeParams(a, 0) == class._System.bool
- ==>
- (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) }
- 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i))));
-****/
-
-// Commutability of Take and Drop with Update.
-axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
- { Seq#Take(Seq#Update(s, i, v), n) }
- 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );
-axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
- { Seq#Take(Seq#Update(s, i, v), n) }
- n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));
-axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
- { Seq#Drop(Seq#Update(s, i, v), n) }
- 0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) );
-axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
- { Seq#Drop(Seq#Update(s, i, v), n) }
- 0 <= i && i < n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));
-// Extension axiom, triggers only on Takes from arrays.
-axiom (forall h: HeapType, a: ref, n0, n1: int ::
- { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) }
- n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) );
-// drop commutes with build.
-axiom (forall<T> s: Seq T, v: T, n: int ::
- { Seq#Drop(Seq#Build(s, v), n) }
- 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );
-
-// Additional axioms about common things
-axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][..0] == []
-axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][0..] == []
-
-// ---------------------------------------------------------------
-// -- Axiomatization of Maps -------------------------------------
-// ---------------------------------------------------------------
-
-type Map U V;
-
-function Map#Domain<U, V>(Map U V): [U] bool;
-function Map#Elements<U, V>(Map U V): [U]V;
-
-function Map#Empty<U, V>(): Map U V;
-axiom (forall<U, V> u: U ::
- { Map#Domain(Map#Empty(): Map U V)[u] }
- !Map#Domain(Map#Empty(): Map U V)[u]);
-
-function Map#Glue<U, V>([U] bool, [U]V): Map U V;
-axiom (forall<U, V> a: [U] bool, b:[U]V ::
- { Map#Domain(Map#Glue(a, b)) }
- Map#Domain(Map#Glue(a, b)) == a);
-axiom (forall<U, V> a: [U] bool, b:[U]V ::
- { Map#Elements(Map#Glue(a, b)) }
- Map#Elements(Map#Glue(a, b)) == b);
-
-
-//Build is used in displays, and for map updates
-function Map#Build<U, V>(Map U V, U, V): Map U V;
-/*axiom (forall<U, V> m: Map U V, u: U, v: V ::
- { Map#Domain(Map#Build(m, u, v))[u] } { Map#Elements(Map#Build(m, u, v))[u] }
- Map#Domain(Map#Build(m, u, v))[u] && Map#Elements(Map#Build(m, u, v))[u] == v);*/
-
-axiom (forall<U, V> m: Map U V, u: U, u': U, v: V ::
- { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Elements(Map#Build(m, u, v))[u'] }
- (u' == u ==> Map#Domain(Map#Build(m, u, v))[u'] &&
- Map#Elements(Map#Build(m, u, v))[u'] == v) &&
- (u' != u ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] &&
- Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u']));
-
-//equality for maps
-function Map#Equal<U, V>(Map U V, Map U V): bool;
-axiom (forall<U, V> m: Map U V, m': Map U V::
- { Map#Equal(m, m') }
- Map#Equal(m, m') <==> (forall u : U :: Map#Domain(m)[u] == Map#Domain(m')[u]) &&
- (forall u : U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]));
-// extensionality
-axiom (forall<U, V> m: Map U V, m': Map U V::
- { Map#Equal(m, m') }
- Map#Equal(m, m') ==> m == m');
-
-function Map#Disjoint<U, V>(Map U V, Map U V): bool;
-axiom (forall<U, V> m: Map U V, m': Map U V ::
- { Map#Disjoint(m, m') }
- Map#Disjoint(m, m') <==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o]));
-
-// ---------------------------------------------------------------
-// -- Boxing and unboxing ----------------------------------------
-// ---------------------------------------------------------------
-
-type BoxType;
-
-function $Box<T>(T): BoxType;
-function $Unbox<T>(BoxType): T;
-
-axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
-axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);
-axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
-axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
-axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);
-axiom (forall b: BoxType :: { $Unbox(b): Map BoxType BoxType } $Box($Unbox(b): Map BoxType BoxType) == b);
-axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b);
-// Note: an axiom like this for bool would not be sound; instead, we do:
-function $IsCanonicalBoolBox(BoxType): bool;
-axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));
-axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);
-
-// ---------------------------------------------------------------
-// -- Encoding of type names -------------------------------------
-// ---------------------------------------------------------------
-
-type ClassName;
-const unique class._System.int: ClassName;
-const unique class._System.bool: ClassName;
-const unique class._System.set: ClassName;
-const unique class._System.seq: ClassName;
-const unique class._System.multiset: ClassName;
-const unique class._System.array: ClassName;
-
-function /*{:never_pattern true}*/ dtype(ref): ClassName;
-function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;
-
-function TypeTuple(a: ClassName, b: ClassName): ClassName;
-function TypeTupleCar(ClassName): ClassName;
-function TypeTupleCdr(ClassName): ClassName;
-// TypeTuple is injective in both arguments:
-axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
- TypeTupleCar(TypeTuple(a,b)) == a &&
- TypeTupleCdr(TypeTuple(a,b)) == b);
-
-// ---------------------------------------------------------------
-// -- Datatypes --------------------------------------------------
-// ---------------------------------------------------------------
-
-type DatatypeType;
-
-function /*{:never_pattern true}*/ DtType(DatatypeType): ClassName; // the analog of dtype for datatype values
-function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName; // the analog of TypeParams
-
-type DtCtorId;
-function DatatypeCtorId(DatatypeType): DtCtorId;
-
-function DtRank(DatatypeType): int;
-
-// ---------------------------------------------------------------
-// -- Axiom contexts ---------------------------------------------
-// ---------------------------------------------------------------
-
-// used to make sure function axioms are not used while their consistency is being checked
-const $ModuleContextHeight: int;
-const $FunctionContextHeight: int;
-const $InMethodContext: bool;
-
-// ---------------------------------------------------------------
-// -- Fields -----------------------------------------------------
-// ---------------------------------------------------------------
-
-type Field alpha;
-
-function FDim<T>(Field T): int;
-
-function IndexField(int): Field BoxType;
-axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);
-function IndexField_Inverse<T>(Field T): int;
-axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);
-
-function MultiIndexField(Field BoxType, int): Field BoxType;
-axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } FDim(MultiIndexField(f,i)) == FDim(f) + 1);
-function MultiIndexField_Inverse0<T>(Field T): Field T;
-function MultiIndexField_Inverse1<T>(Field T): int;
-axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }
- MultiIndexField_Inverse0(MultiIndexField(f,i)) == f &&
- MultiIndexField_Inverse1(MultiIndexField(f,i)) == i);
-
-
-function DeclType<T>(Field T): ClassName;
-
-type NameFamily;
-function DeclName<T>(Field T): NameFamily;
-function FieldOfDecl<alpha>(ClassName, NameFamily): Field alpha;
-axiom (forall<T> cl : ClassName, nm: NameFamily ::
- {FieldOfDecl(cl, nm): Field T}
- DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm);
-
-// ---------------------------------------------------------------
-// -- Allocatedness ----------------------------------------------
-// ---------------------------------------------------------------
-
-const unique alloc: Field bool;
-axiom FDim(alloc) == 0;
-
-function DtAlloc(DatatypeType, HeapType): bool;
-axiom (forall h, k: HeapType, d: DatatypeType ::
- { $HeapSucc(h, k), DtAlloc(d, h) }
- { $HeapSucc(h, k), DtAlloc(d, k) }
- $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k));
-
-function GenericAlloc(BoxType, HeapType): bool;
-axiom (forall h: HeapType, k: HeapType, d: BoxType ::
- { $HeapSucc(h, k), GenericAlloc(d, h) }
- { $HeapSucc(h, k), GenericAlloc(d, k) }
- $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k));
-// GenericAlloc ==>
-axiom (forall b: BoxType, h: HeapType ::
- { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] }
- GenericAlloc(b, h) ==>
- $Unbox(b): ref == null || h[$Unbox(b): ref, alloc]);
-//seqs
-axiom (forall b: BoxType, h: HeapType, i: int ::
- { GenericAlloc(b, h), Seq#Index($Unbox(b): Seq BoxType, i) }
- GenericAlloc(b, h) &&
- 0 <= i && i < Seq#Length($Unbox(b): Seq BoxType) ==>
- GenericAlloc( Seq#Index($Unbox(b): Seq BoxType, i), h ) );
-
-//maps
-//seq-like axiom, talking about the range elements
-axiom (forall b: BoxType, h: HeapType, i: BoxType ::
- { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[i] }
- GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[i] ==>
- GenericAlloc( Map#Elements($Unbox(b): Map BoxType BoxType)[i], h ) );
-//set-like axiom, talking about the domain elements
-axiom (forall b: BoxType, h: HeapType, t: BoxType ::
- { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[t] }
- GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[t] ==>
- GenericAlloc(t, h));
-
-//sets
-axiom (forall b: BoxType, h: HeapType, t: BoxType ::
- { GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] }
- GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==>
- GenericAlloc(t, h));
-axiom (forall b: BoxType, h: HeapType ::
- { GenericAlloc(b, h), DtType($Unbox(b): DatatypeType) }
- GenericAlloc(b, h) ==> DtAlloc($Unbox(b): DatatypeType, h));
-// ==> GenericAlloc
-axiom (forall b: bool, h: HeapType ::
- $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));
-axiom (forall x: int, h: HeapType ::
- $IsGoodHeap(h) ==> GenericAlloc($Box(x), h));
-axiom (forall r: ref, h: HeapType ::
- { GenericAlloc($Box(r), h) }
- $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));
-// boxes in the heap
-axiom (forall r: ref, f: Field BoxType, h: HeapType ::
- { GenericAlloc(read(h, r, f), h) }
- $IsGoodHeap(h) && r != null && read(h, r, alloc) ==>
- GenericAlloc(read(h, r, f), h));
-
-// ---------------------------------------------------------------
-// -- Arrays -----------------------------------------------------
-// ---------------------------------------------------------------
-
-function _System.array.Length(a: ref): int;
-axiom (forall o: ref :: 0 <= _System.array.Length(o));
-
-// ---------------------------------------------------------------
-// -- The heap ---------------------------------------------------
-// ---------------------------------------------------------------
-
-type HeapType = <alpha>[ref,Field alpha]alpha;
-function {:inline true} read<alpha>(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] }
-function {:inline true} update<alpha>(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] }
-
-function $IsGoodHeap(HeapType): bool;
-var $Heap: HeapType where $IsGoodHeap($Heap);
-
-function $HeapSucc(HeapType, HeapType): bool;
-axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }
- $IsGoodHeap(update(h, r, f, x)) ==>
- $HeapSucc(h, update(h, r, f, x)));
-axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }
- $HeapSucc(a,b) && $HeapSucc(b,c) ==> $HeapSucc(a,c));
-axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
- $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
-
-// ---------------------------------------------------------------
-// -- Useful macros ----------------------------------------------
-// ---------------------------------------------------------------
-
-// havoc everything in $Heap, except {this}+rds+nw
-procedure $YieldHavoc(this: ref, rds: Set BoxType, nw: Set BoxType);
- modifies $Heap;
- ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
- $o != null && read(old($Heap), $o, alloc) ==>
- $o == this || rds[$Box($o)] || nw[$Box($o)] ==>
- read($Heap, $o, $f) == read(old($Heap), $o, $f));
- ensures $HeapSucc(old($Heap), $Heap);
-
-// havoc everything in $Heap, except rds-modi-{this}
-procedure $IterHavoc0(this: ref, rds: Set BoxType, modi: Set BoxType);
- modifies $Heap;
- ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
- $o != null && read(old($Heap), $o, alloc) ==>
- rds[$Box($o)] && !modi[$Box($o)] && $o != this ==>
- read($Heap, $o, $f) == read(old($Heap), $o, $f));
- ensures $HeapSucc(old($Heap), $Heap);
-
-// havoc $Heap at {this}+modi+nw
-procedure $IterHavoc1(this: ref, modi: Set BoxType, nw: Set BoxType);
- modifies $Heap;
- ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
- $o != null && read(old($Heap), $o, alloc) ==>
- read($Heap, $o, $f) == read(old($Heap), $o, $f) ||
- $o == this || modi[$Box($o)] || nw[$Box($o)]);
- ensures $HeapSucc(old($Heap), $Heap);
-
-procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType))
- returns (s: Set BoxType);
- ensures (forall bx: BoxType :: { s[bx] } s[bx] <==>
- read(newHeap, this, NW)[bx] ||
- ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc)));
-
-// ---------------------------------------------------------------
-// -- Non-determinism --------------------------------------------
-// ---------------------------------------------------------------
-
-type TickType;
-var $Tick: TickType;
-
-// ---------------------------------------------------------------
|