From dd37b19e4afcb2d9475894d48c48e6a8308ec0a0 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Thu, 14 Jul 2011 15:58:35 -0700 Subject: Strengthened axioms for multisets and sequences. --- Binaries/DafnyPrelude.bpl | 59 +++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 50 insertions(+), 9 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 37b972d0..50852724 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -101,7 +101,7 @@ axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0); type MultiSet T = [T]int; function $IsGoodMultiSet(ms: MultiSet T): bool; -// ints are non-negative, used after havocing. +// ints are non-negative, used after havocing, and for conversion from sequences to multisets. axiom (forall ms: MultiSet T :: { $IsGoodMultiSet(ms) } $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o])); @@ -109,9 +109,9 @@ function MultiSet#Empty(): MultiSet T; axiom (forall o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0); function MultiSet#Singleton(T): MultiSet T; -axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r)[r] == 1); axiom (forall r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) && (MultiSet#Singleton(r)[o] == 0 <==> r != o)); +axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r)); function MultiSet#UnionOne(MultiSet T, T): MultiSet T; // pure containment axiom (in the original multiset or is the added element) @@ -131,8 +131,6 @@ function MultiSet#Union(MultiSet T, MultiSet T): MultiSet T; // union-ing is the sum of the contents 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#Union(a,b) } - MultiSet#Union(a,b) == MultiSet#Union(b,a)); // two containment axioms axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] } @@ -186,16 +184,29 @@ axiom (forall s: Set T, a: T :: { MultiSet#FromSet(s)[a] } // conversion to a multiset, from a sequence. function MultiSet#FromSeq(Seq T): MultiSet T; +// conversion produces a good map. +axiom (forall s: Seq T :: { MultiSet#FromSeq(s) } $IsGoodMultiSet(MultiSet#FromSeq(s)) ); +// building axiom axiom (forall s: Seq T, v: T :: { MultiSet#FromSeq(Seq#Build(s, v)) } MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v) ); -axiom (MultiSet#FromSeq(Seq#Empty(): Seq BoxType) == MultiSet#Empty()); +axiom (forall :: MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T); + +// concatenation axiom axiom (forall a: Seq T, b: Seq T :: { MultiSet#FromSeq(Seq#Append(a, b)) } - MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)) && - MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(b), MultiSet#FromSeq(a))); - + MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)) ); + +// update axiom +axiom (forall s: Seq T, i: int, v: T, x: T :: + { MultiSet#FromSeq(Seq#Update(s, i, v))[x] } + MultiSet#FromSeq(Seq#Update(s, i, v))[x] == + MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s,i))), MultiSet#Singleton(v))[x] ); + // 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 -------------------------------- // --------------------------------------------------------------- @@ -303,9 +314,39 @@ axiom (forall s, t: Seq T :: 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 :: { Seq#Length(Seq#FromArray(h,a)) } Seq#Length(Seq#FromArray(h, a)) == array.Length(a)); +axiom (forall h: HeapType, a: ref :: + { Seq#Length(Seq#FromArray(h,a)) } + Seq#Length(Seq#FromArray(h, a)) == array.Length(a)); axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType } (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 :: + { 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 :: + { Seq#FromArray(update(h, a, IndexField(i), v), a) } + 0 <= i && i < array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) ); + +// 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 && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v) ); +axiom (forall s: Seq T, i: int, v: T, n: int :: + { Seq#Take(Seq#Update(s, i, v), n) } + n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n)); +axiom (forall s: Seq T, i: int, v: T, n: int :: + { Seq#Drop(Seq#Update(s, i, v), n) } + 0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i-n, v) ); +axiom (forall s: Seq T, i: int, v: T, n: int :: + { Seq#Drop(Seq#Update(s, i, v), n) } + 0 <= i && i < n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n)); +// 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 <= 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)) ); +// 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) ); // --------------------------------------------------------------- // -- Boxing and unboxing ---------------------------------------- -- cgit v1.2.3