From 13a88d7263c02590f5be9bb9944c0ab43b76bccc Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 26 Feb 2016 09:56:59 -0800 Subject: Fix issue 136. Less aggressive Lit wrap for assert/assume. --- Test/dafny0/DTypes.dfy | 2 +- Test/dafny0/snapshots/Snapshots0.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots1.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots2.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots3.run.dfy.expect | 6 +- Test/dafny0/snapshots/Snapshots4.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots6.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots7.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots8.run.dfy.expect | 4 +- Test/dafny4/Bug136.dfy | 12 + Test/dafny4/Bug136.dfy.expect | 1772 +++++++++++++++++++++++ 11 files changed, 1802 insertions(+), 18 deletions(-) create mode 100644 Test/dafny4/Bug136.dfy create mode 100644 Test/dafny4/Bug136.dfy.expect (limited to 'Test') diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index 9e36e64c..9891c040 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect index d32cd9bb..bf7388cf 100644 --- a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect @@ -1,6 +1,6 @@ Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> DoNothingToAssert -Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots0.v0.dfy(4,10)) assert false; >>> DoNothingToAssert Dafny program verifier finished with 3 verified, 0 errors @@ -16,7 +16,7 @@ Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall $o: ref, $f >>> MarkAsFullyVerified Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap); >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots0.v1.dfy(4,10)) assert false; >>> MarkAsPartiallyVerified Snapshots0.v1.dfy(4,9): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect index 6d5e43f8..1b5c8d24 100644 --- a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect @@ -1,6 +1,6 @@ Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> DoNothingToAssert -Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots1.v0.dfy(4,10)) assert false; >>> DoNothingToAssert Processing command (at Snapshots1.v0.dfy(12,3)) assert true; >>> DoNothingToAssert @@ -12,7 +12,7 @@ Processing command (at Snapshots1.v1.dfy(12,3)) assert true; >>> MarkAsFullyVerified Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> MarkAsFullyVerified -Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots1.v1.dfy(4,10)) assert false; >>> DoNothingToAssert Snapshots1.v1.dfy(4,9): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect index ee2ceecd..949ecec9 100644 --- a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect @@ -1,6 +1,6 @@ Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots2.v0.dfy(4,10)) assert false; >>> DoNothingToAssert Processing command (at Snapshots2.v0.dfy(11,11)) assert true; >>> DoNothingToAssert @@ -24,7 +24,7 @@ Processing command (at Snapshots2.v1.dfy(18,3)) assert true; >>> MarkAsFullyVerified Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> MarkAsFullyVerified -Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots2.v1.dfy(4,10)) assert false; >>> DoNothingToAssert Snapshots2.v1.dfy(4,9): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect index accacd90..a7f05a68 100644 --- a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect @@ -1,4 +1,4 @@ -Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0); +Processing command (at Snapshots3.v0.dfy(9,14)) assert 0 != 0; >>> DoNothingToAssert Snapshots3.v0.dfy(9,13): Error: assertion violation Execution trace: @@ -6,9 +6,9 @@ Execution trace: (0,0): anon3_Else Dafny program verifier finished with 1 verified, 1 error -Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true); +Processing command (at Snapshots3.v1.dfy(5,12)) assert true; >>> DoNothingToAssert -Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0); +Processing command (at Snapshots3.v1.dfy(9,14)) assert 0 != 0; >>> RecycleError Snapshots3.v0.dfy(9,13): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect index d56eb9d0..e0f07849 100644 --- a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect @@ -2,11 +2,11 @@ Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0); >>> DoNothingToAssert Dafny program verifier finished with 2 verified, 0 errors -Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1); +Processing command (at Snapshots4.v1.dfy(5,14)) assert 1 != 1; >>> DoNothingToAssert Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0); >>> MarkAsFullyVerified -Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2); +Processing command (at Snapshots4.v1.dfy(10,14)) assert 2 != 2; >>> DoNothingToAssert Snapshots4.v1.dfy(5,13): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect index bef5a87d..cdb942bb 100644 --- a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect @@ -1,8 +1,8 @@ -Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false); +Processing command (at Snapshots6.v0.dfy(20,14)) assert false; >>> DoNothingToAssert Dafny program verifier finished with 4 verified, 0 errors -Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false); +Processing command (at Snapshots6.v1.dfy(20,14)) assert false; >>> DoNothingToAssert Snapshots6.v1.dfy(20,13): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect index b90a6034..a08b32c6 100644 --- a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect @@ -1,4 +1,4 @@ -Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false); +Processing command (at Snapshots7.v0.dfy(19,14)) assert false; >>> DoNothingToAssert Dafny program verifier finished with 4 verified, 0 errors @@ -22,7 +22,7 @@ Processing command (at ) a##cached##0 := a##cached##0 && ##ext >>> AssumeNegationOfAssumptionVariable Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##4(); >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false); +Processing command (at Snapshots7.v1.dfy(19,14)) assert false; >>> MarkAsPartiallyVerified Snapshots7.v1.dfy(19,13): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect index 625b71b4..e1cbdbe0 100644 --- a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect @@ -20,7 +20,7 @@ Snapshots8.v0.dfy(13,12): Related location: This is the postcondition that might Processing command (at Snapshots8.v0.dfy(23,12)) assert u#0 != 53; >>> DoNothingToAssert Snapshots8.v0.dfy(23,11): Error: assertion violation -Processing command (at Snapshots8.v0.dfy(28,10)) assert Lit(true); +Processing command (at Snapshots8.v0.dfy(28,10)) assert true; >>> DoNothingToAssert Dafny program verifier finished with 7 verified, 4 errors @@ -45,7 +45,7 @@ Snapshots8.v1.dfy(12,20): Related location: This is the precondition that might Snapshots8.v1.dfy(7,11): Error: assertion violation Processing command (at Snapshots8.v1.dfy(21,12)) assert true; >>> MarkAsFullyVerified -Processing command (at Snapshots8.v1.dfy(23,12)) assert Lit(true); +Processing command (at Snapshots8.v1.dfy(23,12)) assert true; >>> DoNothingToAssert Processing command (at Snapshots8.v1.dfy(19,13)) assert LitInt(2) <= z#0; >>> DoNothingToAssert diff --git a/Test/dafny4/Bug136.dfy b/Test/dafny4/Bug136.dfy new file mode 100644 index 00000000..5f3cde69 --- /dev/null +++ b/Test/dafny4/Bug136.dfy @@ -0,0 +1,12 @@ +// RUN: %dafny /compile:0 /print:- "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method test() +{ + assume false; + assert true; +} + + + + diff --git a/Test/dafny4/Bug136.dfy.expect b/Test/dafny4/Bug136.dfy.expect new file mode 100644 index 00000000..8b9d32a8 --- /dev/null +++ b/Test/dafny4/Bug136.dfy.expect @@ -0,0 +1,1772 @@ +// 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(x: T) : T; + +axiom (forall x: T :: {:identity} { Lit(x): T } Lit(x): T == x); + +axiom (forall 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) : Box; + +function $Unbox(Box) : T; + +axiom (forall 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 v: T, t: Ty :: + { $IsBox($Box(v), t) } + $IsBox($Box(v), t) <==> $Is(v, t)); + +axiom (forall v: T, t: Ty, h: Heap :: + { $IsAllocBox($Box(v), t, h) } + $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v, t, h)); + +function $Is(T, Ty) : bool; + +function $IsAlloc(T, Ty, Heap) : bool; + +function $IsBox(T, Ty) : bool; + +function $IsAllocBox(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([LayerType]A, LayerType) : A; + +axiom (forall f: [LayerType]A, ly: LayerType :: + { AtLayer(f, ly) } + AtLayer(f, ly) == f[ly]); + +axiom (forall f: [LayerType]A, ly: LayerType :: + { AtLayer(f, $LS(ly)) } + AtLayer(f, $LS(ly)) == AtLayer(f, ly)); + +type Field _; + +function FDim(Field T) : int; + +function IndexField(int) : Field Box; + +axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1); + +function IndexField_Inverse(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(Field T) : Field T; + +function MultiIndexField_Inverse1(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(Field T) : ClassName; + +type NameFamily; + +function DeclName(Field T) : NameFamily; + +function FieldOfDecl(ClassName, NameFamily) : Field alpha; + +axiom (forall 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(Field T) : bool; + +axiom (forall 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 = [ref,Field alpha]alpha; + +function {:inline true} read(H: Heap, r: ref, f: Field alpha) : alpha +{ + H[r, f] +} + +function {:inline true} update(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 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 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 $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 $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 $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(Set T) : int; + +axiom (forall s: Set T :: { Set#Card(s) } 0 <= Set#Card(s)); + +function Set#Empty() : Set T; + +axiom (forall o: T :: { Set#Empty()[o] } !Set#Empty()[o]); + +axiom (forall 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) : Set T; + +axiom (forall r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]); + +axiom (forall r: T, o: T :: + { Set#Singleton(r)[o] } + Set#Singleton(r)[o] <==> r == o); + +axiom (forall r: T :: + { Set#Card(Set#Singleton(r)) } + Set#Card(Set#Singleton(r)) == 1); + +function Set#UnionOne(Set T, T) : Set T; + +axiom (forall a: Set T, x: T, o: T :: + { Set#UnionOne(a, x)[o] } + Set#UnionOne(a, x)[o] <==> o == x || a[o]); + +axiom (forall a: Set T, x: T :: { Set#UnionOne(a, x) } Set#UnionOne(a, x)[x]); + +axiom (forall a: Set T, x: T, y: T :: + { Set#UnionOne(a, x), a[y] } + a[y] ==> Set#UnionOne(a, x)[y]); + +axiom (forall a: Set T, x: T :: + { Set#Card(Set#UnionOne(a, x)) } + a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a)); + +axiom (forall 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(Set T, Set T) : Set T; + +axiom (forall a: Set T, b: Set T, o: T :: + { Set#Union(a, b)[o] } + Set#Union(a, b)[o] <==> a[o] || b[o]); + +axiom (forall a: Set T, b: Set T, y: T :: + { Set#Union(a, b), a[y] } + a[y] ==> Set#Union(a, b)[y]); + +axiom (forall a: Set T, b: Set T, y: T :: + { Set#Union(a, b), b[y] } + b[y] ==> Set#Union(a, b)[y]); + +axiom (forall 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(Set T, Set T) : Set T; + +axiom (forall a: Set T, b: Set T, o: T :: + { Set#Intersection(a, b)[o] } + Set#Intersection(a, b)[o] <==> a[o] && b[o]); + +axiom (forall 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 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 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 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 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(Set T, Set T) : Set T; + +axiom (forall a: Set T, b: Set T, o: T :: + { Set#Difference(a, b)[o] } + Set#Difference(a, b)[o] <==> a[o] && !b[o]); + +axiom (forall a: Set T, b: Set T, y: T :: + { Set#Difference(a, b), b[y] } + b[y] ==> !Set#Difference(a, b)[y]); + +axiom (forall 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(Set T, Set T) : bool; + +axiom (forall 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(Set T, Set T) : bool; + +axiom (forall 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 a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) ==> a == b); + +function Set#Disjoint(Set T, Set T) : bool; + +axiom (forall 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() : Set T; + +axiom (forall o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]); + +function ISet#UnionOne(ISet T, T) : ISet T; + +axiom (forall a: ISet T, x: T, o: T :: + { ISet#UnionOne(a, x)[o] } + ISet#UnionOne(a, x)[o] <==> o == x || a[o]); + +axiom (forall a: ISet T, x: T :: { ISet#UnionOne(a, x) } ISet#UnionOne(a, x)[x]); + +axiom (forall a: ISet T, x: T, y: T :: + { ISet#UnionOne(a, x), a[y] } + a[y] ==> ISet#UnionOne(a, x)[y]); + +function ISet#Union(ISet T, ISet T) : ISet T; + +axiom (forall a: ISet T, b: ISet T, o: T :: + { ISet#Union(a, b)[o] } + ISet#Union(a, b)[o] <==> a[o] || b[o]); + +axiom (forall a: ISet T, b: ISet T, y: T :: + { ISet#Union(a, b), a[y] } + a[y] ==> ISet#Union(a, b)[y]); + +axiom (forall a: Set T, b: Set T, y: T :: + { ISet#Union(a, b), b[y] } + b[y] ==> ISet#Union(a, b)[y]); + +axiom (forall 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(ISet T, ISet T) : ISet T; + +axiom (forall a: ISet T, b: ISet T, o: T :: + { ISet#Intersection(a, b)[o] } + ISet#Intersection(a, b)[o] <==> a[o] && b[o]); + +axiom (forall 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 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 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 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(ISet T, ISet T) : ISet T; + +axiom (forall a: ISet T, b: ISet T, o: T :: + { ISet#Difference(a, b)[o] } + ISet#Difference(a, b)[o] <==> a[o] && !b[o]); + +axiom (forall a: ISet T, b: ISet T, y: T :: + { ISet#Difference(a, b), b[y] } + b[y] ==> !ISet#Difference(a, b)[y]); + +function ISet#Subset(ISet T, ISet T) : bool; + +axiom (forall 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(ISet T, ISet T) : bool; + +axiom (forall 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 a: ISet T, b: ISet T :: + { ISet#Equal(a, b) } + ISet#Equal(a, b) ==> a == b); + +function ISet#Disjoint(ISet T, ISet T) : bool; + +axiom (forall 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(ms: MultiSet T) : bool; + +axiom (forall ms: MultiSet T :: + { $IsGoodMultiSet(ms) } + $IsGoodMultiSet(ms) + <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms))); + +function MultiSet#Card(MultiSet T) : int; + +axiom (forall s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s)); + +axiom (forall 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() : MultiSet T; + +axiom (forall o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0); + +axiom (forall 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) : MultiSet T; + +axiom (forall r: T, o: T :: + { MultiSet#Singleton(r)[o] } + (MultiSet#Singleton(r)[o] == 1 <==> r == o) + && (MultiSet#Singleton(r)[o] == 0 <==> r != o)); + +axiom (forall r: T :: + { MultiSet#Singleton(r) } + MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r)); + +function MultiSet#UnionOne(MultiSet T, T) : MultiSet T; + +axiom (forall 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 a: MultiSet T, x: T :: + { MultiSet#UnionOne(a, x) } + MultiSet#UnionOne(a, x)[x] == a[x] + 1); + +axiom (forall a: MultiSet T, x: T, y: T :: + { MultiSet#UnionOne(a, x), a[y] } + 0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]); + +axiom (forall a: MultiSet T, x: T, y: T :: + { MultiSet#UnionOne(a, x), a[y] } + x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]); + +axiom (forall a: MultiSet T, x: T :: + { MultiSet#Card(MultiSet#UnionOne(a, x)) } + MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1); + +function MultiSet#Union(MultiSet T, MultiSet T) : MultiSet T; + +axiom (forall a: MultiSet T, b: MultiSet T, o: T :: + { MultiSet#Union(a, b)[o] } + MultiSet#Union(a, b)[o] == a[o] + b[o]); + +axiom (forall 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(MultiSet T, MultiSet T) : MultiSet T; + +axiom (forall 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 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 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(MultiSet T, MultiSet T) : MultiSet T; + +axiom (forall 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 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 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(MultiSet T, MultiSet T) : bool; + +axiom (forall 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(MultiSet T, MultiSet T) : bool; + +axiom (forall 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 a: MultiSet T, b: MultiSet T :: + { MultiSet#Equal(a, b) } + MultiSet#Equal(a, b) ==> a == b); + +function MultiSet#Disjoint(MultiSet T, MultiSet T) : bool; + +axiom (forall 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(Set T) : MultiSet T; + +axiom (forall 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 s: Set T :: + { MultiSet#Card(MultiSet#FromSet(s)) } + MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s)); + +function MultiSet#FromSeq(Seq T) : MultiSet T; + +axiom (forall s: Seq T :: + { MultiSet#FromSeq(s) } + $IsGoodMultiSet(MultiSet#FromSeq(s))); + +axiom (forall s: Seq T :: + { MultiSet#Card(MultiSet#FromSeq(s)) } + MultiSet#Card(MultiSet#FromSeq(s)) == Seq#Length(s)); + +axiom (forall 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 :: + MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T); + +axiom (forall 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 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 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(Seq T) : int; + +axiom (forall s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s)); + +function Seq#Empty() : Seq T; + +axiom (forall :: Seq#Length(Seq#Empty(): Seq T) == 0); + +axiom (forall s: Seq T :: + { Seq#Length(s) } + Seq#Length(s) == 0 ==> s == Seq#Empty()); + +axiom (forall t: Ty :: { $Is(Seq#Empty(): Seq T, t) } $Is(Seq#Empty(): Seq T, t)); + +function Seq#Singleton(T) : Seq T; + +axiom (forall t: T :: + { Seq#Length(Seq#Singleton(t)) } + Seq#Length(Seq#Singleton(t)) == 1); + +function Seq#Build(s: Seq T, val: T) : Seq T; + +axiom (forall s: Seq T, v: T :: + { Seq#Length(Seq#Build(s, v)) } + Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s)); + +axiom (forall 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(Seq T, Seq T) : Seq T; + +axiom (forall 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(Seq T, int) : T; + +axiom (forall t: T :: + { Seq#Index(Seq#Singleton(t), 0) } + Seq#Index(Seq#Singleton(t), 0) == t); + +axiom (forall 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(Seq T, int, T) : Seq T; + +axiom (forall 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 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(Seq T, T) : bool; + +axiom (forall 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: T :: + { Seq#Contains(Seq#Empty(), x) } + !Seq#Contains(Seq#Empty(), x)); + +axiom (forall 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 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 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 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(Seq T, Seq T) : bool; + +axiom (forall 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 a: Seq T, b: Seq T :: { Seq#Equal(a, b) } Seq#Equal(a, b) ==> a == b); + +function Seq#SameUntil(Seq T, Seq T, int) : bool; + +axiom (forall 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(s: Seq T, howMany: int) : Seq T; + +axiom (forall 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 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(s: Seq T, howMany: int) : Seq T; + +axiom (forall 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 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 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 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 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 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 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 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 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(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 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 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 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 s: Seq T, n: int :: + { Seq#Drop(s, n) } + n == 0 ==> Seq#Drop(s, n) == s); + +axiom (forall s: Seq T, n: int :: + { Seq#Take(s, n) } + n == 0 ==> Seq#Take(s, n) == Seq#Empty()); + +axiom (forall 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(Map U V) : [U]bool; + +function Map#Elements(Map U V) : [U]V; + +function Map#Card(Map U V) : int; + +axiom (forall m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m)); + +function Map#Empty() : Map U V; + +axiom (forall u: U :: + { Map#Domain(Map#Empty(): Map U V)[u] } + !Map#Domain(Map#Empty(): Map U V)[u]); + +axiom (forall 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]bool, [U]V, Ty) : Map U V; + +axiom (forall 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 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 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(Map U V, U, V) : Map U V; + +axiom (forall 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 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 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(Map U V, Map U V) : bool; + +axiom (forall 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 m: Map U V, m': Map U V :: + { Map#Equal(m, m') } + Map#Equal(m, m') ==> m == m'); + +function Map#Disjoint(Map U V, Map U V) : bool; + +axiom (forall 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(IMap U V) : [U]bool; + +function IMap#Elements(IMap U V) : [U]V; + +function IMap#Empty() : IMap U V; + +axiom (forall u: U :: + { IMap#Domain(IMap#Empty(): IMap U V)[u] } + !IMap#Domain(IMap#Empty(): IMap U V)[u]); + +function IMap#Glue([U]bool, [U]V, Ty) : IMap U V; + +axiom (forall 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 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 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(IMap U V, U, V) : IMap U V; + +axiom (forall 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(IMap U V, IMap U V) : bool; + +axiom (forall 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 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 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 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 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 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 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 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: [ref,Field beta]bool; + + // AddMethodImpl: test, CheckWellformed$$_module.__default.test + $_Frame := (lambda $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 $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 $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 $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 $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: [ref,Field beta]bool; + + // AddMethodImpl: test, Impl$$_module.__default.test + $_Frame := (lambda $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 -- cgit v1.2.3