From f21cde811e9194934eb30f196ad19c2cfbeb8ff9 Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 1 Nov 2014 13:02:38 -0700 Subject: Various DafnyPrelude.bpl cleanup. Removed unused cases from axioms where Seq#Take and Seq#Drop take out-of-range arguments --- Binaries/DafnyPrelude.bpl | 128 ++-------------------------------------------- 1 file changed, 4 insertions(+), 124 deletions(-) (limited to 'Binaries/DafnyPrelude.bpl') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index eea23383..6ddff694 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -103,21 +103,6 @@ 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 :: @@ -255,7 +240,6 @@ 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; @@ -275,10 +259,6 @@ type HandleType; 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; @@ -358,91 +338,6 @@ axiom(forall h, k : Heap, bx : Box, t : Ty :: 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 ----------------------------------------------------- // --------------------------------------------------------------- @@ -558,10 +453,6 @@ 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]); @@ -832,12 +723,13 @@ axiom (forall s: Seq T, x: T :: { Seq#Contains(s,x) } axiom (forall x: ref :: { Seq#Contains(Seq#Empty(), x) } !Seq#Contains(Seq#Empty(), x)); + axiom (forall s0: Seq T, s1: Seq T, x: T :: { Seq#Contains(Seq#Append(s0, s1), x) } Seq#Contains(Seq#Append(s0, s1), x) <==> Seq#Contains(s0, x) || Seq#Contains(s1, x)); -axiom (forall s: Seq T, v: T, x: T :: +axiom (forall s: Seq T, v: T, x: T :: // needed to prove things like '4 in [2,3,4]', see method TestSequences0 in SmallTests.dfy { Seq#Contains(Seq#Build(s, v), x) } Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x))); @@ -869,9 +761,7 @@ axiom (forall s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) } function Seq#Take(s: Seq T, howMany: int): Seq T; axiom (forall s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) } - 0 <= n ==> - (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) && - (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s))); + 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n); axiom (forall s: Seq T, n: int, j: int :: {:weight 25} { Seq#Index(Seq#Take(s,n), j) } @@ -881,9 +771,7 @@ axiom (forall s: Seq T, n: int, j: int :: function Seq#Drop(s: Seq T, howMany: int): Seq T; axiom (forall s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) } - 0 <= n ==> - (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) && - (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0)); + 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n); axiom (forall s: Seq T, n: int, j: int :: {:weight 25} { Seq#Index(Seq#Drop(s,n), j) } @@ -926,14 +814,6 @@ axiom (forall h0, h1: Heap, 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: 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 - ==> - (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) } - 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i)))); -****/ // Commutability of Take and Drop with Update. axiom (forall s: Seq T, i: int, v: T, n: int :: -- cgit v1.2.3