summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl908
1 files changed, 548 insertions, 360 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 224c5ffd..adb9f043 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -2,12 +2,64 @@
// 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 ---------------------------------------------------
// ---------------------------------------------------------------
function {:identity} Lit<T>(x: T): T { x }
@@ -21,6 +73,429 @@ type ref;
const null: ref;
// ---------------------------------------------------------------
+// -- Boxing and unboxing ----------------------------------------
+// ---------------------------------------------------------------
+
+type Box;
+const $ArbitraryBoxValue: Box;
+
+function $Box<T>(T): Box;
+function $Unbox<T>(Box): T;
+
+/*
+axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
+axiom (forall 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<T> x : T :: { $Box(x) } $Unbox($Box(x)) == x);
+
+axiom (forall bx : Box ::
+ { $IsBox(bx, TInt) }
+ ( $IsBox(bx, TInt) ==> $Box($Unbox(bx) : int) == bx && $Is($Unbox(bx) : int, TInt)));
+axiom (forall bx : Box ::
+ { $IsBox(bx, TNat) }
+ ( $IsBox(bx, TNat) ==> $Box($Unbox(bx) : int) == bx && $Is($Unbox(bx) : int, TNat)));
+axiom (forall bx : Box ::
+ { $IsBox(bx, TReal) }
+ ( $IsBox(bx, TReal) ==> $Box($Unbox(bx) : real) == bx && $Is($Unbox(bx) : real, TReal)));
+axiom (forall bx : Box ::
+ { $IsBox(bx, TBool) }
+ ( $IsBox(bx, TBool) ==> $Box($Unbox(bx) : bool) == bx && $Is($Unbox(bx) : bool, TBool)));
+axiom (forall bx : Box, 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<T> v : T, t : Ty ::
+ { $IsBox($Box(v), t) }
+ ( $IsBox($Box(v), t) <==> $Is(v,t) ));
+axiom (forall<T> v : T, t : Ty, h : Heap ::
+ { $IsAllocBox($Box(v), t, h) }
+ ( $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v,t,h) ));
+
+// 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<T>(s: Set Box, dummy: T): bool;
+axiom (forall<T> 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<T>(ms: MultiSet Box, dummy: T): bool;
+axiom (forall<T> 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>(T,Ty): bool; // no heap for now
+function $IsAlloc<T>(T,Ty,Heap): bool;
+
+// Corresponding entries for boxes...
+// This could probably be solved by having Box also inhabit Ty
+function $IsBox<T>(T,Ty): bool;
+function $IsAllocBox<T>(T,Ty,Heap): bool;
+
+axiom(forall v : int :: { $Is(v,TInt) } $Is(v,TInt));
+axiom(forall v : int :: { $Is(v,TNat) } $Is(v,TNat) <==> v >= 0);
+axiom(forall v : real :: { $Is(v,TReal) } $Is(v,TReal));
+axiom(forall v : bool :: { $Is(v,TBool) } $Is(v,TBool));
+
+axiom(forall 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<T>(Field T): int;
+
+function IndexField(int): Field Box;
+axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);
+function IndexField_Inverse<T>(Field T): int;
+axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);
+
+function MultiIndexField(Field Box, int): Field Box;
+axiom (forall f: Field Box, i: int :: { MultiIndexField(f,i) } FDim(MultiIndexField(f,i)) == FDim(f) + 1);
+function MultiIndexField_Inverse0<T>(Field T): Field T;
+function MultiIndexField_Inverse1<T>(Field T): int;
+axiom (forall f: Field Box, i: int :: { MultiIndexField(f,i) }
+ MultiIndexField_Inverse0(MultiIndexField(f,i)) == f &&
+ MultiIndexField_Inverse1(MultiIndexField(f,i)) == i);
+
+function DeclType<T>(Field T): ClassName;
+
+type NameFamily;
+function DeclName<T>(Field T): NameFamily;
+function FieldOfDecl<alpha>(ClassName, NameFamily): Field alpha;
+axiom (forall<T> cl : ClassName, nm: NameFamily ::
+ {FieldOfDecl(cl, nm): Field T}
+ DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm);
+
+function $IsGhostField<T>(Field T): bool;
+
+// ---------------------------------------------------------------
+// -- Allocatedness and Heap Succession --------------------------
+// ---------------------------------------------------------------
+
+
+// $IsAlloc and $IsAllocBox are monotonic
+
+axiom(forall<T> 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 = <alpha>[ref,Field alpha]alpha;
+function {:inline true} read<alpha>(H:Heap, r:ref, f:Field alpha): alpha { H[r, f] }
+function {:inline true} update<alpha>(H:Heap, r:ref, f:Field alpha, v:alpha): Heap { H[r,f := v] }
+
+function $IsGoodHeap(Heap): bool;
+var $Heap: Heap where $IsGoodHeap($Heap);
+
+function $HeapSucc(Heap, Heap): bool;
+axiom (forall<alpha> h: Heap, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }
+ $IsGoodHeap(update(h, r, f, x)) ==>
+ $HeapSucc(h, update(h, r, f, x)));
+axiom (forall a,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<alpha> 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<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc) ==>
+ $o == this || rds[$Box($o)] || nw[$Box($o)] ==>
+ read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ ensures $HeapSucc(old($Heap), $Heap);
+
+// havoc everything in $Heap, except rds-modi-{this}
+procedure $IterHavoc0(this: ref, rds: Set Box, modi: Set Box);
+ modifies $Heap;
+ ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc) ==>
+ rds[$Box($o)] && !modi[$Box($o)] && $o != this ==>
+ read($Heap, $o, $f) == read(old($Heap), $o, $f));
+ ensures $HeapSucc(old($Heap), $Heap);
+
+// havoc $Heap at {this}+modi+nw
+procedure $IterHavoc1(this: ref, modi: Set Box, nw: Set Box);
+ modifies $Heap;
+ ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
+ $o != null && read(old($Heap), $o, alloc) ==>
+ read($Heap, $o, $f) == read(old($Heap), $o, $f) ||
+ $o == this || modi[$Box($o)] || nw[$Box($o)]);
+ ensures $HeapSucc(old($Heap), $Heap);
+
+procedure $IterCollectNewObjects(prevHeap: Heap, newHeap: Heap, this: ref, NW: Field (Set Box))
+ returns (s: Set Box);
+ ensures (forall bx: Box :: { s[bx] } s[bx] <==>
+ read(newHeap, this, NW)[bx] ||
+ ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc)));
+
+// ---------------------------------------------------------------
+// -- Axiomatizations --------------------------------------------
+// ---------------------------------------------------------------
+
+// ---------------------------------------------------------------
// -- Axiomatization of sets -------------------------------------
// ---------------------------------------------------------------
@@ -35,11 +510,18 @@ axiom (forall<T> s: Set T :: { Set#Card(s) }
(Set#Card(s) == 0 <==> s == Set#Empty()) &&
(Set#Card(s) != 0 ==> (exists x: T :: s[x])));
+// the empty set could be of anything
+//axiom (forall<T> t: Ty :: { $Is(Set#Empty() : [T]bool, TSet(t)) } $Is(Set#Empty() : [T]bool, TSet(t)));
+
function Set#Singleton<T>(T): Set T;
axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
axiom (forall<T> r: T :: { Set#Card(Set#Singleton(r)) } Set#Card(Set#Singleton(r)) == 1);
+// the singleton set will be the same type as its box
+//axiom (forall bx : Ty, t: Ty :: { $Is(Set#Singleton(
+
+
function Set#UnionOne<T>(Set T, T): Set T;
axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }
Set#UnionOne(a,x)[o] <==> o == x || a[o]);
@@ -48,9 +530,9 @@ axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }
axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }
a[y] ==> Set#UnionOne(a, x)[y]);
axiom (forall<T> a: Set T, x: T :: { Set#Card(Set#UnionOne(a, x)) }
- a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a));
+ a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a));
axiom (forall<T> a: Set T, x: T :: { Set#Card(Set#UnionOne(a, x)) }
- !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1);
+ !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1);
function Set#Union<T>(Set T, Set T): Set T;
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }
@@ -90,7 +572,7 @@ axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }
b[y] ==> !Set#Difference(a, b)[y] );
axiom (forall<T> 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<T> a: Set T, b: Set T :: { Set#Subset(a,b) }
// axiom(forall<T> 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<T>(Set T, Set T): bool;
axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }
@@ -130,11 +612,11 @@ type MultiSet T = [T]int;
function $IsGoodMultiSet<T>(ms: MultiSet T): bool;
// ints are non-negative, used after havocing, and for conversion from sequences to multisets.
-axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) }
+axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) }
$IsGoodMultiSet(ms) <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx]));
function MultiSet#Card<T>(MultiSet T): int;
-axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
+axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
axiom (forall<T> s: MultiSet T, x: T, n: int :: { MultiSet#Card(s[x := n]) }
0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n);
@@ -163,8 +645,8 @@ axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }
axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] }
x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);
axiom (forall<T> a: MultiSet T, x: T :: { MultiSet#Card(MultiSet#UnionOne(a, x)) }
- MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1);
-
+ MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1);
+
function MultiSet#Union<T>(MultiSet T, MultiSet T): MultiSet T;
// union-ing is the sum of the contents
@@ -172,7 +654,7 @@ axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o]
MultiSet#Union(a,b)[o] == a[o] + b[o]);
axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Card(MultiSet#Union(a,b)) }
MultiSet#Card(MultiSet#Union(a,b)) == MultiSet#Card(a) + MultiSet#Card(b));
-
+
function MultiSet#Intersection<T>(MultiSet T, MultiSet T): MultiSet T;
axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] }
MultiSet#Intersection(a,b)[o] == Math#min(a[o], b[o]));
@@ -191,7 +673,7 @@ axiom (forall<T> 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<T> 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<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] }
(MultiSet#FromSet(s)[a] == 0 <==> !s[a]) &&
(MultiSet#FromSet(s)[a] == 1 <==> s[a]));
axiom (forall<T> s: Set T :: { MultiSet#Card(MultiSet#FromSet(s)) }
- MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s));
+ MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s));
// conversion to a multiset, from a sequence.
function MultiSet#FromSeq<T>(Seq T): MultiSet T;
@@ -245,7 +727,7 @@ axiom (forall<T> s: Seq T, i: int, v: T, x: T ::
// i.e. MS(Update(s, i, v)) == MS(s) - {{s[i]}} + {{v}}
axiom (forall<T> s: Seq T, x: T :: { MultiSet#FromSeq(s)[x] }
(exists i : int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && x == Seq#Index(s,i)) <==> 0 < MultiSet#FromSeq(s)[x] );
-
+
// ---------------------------------------------------------------
// -- Axiomatization of sequences --------------------------------
// ---------------------------------------------------------------
@@ -259,6 +741,9 @@ function Seq#Empty<T>(): Seq T;
axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
+// The empty sequence $Is any type
+axiom (forall<T> t: Ty :: {$Is(Seq#Empty(): Seq T, t)} $Is(Seq#Empty(): Seq T, t));
+
function Seq#Singleton<T>(T): Seq T;
axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
@@ -269,10 +754,18 @@ axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Index(Seq#Build(s,v), i) }
(i == Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == v) &&
(i != Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == Seq#Index(s, i)));
+// 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<T>(Seq T, Seq T): Seq T;
axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));
+// 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<T>(Seq T, int): T;
axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);
axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }
@@ -352,20 +845,20 @@ axiom (forall<T> 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<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::
+axiom (forall<alpha> 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<T> s: Seq T, i: int, v: T, n: int ::
- { Seq#Take(Seq#Update(s, i, v), n) }
- 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );
+ { Seq#Take(Seq#Update(s, i, v), n) }
+ 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) );
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
- { Seq#Take(Seq#Update(s, i, v), n) }
- n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));
+ { Seq#Take(Seq#Update(s, i, v), n) }
+ n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
- { Seq#Drop(Seq#Update(s, i, v), n) }
- 0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) );
+ { Seq#Drop(Seq#Update(s, i, v), n) }
+ 0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) );
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
- { Seq#Drop(Seq#Update(s, i, v), n) }
- 0 <= i && i < n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));
+ { 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<T> s: Seq T, v: T, n: int ::
- { Seq#Drop(Seq#Build(s, v), n) }
- 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );
+ { Seq#Drop(Seq#Build(s, v), n) }
+ 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );
function Seq#Rank<T>(Seq T): int;
-axiom (forall s: Seq 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<T> s: Seq T, i: int ::
- { Seq#Rank(Seq#Drop(s, i)) }
- 0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s) );
+ { Seq#Rank(Seq#Drop(s, i)) }
+ 0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s) );
axiom (forall<T> s: Seq T, i: int ::
- { Seq#Rank(Seq#Take(s, i)) }
- 0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s) );
+ { Seq#Rank(Seq#Take(s, i)) }
+ 0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s) );
axiom (forall<T> s: Seq T, i: int, j: int ::
- { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) }
- 0 <= i && i < j && j <= Seq#Length(s) ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s) );
+ { 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<T> 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<T> 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<T> 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<U, V>(Map U V): [U] bool;
function Map#Elements<U, V>(Map U V): [U]V;
function Map#Card<U, V>(Map U V): int;
-axiom (forall<U, V> m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m));
+axiom (forall<U, V> m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m));
function Map#Empty<U, V>(): Map U V;
axiom (forall<U, V> u: U ::
- { Map#Domain(Map#Empty(): Map U V)[u] }
- !Map#Domain(Map#Empty(): Map U V)[u]);
+ { Map#Domain(Map#Empty(): Map U V)[u] }
+ !Map#Domain(Map#Empty(): Map U V)[u]);
axiom (forall<U, V> m: Map U V :: { Map#Card(m) } Map#Card(m) == 0 <==> m == Map#Empty());
function Map#Glue<U, V>([U] bool, [U]V): Map U V;
axiom (forall<U, V> a: [U] bool, b:[U]V ::
- { Map#Domain(Map#Glue(a, b)) }
- Map#Domain(Map#Glue(a, b)) == a);
+ { Map#Domain(Map#Glue(a, b)) }
+ Map#Domain(Map#Glue(a, b)) == a);
axiom (forall<U, V> a: [U] bool, b:[U]V ::
- { Map#Elements(Map#Glue(a, b)) }
- Map#Elements(Map#Glue(a, b)) == b);
+ { 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<U, V> 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<U, V> m: Map U V, u: U, v: V :: { Map#Card(Map#Build(m, u, v)) }
- Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m));
+ Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m));
axiom (forall<U, V> m: Map U V, u: U, v: V :: { Map#Card(Map#Build(m, u, v)) }
- !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1);
-
+ !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1);
+
//equality for maps
function Map#Equal<U, V>(Map U V, Map U V): bool;
@@ -479,308 +972,3 @@ axiom (forall<U, V> m: Map U V, m': Map U V ::
{ Map#Disjoint(m, m') }
Map#Disjoint(m, m') <==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o]));
-// ---------------------------------------------------------------
-// -- Boxing and unboxing ----------------------------------------
-// ---------------------------------------------------------------
-
-type BoxType;
-const $ArbitraryBoxValue: BoxType;
-
-function $Box<T>(T): BoxType;
-function $Unbox<T>(BoxType): T;
-
-axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
-axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);
-axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
-axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
-axiom (forall b: BoxType :: { $Unbox(b): 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<T>(s: Set BoxType, dummy: T): bool;
-axiom (forall<T> 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<T>(ms: MultiSet BoxType, dummy: T): bool;
-axiom (forall<T> 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<T>(Field T): int;
-
-function IndexField(int): Field BoxType;
-axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);
-function IndexField_Inverse<T>(Field T): int;
-axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);
-
-function MultiIndexField(Field BoxType, int): Field BoxType;
-axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } FDim(MultiIndexField(f,i)) == FDim(f) + 1);
-function MultiIndexField_Inverse0<T>(Field T): Field T;
-function MultiIndexField_Inverse1<T>(Field T): int;
-axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }
- MultiIndexField_Inverse0(MultiIndexField(f,i)) == f &&
- MultiIndexField_Inverse1(MultiIndexField(f,i)) == i);
-
-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<T>(Field T): ClassName;
-
-type NameFamily;
-function DeclName<T>(Field T): NameFamily;
-function FieldOfDecl<alpha>(ClassName, NameFamily): Field alpha;
-axiom (forall<T> cl : ClassName, nm: NameFamily ::
- {FieldOfDecl(cl, nm): Field T}
- DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm);
-
-function $IsGhostField<T>(Field T): bool;
-
-// ---------------------------------------------------------------
-// -- 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 = <alpha>[ref,Field alpha]alpha;
-function {:inline true} read<alpha>(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] }
-function {:inline true} update<alpha>(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] }
-
-function $IsGoodHeap(HeapType): bool;
-var $Heap: HeapType where $IsGoodHeap($Heap);
-
-function $HeapSucc(HeapType, HeapType): bool;
-axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }
- $IsGoodHeap(update(h, r, f, x)) ==>
- $HeapSucc(h, update(h, r, f, x)));
-axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }
- $HeapSucc(a,b) && $HeapSucc(b,c) ==> $HeapSucc(a,c));
-axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
- $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));
-
-function $HeapSuccGhost(HeapType, HeapType): bool;
-axiom (forall h: HeapType, k: HeapType :: { $HeapSuccGhost(h,k) }
- $HeapSuccGhost(h,k) ==>
- $HeapSucc(h,k) &&
- (forall<alpha> o: ref, f: Field alpha :: { read(k, o, f) }
- !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
-
-// ---------------------------------------------------------------
-// -- 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<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
- $o != null && read(old($Heap), $o, alloc) ==>
- $o == this || rds[$Box($o)] || nw[$Box($o)] ==>
- read($Heap, $o, $f) == read(old($Heap), $o, $f));
- ensures $HeapSucc(old($Heap), $Heap);
-
-// havoc everything in $Heap, except rds-modi-{this}
-procedure $IterHavoc0(this: ref, rds: Set BoxType, modi: Set BoxType);
- modifies $Heap;
- ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
- $o != null && read(old($Heap), $o, alloc) ==>
- rds[$Box($o)] && !modi[$Box($o)] && $o != this ==>
- read($Heap, $o, $f) == read(old($Heap), $o, $f));
- ensures $HeapSucc(old($Heap), $Heap);
-
-// havoc $Heap at {this}+modi+nw
-procedure $IterHavoc1(this: ref, modi: Set BoxType, nw: Set BoxType);
- modifies $Heap;
- ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
- $o != null && read(old($Heap), $o, alloc) ==>
- read($Heap, $o, $f) == read(old($Heap), $o, $f) ||
- $o == this || modi[$Box($o)] || nw[$Box($o)]);
- ensures $HeapSucc(old($Heap), $Heap);
-
-procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType))
- returns (s: Set BoxType);
- ensures (forall bx: BoxType :: { s[bx] } s[bx] <==>
- read(newHeap, this, NW)[bx] ||
- ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc)));
-
-// ---------------------------------------------------------------
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 13:14:24 +0000