From 60208673a25423e378cc7e9672d5acf9fd6f58bc Mon Sep 17 00:00:00 2001 From: Dan Rosén Date: Mon, 7 Jul 2014 15:09:33 -0700 Subject: New logical encoding of types with Is and IsAlloc --- Binaries/DafnyPrelude.bpl | 908 ++++++++++++++++++++++++++++------------------ 1 file changed, 548 insertions(+), 360 deletions(-) (limited to 'Binaries/DafnyPrelude.bpl') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 224c5ffd..adb9f043 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -2,11 +2,63 @@ // Created 9 February 2008 by Rustan Leino. // Converted to Boogie 2 on 28 June 2008. // Edited sequence axioms 20 October 2009 by Alex Summers. -// Copyright (c) 2008-2010, Microsoft. +// Modified 2014 by Dan Rosen. +// Copyright (c) 2008-2014, Microsoft. const $$Language$Dafny: bool; // To be recognizable to the ModelViewer as axiom $$Language$Dafny; // coming from a Dafny program. +// --------------------------------------------------------------- +// -- Types ------------------------------------------------------ +// --------------------------------------------------------------- + +type Ty; + +const unique TBool : Ty; +const unique TInt : Ty; +const unique TNat : Ty; +const unique TReal : Ty; +function TSet(Ty) : Ty; +function TMultiSet(Ty) : Ty; +function TSeq(Ty) : Ty; +function TMap(Ty, Ty) : Ty; + +function Inv0_TSet(Ty) : Ty; +axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(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, u: Ty :: { TMap(t,u) } Inv0_TMap(TMap(t,u)) == t); +axiom (forall t, u: Ty :: { TMap(t,u) } Inv1_TMap(TMap(t,u)) == u); + +// -- Classes and Datatypes -- + +// -- Type Tags -- +type TyTag; +function Tag(Ty) : TyTag; + +const unique TagBool : TyTag; +const unique TagInt : TyTag; +const unique TagNat : TyTag; +const unique TagReal : TyTag; +const unique TagSet : TyTag; +const unique TagMultiSet : TyTag; +const unique TagSeq : TyTag; +const unique TagMap : TyTag; +const unique TagClass : TyTag; + +axiom Tag(TBool) == TagBool; +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 :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet); +axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq); +axiom (forall t, u: Ty :: { TMap(t,u) } Tag(TMap(t,u)) == TagMap); + // --------------------------------------------------------------- // -- Literals --------------------------------------------------- // --------------------------------------------------------------- @@ -20,6 +72,429 @@ axiom (forall x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) ); type ref; const null: ref; +// --------------------------------------------------------------- +// -- Boxing and unboxing ---------------------------------------- +// --------------------------------------------------------------- + +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 b: Box :: { $Unbox(b): int } $Box($Unbox(b): int) == b); +axiom (forall b: Box :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b); +axiom (forall b: Box :: { $Unbox(b): Set Box } $Box($Unbox(b): Set Box) == b); +axiom (forall b: Box :: { $Unbox(b): MultiSet Box } $Box($Unbox(b): MultiSet Box) == b); +axiom (forall b: Box :: { $Unbox(b): Seq Box } $Box($Unbox(b): Seq Box) == b); +axiom (forall b: Box :: { $Unbox(b): Map Box Box } $Box($Unbox(b): Map Box Box) == b); +axiom (forall b: Box :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b); +// Note: an axiom like this for bool would not be sound; instead, we do: +function $IsCanonicalBoolBox(Box): bool; +axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true)); +axiom (forall b: Box :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b); +*/ + +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, 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, 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 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) )); + +// The following functions and axioms are used to obtain a $Box($Unbox(_)) wrapper around +// certain expressions. Note that it assumes any booleans (or, indeed, values of any type) contained +// in the (multi)set are canonical (which is the case for any (multi)set that occurs in an execution of +// a Dafny program). +// The role of the parameter 'dummy' in the following is (an unfortunately clumsy construction +// whose only purpose is) simply to tell Boogie how to instantiate the type parameter 'T'. + +/* +function $IsGoodSet_Extended(s: Set Box, dummy: T): bool; +axiom (forall ss: Set Box, dummy: T, bx: Box :: { $IsGoodSet_Extended(ss, dummy), ss[bx] } + $IsGoodSet_Extended(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx): T)); +function $IsGoodMultiSet_Extended(ms: MultiSet Box, dummy: T): bool; +axiom (forall ms: MultiSet Box, dummy: T, bx: Box :: { $IsGoodMultiSet_Extended(ms, dummy), ms[bx] } + $IsGoodMultiSet_Extended(ms, dummy) ==> 0 < ms[bx] ==> bx == $Box($Unbox(bx): T)); + */ + +// --------------------------------------------------------------- +// -- Is and IsAlloc --------------------------------------------- +// --------------------------------------------------------------- + +// Type-argument to $Is is the /representation type/, +// the second value argument to $Is is the actual type. +function $Is(T,Ty): bool; // no heap for now +function $IsAlloc(T,Ty,Heap): bool; + +// Corresponding entries for boxes... +// This could probably be solved by having Box also inhabit Ty +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 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 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: 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: 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))); + +// --------------------------------------------------------------- +// -- Encoding of type names ------------------------------------- +// --------------------------------------------------------------- + +type ClassName; +const unique class._System.int: ClassName; +const unique class._System.bool: ClassName; +const unique class._System.set: ClassName; +const unique class._System.seq: ClassName; +const unique class._System.multiset: ClassName; + +function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty +// function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName; + +function TypeTuple(a: ClassName, b: ClassName): ClassName; +function TypeTupleCar(ClassName): ClassName; +function TypeTupleCdr(ClassName): ClassName; +// TypeTuple is injective in both arguments: +axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } + TypeTupleCar(TypeTuple(a,b)) == a && + TypeTupleCdr(TypeTuple(a,b)) == b); + +// --------------------------------------------------------------- +// -- Datatypes -------------------------------------------------- +// --------------------------------------------------------------- + +type DatatypeType; + +// function /*{:never_pattern true}*/ DtType(DatatypeType): Ty; // the analog of dtype for datatype values + // changed from ClassName to Ty +// function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName; // the analog of TypeParams + +type DtCtorId; +function DatatypeCtorId(DatatypeType): DtCtorId; + +function DtRank(DatatypeType): int; + +// --------------------------------------------------------------- +// -- Axiom contexts --------------------------------------------- +// --------------------------------------------------------------- + +// used to make sure function axioms are not used while their consistency is being checked +const $ModuleContextHeight: int; +const $FunctionContextHeight: int; + +// --------------------------------------------------------------- +// -- Layers of function encodings ------------------------------- +// --------------------------------------------------------------- + +type LayerType; +const $LZ: LayerType; +function $LS(LayerType): LayerType; + +// --------------------------------------------------------------- +// -- Fields ----------------------------------------------------- +// --------------------------------------------------------------- + +type Field alpha; + +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; + +// --------------------------------------------------------------- +// -- Allocatedness and Heap Succession -------------------------- +// --------------------------------------------------------------- + + +// $IsAlloc and $IsAllocBox are monotonic + +axiom(forall h, 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, k : Heap, bx : Box, t : Ty :: + { $HeapSucc(h, k), $IsAllocBox(bx, t, h) } + $HeapSucc(h, k) ==> $IsAllocBox(bx, t, h) ==> $IsAllocBox(bx, t, k)); + +// No axioms for $Is and $IsBox since they don't talk about the heap. + +const unique alloc: Field bool; +axiom FDim(alloc) == 0 && !$IsGhostField(alloc); // treat as non-ghost field, because it cannot be changed by ghost code + +// DtAlloc, removed +//function DtAlloc(DatatypeType, Heap): bool; +//axiom (forall h, k: Heap, d: DatatypeType :: +// { $HeapSucc(h, k), DtAlloc(d, h) } +// $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k)); + +// GenericAlloc removed. + +/* +function GenericAlloc(Box, Heap): bool; +axiom (forall h: Heap, k: Heap, d: Box :: + { $HeapSucc(h, k), GenericAlloc(d, h) } + $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k)); +// GenericAlloc ==> +//references +axiom (forall b: Box, h: Heap :: + { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] } + GenericAlloc(b, h) ==> + $Unbox(b): ref == null || h[$Unbox(b): ref, alloc]); +//seqs +axiom (forall b: Box, h: Heap, i: int :: + { GenericAlloc(b, h), Seq#Index($Unbox(b): Seq Box, i) } + GenericAlloc(b, h) && + 0 <= i && i < Seq#Length($Unbox(b): Seq Box) ==> + GenericAlloc( Seq#Index($Unbox(b): Seq Box, i), h ) ); + +//maps +//seq-like axiom, talking about the range elements +axiom (forall b: Box, h: Heap, i: Box :: + { GenericAlloc(b, h), Map#Domain($Unbox(b): Map Box Box)[i] } + GenericAlloc(b, h) && Map#Domain($Unbox(b): Map Box Box)[i] ==> + GenericAlloc( Map#Elements($Unbox(b): Map Box Box)[i], h ) ); +//set-like axiom, talking about the domain elements +axiom (forall b: Box, h: Heap, t: Box :: + { GenericAlloc(b, h), Map#Domain($Unbox(b): Map Box Box)[t] } + GenericAlloc(b, h) && Map#Domain($Unbox(b): Map Box Box)[t] ==> + GenericAlloc(t, h)); + +//sets +axiom (forall b: Box, h: Heap, t: Box :: + { GenericAlloc(b, h), ($Unbox(b): Set Box)[t] } + GenericAlloc(b, h) && ($Unbox(b): Set Box)[t] ==> + GenericAlloc(t, h)); +//datatypes +axiom (forall b: Box, h: Heap :: + { GenericAlloc(b, h), DtAlloc($Unbox(b): DatatypeType, h) } + GenericAlloc(b, h) <==> DtAlloc($Unbox(b): DatatypeType, h)); +axiom (forall dt: DatatypeType, h: Heap :: + { GenericAlloc($Box(dt), h) } + GenericAlloc($Box(dt), h) <==> DtAlloc(dt, h)); +// ==> GenericAlloc +axiom (forall b: bool, h: Heap :: + $IsGoodHeap(h) ==> GenericAlloc($Box(b), h)); +axiom (forall x: int, h: Heap :: + $IsGoodHeap(h) ==> GenericAlloc($Box(x), h)); +axiom (forall r: ref, h: Heap :: + { GenericAlloc($Box(r), h) } + $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h)); +// boxes in the heap +axiom (forall r: ref, f: Field Box, h: Heap :: + { GenericAlloc(read(h, r, f), h) } + $IsGoodHeap(h) && r != null && read(h, r, alloc) ==> + GenericAlloc(read(h, r, f), h)); + +axiom (forall h: Heap, r: ref, j: int :: + { read(h, r, IndexField(j)) } + $IsGoodHeap(h) && r != null && read(h, r, alloc) && + 0 <= j && j < _System.array.Length(r) + ==> + GenericAlloc(read(h, r, IndexField(j)), h)); +axiom (forall h: Heap, r: ref, m: Field Box, j: int :: + { read(h, r, MultiIndexField(m, j)) } + $IsGoodHeap(h) && r != null && read(h, r, alloc) + // It would be best also to constrain MultiIndexField(m,j) to produce + // a proper field (that is, to refer to an array element within + // bounds. However, since the LengthX fields of multi-dimentional + // are produced on the fly, adding them would require more work. + // Thus, the model to keep in mind is that MultiIndexField then + // produces a field who value, when dereferenced for array 'r', + // is a box that has the desired allocation properties. + ==> + GenericAlloc(read(h, r, MultiIndexField(m, j)), h)); + */ + + +// --------------------------------------------------------------- +// -- Arrays ----------------------------------------------------- +// --------------------------------------------------------------- + +function _System.array.Length(a: ref): int; +axiom (forall o: ref :: 0 <= _System.array.Length(o)); + +// --------------------------------------------------------------- +// -- Reals ------------------------------------------------------ +// --------------------------------------------------------------- + +function _System.Real.RealToInt(h: Heap, x: real): int { int(x) } +function _System.Real.IntToReal(h: Heap, x: int): real { real(x) } + +// --------------------------------------------------------------- +// -- The heap --------------------------------------------------- +// --------------------------------------------------------------- + +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; +var $Heap: Heap where $IsGoodHeap($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,b,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))); + +// --------------------------------------------------------------- +// -- Non-determinism -------------------------------------------- +// --------------------------------------------------------------- + +type TickType; +var $Tick: TickType; + +// --------------------------------------------------------------- +// -- Useful macros ---------------------------------------------- +// --------------------------------------------------------------- + +// havoc everything in $Heap, except {this}+rds+nw +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); + +// havoc everything in $Heap, except rds-modi-{this} +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); + +// havoc $Heap at {this}+modi+nw +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))); + +// --------------------------------------------------------------- +// -- Axiomatizations -------------------------------------------- +// --------------------------------------------------------------- + // --------------------------------------------------------------- // -- Axiomatization of sets ------------------------------------- // --------------------------------------------------------------- @@ -35,11 +510,18 @@ axiom (forall s: Set T :: { Set#Card(s) } (Set#Card(s) == 0 <==> s == Set#Empty()) && (Set#Card(s) != 0 ==> (exists x: T :: s[x]))); +// the empty set could be of anything +//axiom (forall t: Ty :: { $Is(Set#Empty() : [T]bool, TSet(t)) } $Is(Set#Empty() : [T]bool, TSet(t))); + 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); +// the singleton set will be the same type as its box +//axiom (forall bx : Ty, t: Ty :: { $Is(Set#Singleton( + + 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]); @@ -48,9 +530,9 @@ axiom (forall a: Set T, x: T :: { Set#UnionOne(a, 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)); + 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); + !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] } @@ -90,7 +572,7 @@ axiom (forall a, b: Set T, y: T :: { Set#Difference(a, b), b[y] } b[y] ==> !Set#Difference(a, b)[y] ); axiom (forall a, b: Set T :: { Set#Card(Set#Difference(a, b)) } - Set#Card(Set#Difference(a, b)) + Set#Card(Set#Difference(b, a)) + 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))); @@ -101,7 +583,7 @@ axiom(forall a: Set T, b: Set T :: { Set#Subset(a,b) } // axiom(forall a: Set T, b: Set T :: // { Set#Subset(a,b), Set#Card(a), Set#Card(b) } // very restrictive trigger // Set#Subset(a,b) ==> Set#Card(a) <= Set#Card(b)); - + function Set#Equal(Set T, Set T): bool; axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) } @@ -130,11 +612,11 @@ type MultiSet T = [T]int; function $IsGoodMultiSet(ms: MultiSet T): bool; // ints are non-negative, used after havocing, and for conversion from sequences to multisets. -axiom (forall ms: MultiSet T :: { $IsGoodMultiSet(ms) } +axiom (forall ms: MultiSet T :: { $IsGoodMultiSet(ms) } $IsGoodMultiSet(ms) <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx])); function MultiSet#Card(MultiSet T): int; -axiom (forall s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s)); +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); @@ -163,8 +645,8 @@ axiom (forall a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[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); - + MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1); + function MultiSet#Union(MultiSet T, MultiSet T): MultiSet T; // union-ing is the sum of the contents @@ -172,7 +654,7 @@ 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])); @@ -191,7 +673,7 @@ axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), b[y], a[ a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0 ); axiom (forall a, b: MultiSet T :: { MultiSet#Card(MultiSet#Difference(a, b)) } - MultiSet#Card(MultiSet#Difference(a, b)) + MultiSet#Card(MultiSet#Difference(b, a)) + 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))); @@ -218,7 +700,7 @@ 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)); + MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s)); // conversion to a multiset, from a sequence. function MultiSet#FromSeq(Seq T): MultiSet T; @@ -245,7 +727,7 @@ axiom (forall s: Seq T, i: int, v: T, x: T :: // i.e. MS(Update(s, i, v)) == MS(s) - {{s[i]}} + {{v}} 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] ); - + // --------------------------------------------------------------- // -- Axiomatization of sequences -------------------------------- // --------------------------------------------------------------- @@ -259,6 +741,9 @@ 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()); +// The empty sequence $Is any type +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); @@ -269,10 +754,18 @@ 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))); +// Build preserves $Is +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)); +// Append preserves $Is +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) } @@ -352,20 +845,20 @@ axiom (forall s, t: Seq T :: Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s && Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t); -function Seq#FromArray(h: HeapType, a: ref): Seq BoxType; -axiom (forall h: HeapType, a: ref :: +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: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType } +axiom (forall h: Heap, a: ref :: { Seq#FromArray(h,a): Seq Box } (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)))); -axiom (forall h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref :: +axiom (forall h: Heap, o: ref, f: Field alpha, v: alpha, a: ref :: { Seq#FromArray(update(h, o, f, v), a) } o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) ); -axiom (forall h: HeapType, i: int, v: BoxType, a: ref :: +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) ); /**** Someday: -axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) } +axiom (forall h: Heap, a: ref :: { Seq#FromArray(h, a) } $IsGoodHeap(h) && a != null && read(h, a, alloc) && dtype(a) == class._System.array && TypeParams(a, 0) == class._System.bool ==> @@ -375,48 +868,48 @@ axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) } // Commutability of Take and Drop with Update. 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) ); + { 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)); + { 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) ); + { 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)); + { Seq#Drop(Seq#Update(s, i, v), n) } + 0 <= i && i < n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n)); // Extension axiom, triggers only on Takes from arrays. -axiom (forall h: HeapType, a: ref, n0, n1: int :: - { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } - n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) ); +axiom (forall h: Heap, a: ref, n0, n1: int :: + { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } + n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field Box)) ); // drop commutes with build. 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) ); + { 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 BoxType, 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 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) ); + { 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) ); + { 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) ); + { 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) ); // Additional axioms about common things axiom (forall s: Seq T, n: int :: { Seq#Drop(s, n) } - n == 0 ==> Seq#Drop(s, n) == s); + 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()); + n == 0 ==> Seq#Take(s, n) == Seq#Empty()); axiom (forall s: Seq T, m, 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)); + 0 <= m && 0 <= n && m+n <= Seq#Length(s) ==> + Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m+n)); // --------------------------------------------------------------- // -- Axiomatization of Maps ------------------------------------- @@ -428,21 +921,21 @@ 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)); +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]); + { 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()); function Map#Glue([U] bool, [U]V): Map U V; axiom (forall a: [U] bool, b:[U]V :: - { Map#Domain(Map#Glue(a, b)) } - Map#Domain(Map#Glue(a, b)) == a); + { Map#Domain(Map#Glue(a, b)) } + Map#Domain(Map#Glue(a, b)) == a); axiom (forall a: [U] bool, b:[U]V :: - { Map#Elements(Map#Glue(a, b)) } - Map#Elements(Map#Glue(a, b)) == b); + { Map#Elements(Map#Glue(a, b)) } + Map#Elements(Map#Glue(a, b)) == b); //Build is used in displays, and for map updates @@ -458,10 +951,10 @@ axiom (forall m: Map U V, u: U, u': U, v: 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)); + 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); - + !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1); + //equality for maps function Map#Equal(Map U V, Map U V): bool; @@ -479,308 +972,3 @@ 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])); -// --------------------------------------------------------------- -// -- Boxing and unboxing ---------------------------------------- -// --------------------------------------------------------------- - -type BoxType; -const $ArbitraryBoxValue: BoxType; - -function $Box(T): BoxType; -function $Unbox(BoxType): T; - -axiom (forall x: T :: { $Box(x) } $Unbox($Box(x)) == x); -axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b); -axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b); -axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b); -axiom (forall b: BoxType :: { $Unbox(b): MultiSet BoxType } $Box($Unbox(b): MultiSet BoxType) == b); -axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b); -axiom (forall b: BoxType :: { $Unbox(b): Map BoxType BoxType } $Box($Unbox(b): Map BoxType BoxType) == b); -axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b); -// Note: an axiom like this for bool would not be sound; instead, we do: -function $IsCanonicalBoolBox(BoxType): bool; -axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true)); -axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b); - -// The following functions and axioms are used to obtain a $Box($Unbox(_)) wrapper around -// certain expressions. Note that it assumes any booleans (or, indeed, values of any type) contained -// in the (multi)set are canonical (which is the case for any (multi)set that occurs in an execution of -// a Dafny program). -// The role of the parameter 'dummy' in the following is (an unfortunately clumsy construction -// whose only purpose is) simply to tell Boogie how to instantiate the type parameter 'T'. -function $IsGoodSet_Extended(s: Set BoxType, dummy: T): bool; -axiom (forall ss: Set BoxType, dummy: T, bx: BoxType :: { $IsGoodSet_Extended(ss, dummy), ss[bx] } - $IsGoodSet_Extended(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx): T)); -function $IsGoodMultiSet_Extended(ms: MultiSet BoxType, dummy: T): bool; -axiom (forall ms: MultiSet BoxType, dummy: T, bx: BoxType :: { $IsGoodMultiSet_Extended(ms, dummy), ms[bx] } - $IsGoodMultiSet_Extended(ms, dummy) ==> 0 < ms[bx] ==> bx == $Box($Unbox(bx): T)); - -// --------------------------------------------------------------- -// -- Encoding of type names ------------------------------------- -// --------------------------------------------------------------- - -type ClassName; -const unique class._System.int: ClassName; -const unique class._System.bool: ClassName; -const unique class._System.set: ClassName; -const unique class._System.seq: ClassName; -const unique class._System.multiset: ClassName; -const unique class._System.array: ClassName; - -function /*{:never_pattern true}*/ dtype(ref): ClassName; -function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName; - -function TypeTuple(a: ClassName, b: ClassName): ClassName; -function TypeTupleCar(ClassName): ClassName; -function TypeTupleCdr(ClassName): ClassName; -// TypeTuple is injective in both arguments: -axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } - TypeTupleCar(TypeTuple(a,b)) == a && - TypeTupleCdr(TypeTuple(a,b)) == b); - -// --------------------------------------------------------------- -// -- Datatypes -------------------------------------------------- -// --------------------------------------------------------------- - -type DatatypeType; - -function /*{:never_pattern true}*/ DtType(DatatypeType): ClassName; // the analog of dtype for datatype values -function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName; // the analog of TypeParams - -type DtCtorId; -function DatatypeCtorId(DatatypeType): DtCtorId; - -function DtRank(DatatypeType): int; - -// --------------------------------------------------------------- -// -- Axiom contexts --------------------------------------------- -// --------------------------------------------------------------- - -// used to make sure function axioms are not used while their consistency is being checked -const $ModuleContextHeight: int; -const $FunctionContextHeight: int; - -// --------------------------------------------------------------- -// -- Layers of function encodings ------------------------------- -// --------------------------------------------------------------- - -type LayerType; -const $LZ: LayerType; -function $LS(LayerType): LayerType; - -// --------------------------------------------------------------- -// -- Fields ----------------------------------------------------- -// --------------------------------------------------------------- - -type Field alpha; - -function FDim(Field T): int; - -function IndexField(int): Field BoxType; -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 BoxType, int): Field BoxType; -axiom (forall f: Field BoxType, 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 BoxType, i: int :: { MultiIndexField(f,i) } - MultiIndexField_Inverse0(MultiIndexField(f,i)) == f && - MultiIndexField_Inverse1(MultiIndexField(f,i)) == i); - -axiom (forall h: HeapType, a: ref, j: int :: - { $Unbox(read(h, a, IndexField(j))) : ref } - $IsGoodHeap(h) && - a != null && read(h, a, alloc) && - 0 <= j && j < _System.array.Length(a) - // It would be nice also to restrict this axiom to an 'a' whose type is - // really a reference type. - ==> - $Unbox(read(h, a, IndexField(j))) : ref == null || - dtype($Unbox(read(h, a, IndexField(j))) : ref) == TypeParams(a, 0)); - -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; - -// --------------------------------------------------------------- -// -- Allocatedness ---------------------------------------------- -// --------------------------------------------------------------- - -const unique alloc: Field bool; -axiom FDim(alloc) == 0 && !$IsGhostField(alloc); // treat as non-ghost field, because it cannot be changed by ghost code - -function DtAlloc(DatatypeType, HeapType): bool; -axiom (forall h, k: HeapType, d: DatatypeType :: - { $HeapSucc(h, k), DtAlloc(d, h) } - $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k)); - -function GenericAlloc(BoxType, HeapType): bool; -axiom (forall h: HeapType, k: HeapType, d: BoxType :: - { $HeapSucc(h, k), GenericAlloc(d, h) } - $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k)); -// GenericAlloc ==> -//references -axiom (forall b: BoxType, h: HeapType :: - { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] } - GenericAlloc(b, h) ==> - $Unbox(b): ref == null || h[$Unbox(b): ref, alloc]); -//seqs -axiom (forall b: BoxType, h: HeapType, i: int :: - { GenericAlloc(b, h), Seq#Index($Unbox(b): Seq BoxType, i) } - GenericAlloc(b, h) && - 0 <= i && i < Seq#Length($Unbox(b): Seq BoxType) ==> - GenericAlloc( Seq#Index($Unbox(b): Seq BoxType, i), h ) ); - -//maps -//seq-like axiom, talking about the range elements -axiom (forall b: BoxType, h: HeapType, i: BoxType :: - { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[i] } - GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[i] ==> - GenericAlloc( Map#Elements($Unbox(b): Map BoxType BoxType)[i], h ) ); -//set-like axiom, talking about the domain elements -axiom (forall b: BoxType, h: HeapType, t: BoxType :: - { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[t] } - GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[t] ==> - GenericAlloc(t, h)); - -//sets -axiom (forall b: BoxType, h: HeapType, t: BoxType :: - { GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] } - GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==> - GenericAlloc(t, h)); -//datatypes -axiom (forall b: BoxType, h: HeapType :: - { GenericAlloc(b, h), DtAlloc($Unbox(b): DatatypeType, h) } - GenericAlloc(b, h) <==> DtAlloc($Unbox(b): DatatypeType, h)); -axiom (forall dt: DatatypeType, h: HeapType :: - { GenericAlloc($Box(dt), h) } - GenericAlloc($Box(dt), h) <==> DtAlloc(dt, h)); -// ==> GenericAlloc -axiom (forall b: bool, h: HeapType :: - $IsGoodHeap(h) ==> GenericAlloc($Box(b), h)); -axiom (forall x: int, h: HeapType :: - $IsGoodHeap(h) ==> GenericAlloc($Box(x), h)); -axiom (forall r: ref, h: HeapType :: - { GenericAlloc($Box(r), h) } - $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h)); -// boxes in the heap -axiom (forall r: ref, f: Field BoxType, h: HeapType :: - { GenericAlloc(read(h, r, f), h) } - $IsGoodHeap(h) && r != null && read(h, r, alloc) ==> - GenericAlloc(read(h, r, f), h)); - -axiom (forall h: HeapType, r: ref, j: int :: - { read(h, r, IndexField(j)) } - $IsGoodHeap(h) && r != null && read(h, r, alloc) && - 0 <= j && j < _System.array.Length(r) - ==> - GenericAlloc(read(h, r, IndexField(j)), h)); -axiom (forall h: HeapType, r: ref, m: Field BoxType, j: int :: - { read(h, r, MultiIndexField(m, j)) } - $IsGoodHeap(h) && r != null && read(h, r, alloc) - // It would be best also to constrain MultiIndexField(m,j) to produce - // a proper field (that is, to refer to an array element within - // bounds. However, since the LengthX fields of multi-dimentional - // are produced on the fly, adding them would require more work. - // Thus, the model to keep in mind is that MultiIndexField then - // produces a field who value, when dereferenced for array 'r', - // is a box that has the desired allocation properties. - ==> - GenericAlloc(read(h, r, MultiIndexField(m, j)), h)); - - -// --------------------------------------------------------------- -// -- Arrays ----------------------------------------------------- -// --------------------------------------------------------------- - -function _System.array.Length(a: ref): int; -axiom (forall o: ref :: 0 <= _System.array.Length(o)); - -// --------------------------------------------------------------- -// -- Reals ------------------------------------------------------ -// --------------------------------------------------------------- - -function _System.Real.RealToInt(h: HeapType, x: real): int { int(x) } -function _System.Real.IntToReal(h: HeapType, x: int): real { real(x) } - -// --------------------------------------------------------------- -// -- The heap --------------------------------------------------- -// --------------------------------------------------------------- - -type HeapType = [ref,Field alpha]alpha; -function {:inline true} read(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] } -function {:inline true} update(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] } - -function $IsGoodHeap(HeapType): bool; -var $Heap: HeapType where $IsGoodHeap($Heap); - -function $HeapSucc(HeapType, HeapType): bool; -axiom (forall h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) } - $IsGoodHeap(update(h, r, f, x)) ==> - $HeapSucc(h, update(h, r, f, x))); -axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) } - $HeapSucc(a,b) && $HeapSucc(b,c) ==> $HeapSucc(a,c)); -axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) } - $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc))); - -function $HeapSuccGhost(HeapType, HeapType): bool; -axiom (forall h: HeapType, k: HeapType :: { $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))); - -// --------------------------------------------------------------- -// -- Non-determinism -------------------------------------------- -// --------------------------------------------------------------- - -type TickType; -var $Tick: TickType; - -// --------------------------------------------------------------- -// -- Useful macros ---------------------------------------------- -// --------------------------------------------------------------- - -// havoc everything in $Heap, except {this}+rds+nw -procedure $YieldHavoc(this: ref, rds: Set BoxType, nw: Set BoxType); - 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); - -// havoc everything in $Heap, except rds-modi-{this} -procedure $IterHavoc0(this: ref, rds: Set BoxType, modi: Set BoxType); - 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); - -// havoc $Heap at {this}+modi+nw -procedure $IterHavoc1(this: ref, modi: Set BoxType, nw: Set BoxType); - 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: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType)) - returns (s: Set BoxType); - ensures (forall bx: BoxType :: { s[bx] } s[bx] <==> - read(newHeap, this, NW)[bx] || - ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc))); - -// --------------------------------------------------------------- -- cgit v1.2.3