From 62f42e257fd72498e692c7ce8aaee339ad5322e6 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 26 Feb 2016 11:06:11 -0800 Subject: Fix test failure. Print the resulting boogie code to a file instead of console. --- Test/dafny4/Bug136.dfy | 2 +- Test/dafny4/Bug136.dfy.expect | 1770 ----------------------------------------- 2 files changed, 1 insertion(+), 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(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