summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2016-02-26 11:06:11 -0800
committerGravatar qunyanm <unknown>2016-02-26 11:06:11 -0800
commit62f42e257fd72498e692c7ce8aaee339ad5322e6 (patch)
tree98eb7f38ccc09ec701b15dc81d36c0508f072ce0 /Test
parent273a5368fb5b7e919011c3774317c302d1bad87d (diff)
Fix test failure. Print the resulting boogie code to a file instead
of console.
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny4/Bug136.dfy2
-rw-r--r--Test/dafny4/Bug136.dfy.expect1770
2 files changed, 1 insertions, 1771 deletions
diff --git a/Test/dafny4/Bug136.dfy b/Test/dafny4/Bug136.dfy
index 5f3cde69..97c9e389 100644
--- a/Test/dafny4/Bug136.dfy
+++ b/Test/dafny4/Bug136.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:- "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method test()
diff --git a/Test/dafny4/Bug136.dfy.expect b/Test/dafny4/Bug136.dfy.expect
index 8b9d32a8..069e7767 100644
--- a/Test/dafny4/Bug136.dfy.expect
+++ b/Test/dafny4/Bug136.dfy.expect
@@ -1,1772 +1,2 @@
-// Dafny program verifier version 1.9.6.21116, Copyright (c) 2003-2015, Microsoft.
-// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /compile:0 /print:- c:\dafny\Test\dafny4\Bug136.dfy
-
-const $$Language$Dafny: bool;
-
-axiom $$Language$Dafny;
-
-type Ty;
-
-const unique TBool: Ty;
-
-const unique TChar: Ty;
-
-const unique TInt: Ty;
-
-const unique TNat: Ty;
-
-const unique TReal: Ty;
-
-function TSet(Ty) : Ty;
-
-function TISet(Ty) : Ty;
-
-function TMultiSet(Ty) : Ty;
-
-function TSeq(Ty) : Ty;
-
-function TMap(Ty, Ty) : Ty;
-
-function TIMap(Ty, Ty) : Ty;
-
-function Inv0_TSet(Ty) : Ty;
-
-axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t);
-
-function Inv0_TISet(Ty) : Ty;
-
-axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t);
-
-function Inv0_TSeq(Ty) : Ty;
-
-axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t);
-
-function Inv0_TMultiSet(Ty) : Ty;
-
-axiom (forall t: Ty :: { TMultiSet(t) } Inv0_TMultiSet(TMultiSet(t)) == t);
-
-function Inv0_TMap(Ty) : Ty;
-
-function Inv1_TMap(Ty) : Ty;
-
-axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv0_TMap(TMap(t, u)) == t);
-
-axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv1_TMap(TMap(t, u)) == u);
-
-function Inv0_TIMap(Ty) : Ty;
-
-function Inv1_TIMap(Ty) : Ty;
-
-axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv0_TIMap(TIMap(t, u)) == t);
-
-axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv1_TIMap(TIMap(t, u)) == u);
-
-type TyTag;
-
-function Tag(Ty) : TyTag;
-
-const unique TagBool: TyTag;
-
-const unique TagChar: TyTag;
-
-const unique TagInt: TyTag;
-
-const unique TagNat: TyTag;
-
-const unique TagReal: TyTag;
-
-const unique TagSet: TyTag;
-
-const unique TagISet: TyTag;
-
-const unique TagMultiSet: TyTag;
-
-const unique TagSeq: TyTag;
-
-const unique TagMap: TyTag;
-
-const unique TagIMap: TyTag;
-
-const unique TagClass: TyTag;
-
-axiom Tag(TBool) == TagBool;
-
-axiom Tag(TChar) == TagChar;
-
-axiom Tag(TInt) == TagInt;
-
-axiom Tag(TNat) == TagNat;
-
-axiom Tag(TReal) == TagReal;
-
-axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet);
-
-axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet);
-
-axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet);
-
-axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq);
-
-axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Tag(TMap(t, u)) == TagMap);
-
-axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Tag(TIMap(t, u)) == TagIMap);
-
-function {:identity} LitInt(x: int) : int;
-
-axiom (forall x: int :: {:identity} { LitInt(x): int } LitInt(x): int == x);
-
-axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)));
-
-function {:identity} LitReal(x: real) : real;
-
-axiom (forall x: real :: {:identity} { LitReal(x): real } LitReal(x): real == x);
-
-axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)));
-
-function {:identity} Lit<T>(x: T) : T;
-
-axiom (forall<T> x: T :: {:identity} { Lit(x): T } Lit(x): T == x);
-
-axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)));
-
-type char;
-
-function char#FromInt(int) : char;
-
-function char#ToInt(char) : int;
-
-axiom (forall ch: char :: { char#ToInt(ch) } char#FromInt(char#ToInt(ch)) == ch);
-
-axiom (forall n: int ::
- { char#FromInt(n) }
- 0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n);
-
-type ref;
-
-const null: ref;
-
-const unique NoTraitAtAll: ClassName;
-
-function TraitParent(ClassName) : ClassName;
-
-type Box;
-
-const $ArbitraryBoxValue: Box;
-
-function $Box<T>(T) : Box;
-
-function $Unbox<T>(Box) : T;
-
-axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
-
-axiom (forall bx: Box ::
- { $IsBox(bx, TInt) }
- $IsBox(bx, TInt) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TInt));
-
-axiom (forall bx: Box ::
- { $IsBox(bx, TNat) }
- $IsBox(bx, TNat) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TNat));
-
-axiom (forall bx: Box ::
- { $IsBox(bx, TReal) }
- $IsBox(bx, TReal)
- ==> $Box($Unbox(bx): real) == bx && $Is($Unbox(bx): real, TReal));
-
-axiom (forall bx: Box ::
- { $IsBox(bx, TBool) }
- $IsBox(bx, TBool)
- ==> $Box($Unbox(bx): bool) == bx && $Is($Unbox(bx): bool, TBool));
-
-axiom (forall bx: Box ::
- { $IsBox(bx, TChar) }
- $IsBox(bx, TChar)
- ==> $Box($Unbox(bx): char) == bx && $Is($Unbox(bx): char, TChar));
-
-axiom (forall bx: Box, t: Ty ::
- { $IsBox(bx, TSet(t)) }
- $IsBox(bx, TSet(t))
- ==> $Box($Unbox(bx): Set Box) == bx && $Is($Unbox(bx): Set Box, TSet(t)));
-
-axiom (forall bx: Box, t: Ty ::
- { $IsBox(bx, TISet(t)) }
- $IsBox(bx, TISet(t))
- ==> $Box($Unbox(bx): ISet Box) == bx && $Is($Unbox(bx): ISet Box, TISet(t)));
-
-axiom (forall bx: Box, t: Ty ::
- { $IsBox(bx, TMultiSet(t)) }
- $IsBox(bx, TMultiSet(t))
- ==> $Box($Unbox(bx): MultiSet Box) == bx
- && $Is($Unbox(bx): MultiSet Box, TMultiSet(t)));
-
-axiom (forall bx: Box, t: Ty ::
- { $IsBox(bx, TSeq(t)) }
- $IsBox(bx, TSeq(t))
- ==> $Box($Unbox(bx): Seq Box) == bx && $Is($Unbox(bx): Seq Box, TSeq(t)));
-
-axiom (forall bx: Box, s: Ty, t: Ty ::
- { $IsBox(bx, TMap(s, t)) }
- $IsBox(bx, TMap(s, t))
- ==> $Box($Unbox(bx): Map Box Box) == bx && $Is($Unbox(bx): Map Box Box, TMap(s, t)));
-
-axiom (forall bx: Box, s: Ty, t: Ty ::
- { $IsBox(bx, TIMap(s, t)) }
- $IsBox(bx, TIMap(s, t))
- ==> $Box($Unbox(bx): IMap Box Box) == bx
- && $Is($Unbox(bx): IMap Box Box, TIMap(s, t)));
-
-axiom (forall<T> v: T, t: Ty ::
- { $IsBox($Box(v), t) }
- $IsBox($Box(v), t) <==> $Is(v, t));
-
-axiom (forall<T> v: T, t: Ty, h: Heap ::
- { $IsAllocBox($Box(v), t, h) }
- $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v, t, h));
-
-function $Is<T>(T, Ty) : bool;
-
-function $IsAlloc<T>(T, Ty, Heap) : bool;
-
-function $IsBox<T>(T, Ty) : bool;
-
-function $IsAllocBox<T>(T, Ty, Heap) : bool;
-
-axiom (forall v: int :: { $Is(v, TInt) } $Is(v, TInt));
-
-axiom (forall v: int :: { $Is(v, TNat) } $Is(v, TNat) <==> v >= 0);
-
-axiom (forall v: real :: { $Is(v, TReal) } $Is(v, TReal));
-
-axiom (forall v: bool :: { $Is(v, TBool) } $Is(v, TBool));
-
-axiom (forall v: char :: { $Is(v, TChar) } $Is(v, TChar));
-
-axiom (forall h: Heap, v: int :: { $IsAlloc(v, TInt, h) } $IsAlloc(v, TInt, h));
-
-axiom (forall h: Heap, v: int :: { $IsAlloc(v, TNat, h) } $IsAlloc(v, TNat, h));
-
-axiom (forall h: Heap, v: real :: { $IsAlloc(v, TReal, h) } $IsAlloc(v, TReal, h));
-
-axiom (forall h: Heap, v: bool :: { $IsAlloc(v, TBool, h) } $IsAlloc(v, TBool, h));
-
-axiom (forall h: Heap, v: char :: { $IsAlloc(v, TChar, h) } $IsAlloc(v, TChar, h));
-
-axiom (forall v: Set Box, t0: Ty ::
- { $Is(v, TSet(t0)) }
- $Is(v, TSet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0)));
-
-axiom (forall v: ISet Box, t0: Ty ::
- { $Is(v, TISet(t0)) }
- $Is(v, TISet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0)));
-
-axiom (forall v: MultiSet Box, t0: Ty ::
- { $Is(v, TMultiSet(t0)) }
- $Is(v, TMultiSet(t0))
- <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsBox(bx, t0)));
-
-axiom (forall v: MultiSet Box, t0: Ty ::
- { $Is(v, TMultiSet(t0)) }
- $Is(v, TMultiSet(t0)) ==> $IsGoodMultiSet(v));
-
-axiom (forall v: Seq Box, t0: Ty ::
- { $Is(v, TSeq(t0)) }
- $Is(v, TSeq(t0))
- <==> (forall i: int ::
- { Seq#Index(v, i) }
- 0 <= i && i < Seq#Length(v) ==> $IsBox(Seq#Index(v, i), t0)));
-
-axiom (forall v: Set Box, t0: Ty, h: Heap ::
- { $IsAlloc(v, TSet(t0), h) }
- $IsAlloc(v, TSet(t0), h)
- <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h)));
-
-axiom (forall v: ISet Box, t0: Ty, h: Heap ::
- { $IsAlloc(v, TISet(t0), h) }
- $IsAlloc(v, TISet(t0), h)
- <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h)));
-
-axiom (forall v: MultiSet Box, t0: Ty, h: Heap ::
- { $IsAlloc(v, TMultiSet(t0), h) }
- $IsAlloc(v, TMultiSet(t0), h)
- <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsAllocBox(bx, t0, h)));
-
-axiom (forall v: Seq Box, t0: Ty, h: Heap ::
- { $IsAlloc(v, TSeq(t0), h) }
- $IsAlloc(v, TSeq(t0), h)
- <==> (forall i: int ::
- { Seq#Index(v, i) }
- 0 <= i && i < Seq#Length(v) ==> $IsAllocBox(Seq#Index(v, i), t0, h)));
-
-axiom (forall v: Map Box Box, t0: Ty, t1: Ty ::
- { $Is(v, TMap(t0, t1)) }
- $Is(v, TMap(t0, t1))
- <==> (forall bx: Box ::
- { Map#Elements(v)[bx] } { Map#Domain(v)[bx] }
- Map#Domain(v)[bx] ==> $IsBox(Map#Elements(v)[bx], t1) && $IsBox(bx, t0)));
-
-axiom (forall v: Map Box Box, t0: Ty, t1: Ty, h: Heap ::
- { $IsAlloc(v, TMap(t0, t1), h) }
- $IsAlloc(v, TMap(t0, t1), h)
- <==> (forall bx: Box ::
- { Map#Elements(v)[bx] } { Map#Domain(v)[bx] }
- Map#Domain(v)[bx]
- ==> $IsAllocBox(Map#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h)));
-
-axiom (forall v: IMap Box Box, t0: Ty, t1: Ty ::
- { $Is(v, TIMap(t0, t1)) }
- $Is(v, TIMap(t0, t1))
- <==> (forall bx: Box ::
- { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }
- IMap#Domain(v)[bx] ==> $IsBox(IMap#Elements(v)[bx], t1) && $IsBox(bx, t0)));
-
-axiom (forall v: IMap Box Box, t0: Ty, t1: Ty, h: Heap ::
- { $IsAlloc(v, TIMap(t0, t1), h) }
- $IsAlloc(v, TIMap(t0, t1), h)
- <==> (forall bx: Box ::
- { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] }
- IMap#Domain(v)[bx]
- ==> $IsAllocBox(IMap#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h)));
-
-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;
-
-function Tclass._System.object() : Ty;
-
-function dtype(ref) : Ty;
-
-function TypeTuple(a: ClassName, b: ClassName) : ClassName;
-
-function TypeTupleCar(ClassName) : ClassName;
-
-function TypeTupleCdr(ClassName) : ClassName;
-
-axiom (forall a: ClassName, b: ClassName ::
- { TypeTuple(a, b) }
- TypeTupleCar(TypeTuple(a, b)) == a && TypeTupleCdr(TypeTuple(a, b)) == b);
-
-type HandleType;
-
-function SetRef_to_SetBox(s: [ref]bool) : Set Box;
-
-axiom (forall s: [ref]bool, bx: Box ::
- { SetRef_to_SetBox(s)[bx] }
- SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]);
-
-axiom (forall s: [ref]bool ::
- { SetRef_to_SetBox(s) }
- $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object())));
-
-type DatatypeType;
-
-type DtCtorId;
-
-function DatatypeCtorId(DatatypeType) : DtCtorId;
-
-function DtRank(DatatypeType) : int;
-
-function BoxRank(Box) : int;
-
-axiom (forall d: DatatypeType :: { BoxRank($Box(d)) } BoxRank($Box(d)) == DtRank(d));
-
-const $ModuleContextHeight: int;
-
-const $FunctionContextHeight: int;
-
-type LayerType;
-
-const $LZ: LayerType;
-
-function $LS(LayerType) : LayerType;
-
-function AtLayer<A>([LayerType]A, LayerType) : A;
-
-axiom (forall<A> f: [LayerType]A, ly: LayerType ::
- { AtLayer(f, ly) }
- AtLayer(f, ly) == f[ly]);
-
-axiom (forall<A> f: [LayerType]A, ly: LayerType ::
- { AtLayer(f, $LS(ly)) }
- AtLayer(f, $LS(ly)) == AtLayer(f, ly));
-
-type Field _;
-
-function FDim<T>(Field T) : int;
-
-function IndexField(int) : Field Box;
-
-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 Box, int) : Field Box;
-
-axiom (forall f: Field Box, 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 Box, 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);
-
-function $IsGhostField<T>(Field T) : bool;
-
-axiom (forall<T> h: Heap, k: Heap, v: T, t: Ty ::
- { $HeapSucc(h, k), $IsAlloc(v, t, h) }
- $HeapSucc(h, k) ==> $IsAlloc(v, t, h) ==> $IsAlloc(v, t, k));
-
-axiom (forall h: Heap, k: Heap, bx: Box, t: Ty ::
- { $HeapSucc(h, k), $IsAllocBox(bx, t, h) }
- $HeapSucc(h, k) ==> $IsAllocBox(bx, t, h) ==> $IsAllocBox(bx, t, k));
-
-const unique alloc: Field bool;
-
-axiom FDim(alloc) == 0 && !$IsGhostField(alloc);
-
-function _System.array.Length(a: ref) : int;
-
-axiom (forall o: ref :: 0 <= _System.array.Length(o));
-
-function Int(x: real) : int;
-
-axiom (forall x: real :: { Int(x): int } Int(x): int == int(x));
-
-function Real(x: int) : real;
-
-axiom (forall x: int :: { Real(x): real } Real(x): real == real(x));
-
-axiom (forall i: int :: { Int(Real(i)) } Int(Real(i)) == i);
-
-function {:inline true} _System.real.Trunc(x: real) : int
-{
- Int(x)
-}
-
-type Heap = <alpha>[ref,Field alpha]alpha;
-
-function {:inline true} read<alpha>(H: Heap, r: ref, f: Field alpha) : alpha
-{
- H[r, f]
-}
-
-function {:inline true} update<alpha>(H: Heap, r: ref, f: Field alpha, v: alpha) : Heap
-{
- H[r, f := v]
-}
-
-function $IsGoodHeap(Heap) : bool;
-
-function $IsHeapAnchor(Heap) : bool;
-
-var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);
-
-function $HeapSucc(Heap, Heap) : bool;
-
-axiom (forall<alpha> h: Heap, 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: Heap, b: Heap, c: Heap ::
- { $HeapSucc(a, b), $HeapSucc(b, c) }
- $HeapSucc(a, b) && $HeapSucc(b, c) ==> $HeapSucc(a, c));
-
-axiom (forall h: Heap, k: Heap ::
- { $HeapSucc(h, k) }
- $HeapSucc(h, k)
- ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
-
-function $HeapSuccGhost(Heap, Heap) : bool;
-
-axiom (forall h: Heap, k: Heap ::
- { $HeapSuccGhost(h, k) }
- $HeapSuccGhost(h, k)
- ==> $HeapSucc(h, k)
- && (forall<alpha> o: ref, f: Field alpha ::
- { read(k, o, f) }
- !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
-
-type TickType;
-
-var $Tick: TickType;
-
-procedure $YieldHavoc(this: ref, rds: Set Box, nw: Set Box);
- 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);
-
-
-
-procedure $IterHavoc0(this: ref, rds: Set Box, modi: Set Box);
- 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);
-
-
-
-procedure $IterHavoc1(this: ref, modi: Set Box, nw: Set Box);
- 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: Heap, newHeap: Heap, this: ref, NW: Field (Set Box))
- returns (s: Set Box);
- ensures (forall bx: Box ::
- { s[bx] }
- s[bx]
- <==> read(newHeap, this, NW)[bx]
- || (
- $Unbox(bx) != null
- && !read(prevHeap, $Unbox(bx): ref, alloc)
- && read(newHeap, $Unbox(bx): ref, alloc)));
-
-
-
-type Set T = [T]bool;
-
-function Set#Card<T>(Set T) : int;
-
-axiom (forall<T> s: Set T :: { Set#Card(s) } 0 <= Set#Card(s));
-
-function Set#Empty<T>() : Set T;
-
-axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
-
-axiom (forall<T> s: Set T ::
- { Set#Card(s) }
- (Set#Card(s) == 0 <==> s == Set#Empty())
- && (Set#Card(s) != 0 ==> (exists x: T :: s[x])));
-
-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);
-
-axiom (forall<T> r: T ::
- { Set#Card(Set#Singleton(r)) }
- Set#Card(Set#Singleton(r)) == 1);
-
-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]);
-
-axiom (forall<T> a: Set T, x: T ::
- { Set#Card(Set#UnionOne(a, x)) }
- a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a));
-
-axiom (forall<T> a: Set T, x: T ::
- { Set#Card(Set#UnionOne(a, x)) }
- !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1);
-
-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: Set T, b: Set T, y: T ::
- { Set#Union(a, b), a[y] }
- a[y] ==> Set#Union(a, b)[y]);
-
-axiom (forall<T> a: Set T, b: Set T, y: T ::
- { Set#Union(a, b), b[y] }
- b[y] ==> Set#Union(a, b)[y]);
-
-axiom (forall<T> a: Set T, 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: Set T, 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: Set T, 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: Set T, 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: Set T, b: Set T ::
- { Set#Intersection(a, Set#Intersection(a, b)) }
- Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));
-
-axiom (forall<T> a: Set T, b: Set T ::
- { Set#Card(Set#Union(a, b)) } { Set#Card(Set#Intersection(a, b)) }
- Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b))
- == Set#Card(a) + Set#Card(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: Set T, b: Set T, y: T ::
- { Set#Difference(a, b), b[y] }
- b[y] ==> !Set#Difference(a, b)[y]);
-
-axiom (forall<T> a: Set T, b: Set T ::
- { Set#Card(Set#Difference(a, b)) }
- Set#Card(Set#Difference(a, b))
- + Set#Card(Set#Difference(b, a))
- + Set#Card(Set#Intersection(a, b))
- == Set#Card(Set#Union(a, b))
- && Set#Card(Set#Difference(a, b)) == Set#Card(a) - Set#Card(Set#Intersection(a, b)));
-
-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) } 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]));
-
-type ISet T = [T]bool;
-
-function ISet#Empty<T>() : Set T;
-
-axiom (forall<T> o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]);
-
-function ISet#UnionOne<T>(ISet T, T) : ISet T;
-
-axiom (forall<T> a: ISet T, x: T, o: T ::
- { ISet#UnionOne(a, x)[o] }
- ISet#UnionOne(a, x)[o] <==> o == x || a[o]);
-
-axiom (forall<T> a: ISet T, x: T :: { ISet#UnionOne(a, x) } ISet#UnionOne(a, x)[x]);
-
-axiom (forall<T> a: ISet T, x: T, y: T ::
- { ISet#UnionOne(a, x), a[y] }
- a[y] ==> ISet#UnionOne(a, x)[y]);
-
-function ISet#Union<T>(ISet T, ISet T) : ISet T;
-
-axiom (forall<T> a: ISet T, b: ISet T, o: T ::
- { ISet#Union(a, b)[o] }
- ISet#Union(a, b)[o] <==> a[o] || b[o]);
-
-axiom (forall<T> a: ISet T, b: ISet T, y: T ::
- { ISet#Union(a, b), a[y] }
- a[y] ==> ISet#Union(a, b)[y]);
-
-axiom (forall<T> a: Set T, b: Set T, y: T ::
- { ISet#Union(a, b), b[y] }
- b[y] ==> ISet#Union(a, b)[y]);
-
-axiom (forall<T> a: ISet T, b: ISet T ::
- { ISet#Union(a, b) }
- ISet#Disjoint(a, b)
- ==> ISet#Difference(ISet#Union(a, b), a) == b
- && ISet#Difference(ISet#Union(a, b), b) == a);
-
-function ISet#Intersection<T>(ISet T, ISet T) : ISet T;
-
-axiom (forall<T> a: ISet T, b: ISet T, o: T ::
- { ISet#Intersection(a, b)[o] }
- ISet#Intersection(a, b)[o] <==> a[o] && b[o]);
-
-axiom (forall<T> a: ISet T, b: ISet T ::
- { ISet#Union(ISet#Union(a, b), b) }
- ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b));
-
-axiom (forall<T> a: Set T, b: Set T ::
- { ISet#Union(a, ISet#Union(a, b)) }
- ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b));
-
-axiom (forall<T> a: ISet T, b: ISet T ::
- { ISet#Intersection(ISet#Intersection(a, b), b) }
- ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b));
-
-axiom (forall<T> a: ISet T, b: ISet T ::
- { ISet#Intersection(a, ISet#Intersection(a, b)) }
- ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b));
-
-function ISet#Difference<T>(ISet T, ISet T) : ISet T;
-
-axiom (forall<T> a: ISet T, b: ISet T, o: T ::
- { ISet#Difference(a, b)[o] }
- ISet#Difference(a, b)[o] <==> a[o] && !b[o]);
-
-axiom (forall<T> a: ISet T, b: ISet T, y: T ::
- { ISet#Difference(a, b), b[y] }
- b[y] ==> !ISet#Difference(a, b)[y]);
-
-function ISet#Subset<T>(ISet T, ISet T) : bool;
-
-axiom (forall<T> a: ISet T, b: ISet T ::
- { ISet#Subset(a, b) }
- ISet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o]));
-
-function ISet#Equal<T>(ISet T, ISet T) : bool;
-
-axiom (forall<T> a: ISet T, b: ISet T ::
- { ISet#Equal(a, b) }
- ISet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o]));
-
-axiom (forall<T> a: ISet T, b: ISet T ::
- { ISet#Equal(a, b) }
- ISet#Equal(a, b) ==> a == b);
-
-function ISet#Disjoint<T>(ISet T, ISet T) : bool;
-
-axiom (forall<T> a: ISet T, b: ISet T ::
- { ISet#Disjoint(a, b) }
- ISet#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o]));
-
-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;
-
-axiom (forall<T> ms: MultiSet T ::
- { $IsGoodMultiSet(ms) }
- $IsGoodMultiSet(ms)
- <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms)));
-
-function MultiSet#Card<T>(MultiSet T) : int;
-
-axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
-
-axiom (forall<T> s: MultiSet T, x: T, n: int ::
- { MultiSet#Card(s[x := n]) }
- 0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n);
-
-function MultiSet#Empty<T>() : MultiSet T;
-
-axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);
-
-axiom (forall<T> s: MultiSet T ::
- { MultiSet#Card(s) }
- (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty())
- && (MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < s[x])));
-
-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;
-
-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]);
-
-axiom (forall<T> a: MultiSet T, x: T ::
- { MultiSet#UnionOne(a, x) }
- MultiSet#UnionOne(a, x)[x] == a[x] + 1);
-
-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]);
-
-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]);
-
-axiom (forall<T> a: MultiSet T, x: T ::
- { MultiSet#Card(MultiSet#UnionOne(a, x)) }
- MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1);
-
-function MultiSet#Union<T>(MultiSet T, MultiSet T) : MultiSet T;
-
-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]);
-
-axiom (forall<T> a: MultiSet T, b: MultiSet T ::
- { MultiSet#Card(MultiSet#Union(a, b)) }
- MultiSet#Card(MultiSet#Union(a, b)) == MultiSet#Card(a) + MultiSet#Card(b));
-
-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]));
-
-axiom (forall<T> a: MultiSet T, 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: MultiSet T, b: MultiSet T ::
- { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) }
- MultiSet#Intersection(a, MultiSet#Intersection(a, b))
- == MultiSet#Intersection(a, b));
-
-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: MultiSet T, b: MultiSet T, y: T ::
- { MultiSet#Difference(a, b), b[y], a[y] }
- a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0);
-
-axiom (forall<T> a: MultiSet T, b: MultiSet T ::
- { MultiSet#Card(MultiSet#Difference(a, b)) }
- MultiSet#Card(MultiSet#Difference(a, b))
- + MultiSet#Card(MultiSet#Difference(b, a))
- + 2 * MultiSet#Card(MultiSet#Intersection(a, b))
- == MultiSet#Card(MultiSet#Union(a, b))
- && MultiSet#Card(MultiSet#Difference(a, b))
- == MultiSet#Card(a) - MultiSet#Card(MultiSet#Intersection(a, 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]));
-
-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));
-
-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]));
-
-axiom (forall<T> s: Set T ::
- { MultiSet#Card(MultiSet#FromSet(s)) }
- MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s));
-
-function MultiSet#FromSeq<T>(Seq T) : MultiSet T;
-
-axiom (forall<T> s: Seq T ::
- { MultiSet#FromSeq(s) }
- $IsGoodMultiSet(MultiSet#FromSeq(s)));
-
-axiom (forall<T> s: Seq T ::
- { MultiSet#Card(MultiSet#FromSeq(s)) }
- MultiSet#Card(MultiSet#FromSeq(s)) == Seq#Length(s));
-
-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);
-
-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)));
-
-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]);
-
-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]);
-
-type Seq _;
-
-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());
-
-axiom (forall<T> t: Ty :: { $Is(Seq#Empty(): Seq T, t) } $Is(Seq#Empty(): Seq T, t));
-
-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)));
-
-axiom (forall s: Seq Box, bx: Box, t: Ty ::
- { $Is(Seq#Build(s, bx), TSeq(t)) }
- $Is(s, TSeq(t)) && $IsBox(bx, t) ==> $Is(Seq#Build(s, bx), TSeq(t)));
-
-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));
-
-axiom (forall s0: Seq Box, s1: Seq Box, t: Ty ::
- { $Is(Seq#Append(s0, s1), t) }
- $Is(s0, t) && $Is(s1, t) ==> $Is(Seq#Append(s0, s1), t));
-
-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<T> x: T ::
- { 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) } 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);
-
-axiom (forall<T> s: Seq T, n: int, j: int ::
- {:weight 25} { Seq#Index(Seq#Take(s, n), j) } { Seq#Index(s, j), Seq#Take(s, n) }
- 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);
-
-axiom (forall<T> s: Seq T, n: int, j: int ::
- {:weight 25} { Seq#Index(Seq#Drop(s, n), j) }
- 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: Seq T, n: int, k: int ::
- {:weight 25} { Seq#Index(s, k), Seq#Drop(s, n) }
- 0 <= n && n <= k && k < Seq#Length(s)
- ==> Seq#Index(Seq#Drop(s, n), k - n) == Seq#Index(s, k));
-
-axiom (forall<T> s: Seq T, 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: Heap, a: ref) : Seq Box;
-
-axiom (forall h: Heap, a: ref ::
- { Seq#Length(Seq#FromArray(h, a)) }
- Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
-
-axiom (forall h: Heap, a: ref ::
- { Seq#FromArray(h, a) }
- (forall i: int ::
- { read(h, a, IndexField(i)) } { Seq#Index(Seq#FromArray(h, a): Seq Box, i) }
- 0 <= i && i < Seq#Length(Seq#FromArray(h, a))
- ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
-
-axiom (forall h0: Heap, h1: Heap, a: ref ::
- { Seq#FromArray(h1, a), $HeapSucc(h0, h1) }
- $IsGoodHeap(h0)
- && $IsGoodHeap(h1)
- && $HeapSucc(h0, h1)
- && (forall i: int ::
- 0 <= i && i < _System.array.Length(a)
- ==> read(h0, a, IndexField(i)) == read(h1, a, IndexField(i)))
- ==> Seq#FromArray(h0, a) == Seq#FromArray(h1, a));
-
-axiom (forall h: Heap, i: int, v: Box, 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));
-
-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));
-
-axiom (forall h: Heap, a: ref, n0: int, 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 Box)));
-
-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));
-
-function Seq#Rank<T>(Seq T) : int;
-
-axiom (forall s: Seq Box, i: int ::
- { DtRank($Unbox(Seq#Index(s, i)): DatatypeType) }
- 0 <= i && i < Seq#Length(s)
- ==> DtRank($Unbox(Seq#Index(s, i)): DatatypeType) < Seq#Rank(s));
-
-axiom (forall<T> s: Seq T, i: int ::
- { Seq#Rank(Seq#Drop(s, i)) }
- 0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s));
-
-axiom (forall<T> s: Seq T, i: int ::
- { Seq#Rank(Seq#Take(s, i)) }
- 0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s));
-
-axiom (forall<T> s: Seq T, i: int, j: int ::
- { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) }
- 0 <= i && i < j && j <= Seq#Length(s)
- ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s));
-
-axiom (forall<T> s: Seq T, n: int ::
- { Seq#Drop(s, n) }
- n == 0 ==> Seq#Drop(s, n) == s);
-
-axiom (forall<T> s: Seq T, n: int ::
- { Seq#Take(s, n) }
- n == 0 ==> Seq#Take(s, n) == Seq#Empty());
-
-axiom (forall<T> s: Seq T, m: int, n: int ::
- { Seq#Drop(Seq#Drop(s, m), n) }
- 0 <= m && 0 <= n && m + n <= Seq#Length(s)
- ==> Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m + n));
-
-type Map _ _;
-
-function Map#Domain<U,V>(Map U V) : [U]bool;
-
-function Map#Elements<U,V>(Map U V) : [U]V;
-
-function Map#Card<U,V>(Map U V) : int;
-
-axiom (forall<U,V> m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m));
-
-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]);
-
-axiom (forall<U,V> m: Map U V ::
- { Map#Card(m) }
- (Map#Card(m) == 0 <==> m == Map#Empty())
- && (Map#Card(m) != 0 ==> (exists x: U :: Map#Domain(m)[x])));
-
-function Map#Glue<U,V>([U]bool, [U]V, Ty) : Map U V;
-
-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
- { Map#Domain(Map#Glue(a, b, t)) }
- Map#Domain(Map#Glue(a, b, t)) == a);
-
-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
- { Map#Elements(Map#Glue(a, b, t)) }
- Map#Elements(Map#Glue(a, b, t)) == b);
-
-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
- { $Is(Map#Glue(a, b, t), t) }
- $Is(Map#Glue(a, b, t), t));
-
-function Map#Build<U,V>(Map U V, U, V) : Map 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']));
-
-axiom (forall<U,V> m: Map U V, u: U, v: V ::
- { Map#Card(Map#Build(m, u, v)) }
- Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m));
-
-axiom (forall<U,V> m: Map U V, u: U, v: V ::
- { Map#Card(Map#Build(m, u, v)) }
- !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1);
-
-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]));
-
-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]));
-
-type IMap _ _;
-
-function IMap#Domain<U,V>(IMap U V) : [U]bool;
-
-function IMap#Elements<U,V>(IMap U V) : [U]V;
-
-function IMap#Empty<U,V>() : IMap U V;
-
-axiom (forall<U,V> u: U ::
- { IMap#Domain(IMap#Empty(): IMap U V)[u] }
- !IMap#Domain(IMap#Empty(): IMap U V)[u]);
-
-function IMap#Glue<U,V>([U]bool, [U]V, Ty) : IMap U V;
-
-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
- { IMap#Domain(IMap#Glue(a, b, t)) }
- IMap#Domain(IMap#Glue(a, b, t)) == a);
-
-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
- { IMap#Elements(IMap#Glue(a, b, t)) }
- IMap#Elements(IMap#Glue(a, b, t)) == b);
-
-axiom (forall<U,V> a: [U]bool, b: [U]V, t: Ty ::
- { $Is(IMap#Glue(a, b, t), t) }
- $Is(IMap#Glue(a, b, t), t));
-
-function IMap#Build<U,V>(IMap U V, U, V) : IMap U V;
-
-axiom (forall<U,V> m: IMap U V, u: U, u': U, v: V ::
- { IMap#Domain(IMap#Build(m, u, v))[u'] }
- { IMap#Elements(IMap#Build(m, u, v))[u'] }
- (u' == u
- ==> IMap#Domain(IMap#Build(m, u, v))[u']
- && IMap#Elements(IMap#Build(m, u, v))[u'] == v)
- && (u' != u
- ==> IMap#Domain(IMap#Build(m, u, v))[u'] == IMap#Domain(m)[u']
- && IMap#Elements(IMap#Build(m, u, v))[u'] == IMap#Elements(m)[u']));
-
-function IMap#Equal<U,V>(IMap U V, IMap U V) : bool;
-
-axiom (forall<U,V> m: IMap U V, m': IMap U V ::
- { IMap#Equal(m, m') }
- IMap#Equal(m, m')
- <==> (forall u: U :: IMap#Domain(m)[u] == IMap#Domain(m')[u])
- && (forall u: U ::
- IMap#Domain(m)[u] ==> IMap#Elements(m)[u] == IMap#Elements(m')[u]));
-
-axiom (forall<U,V> m: IMap U V, m': IMap U V ::
- { IMap#Equal(m, m') }
- IMap#Equal(m, m') ==> m == m');
-
-function INTERNAL_add_boogie(x: int, y: int) : int;
-
-axiom (forall x: int, y: int ::
- { INTERNAL_add_boogie(x, y): int }
- INTERNAL_add_boogie(x, y): int == x + y);
-
-function INTERNAL_sub_boogie(x: int, y: int) : int;
-
-axiom (forall x: int, y: int ::
- { INTERNAL_sub_boogie(x, y): int }
- INTERNAL_sub_boogie(x, y): int == x - y);
-
-function INTERNAL_mul_boogie(x: int, y: int) : int;
-
-axiom (forall x: int, y: int ::
- { INTERNAL_mul_boogie(x, y): int }
- INTERNAL_mul_boogie(x, y): int == x * y);
-
-function INTERNAL_div_boogie(x: int, y: int) : int;
-
-axiom (forall x: int, y: int ::
- { INTERNAL_div_boogie(x, y): int }
- INTERNAL_div_boogie(x, y): int == x div y);
-
-function INTERNAL_mod_boogie(x: int, y: int) : int;
-
-axiom (forall x: int, y: int ::
- { INTERNAL_mod_boogie(x, y): int }
- INTERNAL_mod_boogie(x, y): int == x mod y);
-
-function {:never_pattern true} INTERNAL_lt_boogie(x: int, y: int) : bool;
-
-axiom (forall x: int, y: int ::
- {:never_pattern true} { INTERNAL_lt_boogie(x, y): bool }
- INTERNAL_lt_boogie(x, y): bool == (x < y));
-
-function {:never_pattern true} INTERNAL_le_boogie(x: int, y: int) : bool;
-
-axiom (forall x: int, y: int ::
- {:never_pattern true} { INTERNAL_le_boogie(x, y): bool }
- INTERNAL_le_boogie(x, y): bool == (x <= y));
-
-function {:never_pattern true} INTERNAL_gt_boogie(x: int, y: int) : bool;
-
-axiom (forall x: int, y: int ::
- {:never_pattern true} { INTERNAL_gt_boogie(x, y): bool }
- INTERNAL_gt_boogie(x, y): bool == (x > y));
-
-function {:never_pattern true} INTERNAL_ge_boogie(x: int, y: int) : bool;
-
-axiom (forall x: int, y: int ::
- {:never_pattern true} { INTERNAL_ge_boogie(x, y): bool }
- INTERNAL_ge_boogie(x, y): bool == (x >= y));
-
-const unique class._System.object: ClassName;
-
-// Tclass._System.object Tag
-axiom Tag(Tclass._System.object()) == Tagclass._System.object;
-
-const unique Tagclass._System.object: TyTag;
-
-// Box/unbox axiom for Tclass._System.object
-axiom (forall bx: Box ::
- { $IsBox(bx, Tclass._System.object()) }
- $IsBox(bx, Tclass._System.object())
- ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.object()));
-
-// object: Class $Is
-axiom (forall $o: ref ::
- { $Is($o, Tclass._System.object()) }
- $Is($o, Tclass._System.object()));
-
-// object: Class $IsAlloc
-axiom (forall $o: ref, $h: Heap ::
- { $IsAlloc($o, Tclass._System.object(), $h) }
- $IsAlloc($o, Tclass._System.object(), $h) <==> $o == null || read($h, $o, alloc));
-
-const unique class._System.array: ClassName;
-
-function Tclass._System.array(Ty) : Ty;
-
-// Tclass._System.array Tag
-axiom (forall #$arg: Ty ::
- { Tclass._System.array(#$arg) }
- Tag(Tclass._System.array(#$arg)) == Tagclass._System.array);
-
-const unique Tagclass._System.array: TyTag;
-
-// Tclass._System.array injectivity 0
-axiom (forall #$arg: Ty ::
- { Tclass._System.array(#$arg) }
- Tclass._System.array_0(Tclass._System.array(#$arg)) == #$arg);
-
-function Tclass._System.array_0(Ty) : Ty;
-
-// Box/unbox axiom for Tclass._System.array
-axiom (forall #$arg: Ty, bx: Box ::
- { $IsBox(bx, Tclass._System.array(#$arg)) }
- $IsBox(bx, Tclass._System.array(#$arg))
- ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.array(#$arg)));
-
-// array.: Allocation axiom
-axiom (forall #$arg: Ty, $i0: int, $h: Heap, $o: ref ::
- { read($h, $o, IndexField($i0)), Tclass._System.array(#$arg) }
- $IsGoodHeap($h)
- && $o != null
- && dtype($o) == Tclass._System.array(#$arg)
- &&
- 0 <= $i0
- && $i0 < _System.array.Length($o)
- ==> $IsBox(read($h, $o, IndexField($i0)), #$arg)
- && (read($h, $o, alloc) ==> $IsAllocBox(read($h, $o, IndexField($i0)), #$arg, $h)));
-
-// array: Class $Is
-axiom (forall #$arg: Ty, $o: ref ::
- { $Is($o, Tclass._System.array(#$arg)) }
- $Is($o, Tclass._System.array(#$arg))
- <==> $o == null || dtype($o) == Tclass._System.array(#$arg));
-
-// array: Class $IsAlloc
-axiom (forall #$arg: Ty, $o: ref, $h: Heap ::
- { $IsAlloc($o, Tclass._System.array(#$arg), $h) }
- $IsAlloc($o, Tclass._System.array(#$arg), $h)
- <==> $o == null || read($h, $o, alloc));
-
-// array.Length: Allocation axiom
-axiom (forall #$arg: Ty, $h: Heap, $o: ref ::
- $IsGoodHeap($h) && $o != null && dtype($o) == Tclass._System.array(#$arg)
- ==> $Is(_System.array.Length($o), TInt)
- && (read($h, $o, alloc) ==> $IsAlloc(_System.array.Length($o), TInt, $h)));
-
-function Tclass._System.___hFunc0(Ty) : Ty;
-
-// Tclass._System.___hFunc0 Tag
-axiom (forall #$T0: Ty ::
- { Tclass._System.___hFunc0(#$T0) }
- Tag(Tclass._System.___hFunc0(#$T0)) == Tagclass._System.___hFunc0);
-
-const unique Tagclass._System.___hFunc0: TyTag;
-
-// Tclass._System.___hFunc0 injectivity 0
-axiom (forall #$T0: Ty ::
- { Tclass._System.___hFunc0(#$T0) }
- Tclass._System.___hFunc0_0(Tclass._System.___hFunc0(#$T0)) == #$T0);
-
-function Tclass._System.___hFunc0_0(Ty) : Ty;
-
-// Box/unbox axiom for Tclass._System.___hFunc0
-axiom (forall #$T0: Ty, bx: Box ::
- { $IsBox(bx, Tclass._System.___hFunc0(#$T0)) }
- $IsBox(bx, Tclass._System.___hFunc0(#$T0))
- ==> $Box($Unbox(bx): HandleType) == bx
- && $Is($Unbox(bx): HandleType, Tclass._System.___hFunc0(#$T0)));
-
-function Handle0([Heap]Box, [Heap]bool, [Heap]Set Box) : HandleType;
-
-function Apply0(Ty, HandleType, Heap) : Box;
-
-function Requires0(Ty, HandleType, Heap) : bool;
-
-function Reads0(Ty, HandleType, Heap) : Set Box;
-
-axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box ::
- { Apply0(t0, Handle0(h, r, rd), heap) }
- Apply0(t0, Handle0(h, r, rd), heap) == h[heap]);
-
-axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box ::
- { Requires0(t0, Handle0(h, r, rd), heap) }
- r[heap] ==> Requires0(t0, Handle0(h, r, rd), heap));
-
-axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box, bx: Box ::
- { Reads0(t0, Handle0(h, r, rd), heap)[bx] }
- Reads0(t0, Handle0(h, r, rd), heap)[bx] == rd[heap][bx]);
-
-function {:inline true} _System.___hFunc0.requires(t0: Ty, heap: Heap, f: HandleType) : bool
-{
- Requires0(t0, f, heap)
-}
-
-function {:inline true} _System.___hFunc0.requires#canCall(t0: Ty, heap: Heap, f: HandleType) : bool
-{
- true
-}
-
-function {:inline true} _System.___hFunc0.reads(t0: Ty, heap: Heap, f: HandleType) : Set Box
-{
- Reads0(t0, f, heap)
-}
-
-function {:inline true} _System.___hFunc0.reads#canCall(t0: Ty, heap: Heap, f: HandleType) : bool
-{
- true
-}
-
-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
- { $HeapSucc(h0, h1), Reads0(t0, f, h1) }
- $HeapSucc(h0, h1)
- &&
- $IsGoodHeap(h0)
- && $IsGoodHeap(h1)
- &&
- $Is(f, Tclass._System.___hFunc0(t0))
- && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
- && (forall<a> o: ref, fld: Field a ::
- o != null
- && read(h0, o, alloc)
- && read(h1, o, alloc)
- && Reads0(t0, f, h0)[$Box(o)]
- ==> read(h0, o, fld) == read(h1, o, fld))
- ==> Reads0(t0, f, h0) == Reads0(t0, f, h1));
-
-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
- { $HeapSucc(h0, h1), Reads0(t0, f, h1) }
- $HeapSucc(h0, h1)
- &&
- $IsGoodHeap(h0)
- && $IsGoodHeap(h1)
- &&
- $Is(f, Tclass._System.___hFunc0(t0))
- && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
- && (forall<a> o: ref, fld: Field a ::
- o != null
- && read(h0, o, alloc)
- && read(h1, o, alloc)
- && Reads0(t0, f, h1)[$Box(o)]
- ==> read(h0, o, fld) == read(h1, o, fld))
- ==> Reads0(t0, f, h0) == Reads0(t0, f, h1));
-
-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
- { $HeapSucc(h0, h1), Requires0(t0, f, h1) }
- $HeapSucc(h0, h1)
- &&
- $IsGoodHeap(h0)
- && $IsGoodHeap(h1)
- &&
- $Is(f, Tclass._System.___hFunc0(t0))
- && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
- && (forall<a> o: ref, fld: Field a ::
- o != null
- && read(h0, o, alloc)
- && read(h1, o, alloc)
- && Reads0(t0, f, h0)[$Box(o)]
- ==> read(h0, o, fld) == read(h1, o, fld))
- ==> Requires0(t0, f, h0) == Requires0(t0, f, h1));
-
-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
- { $HeapSucc(h0, h1), Requires0(t0, f, h1) }
- $HeapSucc(h0, h1)
- &&
- $IsGoodHeap(h0)
- && $IsGoodHeap(h1)
- &&
- $Is(f, Tclass._System.___hFunc0(t0))
- && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
- && (forall<a> o: ref, fld: Field a ::
- o != null
- && read(h0, o, alloc)
- && read(h1, o, alloc)
- && Reads0(t0, f, h1)[$Box(o)]
- ==> read(h0, o, fld) == read(h1, o, fld))
- ==> Requires0(t0, f, h0) == Requires0(t0, f, h1));
-
-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
- { $HeapSucc(h0, h1), Apply0(t0, f, h1) }
- $HeapSucc(h0, h1)
- &&
- $IsGoodHeap(h0)
- && $IsGoodHeap(h1)
- &&
- $Is(f, Tclass._System.___hFunc0(t0))
- && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
- && (forall<a> o: ref, fld: Field a ::
- o != null
- && read(h0, o, alloc)
- && read(h1, o, alloc)
- && Reads0(t0, f, h0)[$Box(o)]
- ==> read(h0, o, fld) == read(h1, o, fld))
- ==> Apply0(t0, f, h0) == Apply0(t0, f, h1));
-
-axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType ::
- { $HeapSucc(h0, h1), Apply0(t0, f, h1) }
- $HeapSucc(h0, h1)
- &&
- $IsGoodHeap(h0)
- && $IsGoodHeap(h1)
- &&
- $Is(f, Tclass._System.___hFunc0(t0))
- && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0)
- && (forall<a> o: ref, fld: Field a ::
- o != null
- && read(h0, o, alloc)
- && read(h1, o, alloc)
- && Reads0(t0, f, h1)[$Box(o)]
- ==> read(h0, o, fld) == read(h1, o, fld))
- ==> Apply0(t0, f, h0) == Apply0(t0, f, h1));
-
-axiom (forall t0: Ty, h: Heap, f: HandleType ::
- { Apply0(t0, f, h) }
- $IsGoodHeap(h)
- &&
- $Is(f, Tclass._System.___hFunc0(t0))
- && $IsAlloc(f, Tclass._System.___hFunc0(t0), h)
- ==> $IsBox(Apply0(t0, f, h), t0) && $IsAllocBox(Apply0(t0, f, h), t0, h));
-
-const unique class._module.__default: ClassName;
-
-function Tclass._module.__default() : Ty;
-
-// Tclass._module.__default Tag
-axiom Tag(Tclass._module.__default()) == Tagclass._module.__default;
-
-const unique Tagclass._module.__default: TyTag;
-
-// Box/unbox axiom for Tclass._module.__default
-axiom (forall bx: Box ::
- { $IsBox(bx, Tclass._module.__default()) }
- $IsBox(bx, Tclass._module.__default())
- ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._module.__default()));
-
-// _default: Class $Is
-axiom (forall $o: ref ::
- { $Is($o, Tclass._module.__default()) }
- $Is($o, Tclass._module.__default())
- <==> $o == null || dtype($o) == Tclass._module.__default());
-
-// _default: Class $IsAlloc
-axiom (forall $o: ref, $h: Heap ::
- { $IsAlloc($o, Tclass._module.__default(), $h) }
- $IsAlloc($o, Tclass._module.__default(), $h)
- <==> $o == null || read($h, $o, alloc));
-
-procedure CheckWellformed$$_module.__default.test();
- free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;
- modifies $Heap, $Tick;
-
-
-
-implementation CheckWellformed$$_module.__default.test()
-{
- var $_Frame: <beta>[ref,Field beta]bool;
-
- // AddMethodImpl: test, CheckWellformed$$_module.__default.test
- $_Frame := (lambda<alpha> $o: ref, $f: Field alpha ::
- $o != null && read($Heap, $o, alloc) ==> false);
- assume {:captureState "Bug136.dfy(4,7): initial state"} true;
- havoc $Heap;
- assume (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));
- assume $HeapSucc(old($Heap), $Heap);
-}
-
-
-
-procedure InterModuleCall$$_module.__default.test();
- modifies $Heap, $Tick;
- // frame condition
- free 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));
- // boilerplate
- free ensures $HeapSucc(old($Heap), $Heap);
-
-
-
-procedure IntraModuleCall$$_module.__default.test();
- modifies $Heap, $Tick;
- // frame condition
- free 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));
- // boilerplate
- free ensures $HeapSucc(old($Heap), $Heap);
-
-
-
-procedure Impl$$_module.__default.test() returns ($_reverifyPost: bool);
- free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;
- modifies $Heap, $Tick;
- // frame condition
- free 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));
- // boilerplate
- free ensures $HeapSucc(old($Heap), $Heap);
-
-
-
-implementation Impl$$_module.__default.test() returns ($_reverifyPost: bool)
-{
- var $_Frame: <beta>[ref,Field beta]bool;
-
- // AddMethodImpl: test, Impl$$_module.__default.test
- $_Frame := (lambda<alpha> $o: ref, $f: Field alpha ::
- $o != null && read($Heap, $o, alloc) ==> false);
- assume {:captureState "Bug136.dfy(5,1): initial state"} true;
- $_reverifyPost := false;
- // ----- assume statement ----- Bug136.dfy(6,5)
- assume true;
- assume false;
- // ----- assert statement ----- Bug136.dfy(7,5)
- assume true;
- assert true;
-}
-
-
Dafny program verifier finished with 2 verified, 0 errors