Added some axioms about seq-to-multiset conversions

3 files changed, 44 insertions, 5 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 3f508c81..997b1da2 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -135,7 +135,8 @@ 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) } 

-  $IsGoodMultiSet(ms) <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx]));

+  $IsGoodMultiSet(ms) <==>

+  (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms)));

 

 function MultiSet#Card<T>(MultiSet T): int;

 axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));     

@@ -228,6 +229,10 @@ axiom (forall<T> s: Set T :: { MultiSet#Card(MultiSet#FromSet(s)) }
 function MultiSet#FromSeq<T>(Seq T): MultiSet T;

 // conversion produces a good map.

 axiom (forall<T> s: Seq T :: { MultiSet#FromSeq(s) } $IsGoodMultiSet(MultiSet#FromSeq(s)) );

+// cardinality axiom

+axiom (forall<T> s: Seq T ::

+  { MultiSet#Card(MultiSet#FromSeq(s)) }

+    MultiSet#Card(MultiSet#FromSeq(s)) == Seq#Length(s));

 // building axiom

 axiom (forall<T> s: Seq T, v: T ::

   { MultiSet#FromSeq(Seq#Build(s, v)) }

@@ -356,12 +361,14 @@ 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 ::

   { 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 }

-   (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));

+  Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));

+axiom (forall h: HeapType, a: ref, i: int ::

+  { Seq#Index(Seq#FromArray(h, a): Seq BoxType, i) }

+  0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)));

 axiom (forall h0, h1: HeapType, a: ref ::

   { Seq#FromArray(h1, a), $HeapSucc(h0, h1) }

   $IsGoodHeap(h0) && $IsGoodHeap(h1) && $HeapSucc(h0, h1) &&

diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy
index e01e9898..7478719e 100644
--- a/Test/dafny0/MultiSets.dfy
+++ b/Test/dafny0/MultiSets.dfy
@@ -269,3 +269,29 @@ method MultiSetProperty0(s: multiset<object>, t: multiset<object>, p: object)
     assert s + (t - s) == t;  // error

   }

 }

+

+// ---------- additional properties

+

+lemma UpperBoundOnOccurrenceCount(s: multiset<int>, x: int)

+  ensures 0 <= s[x] <= |s|;

+{

+}

+

+lemma MultisetCardinalityFromSequenceLength(s: seq<int>)

+  ensures |multiset(s)| == |s|;

+{

+}

+

+lemma Set_and_Multiset_Cardinalities(x: int, y: int)

+{

+  if * {

+    assert 1 <= |{x,y}| <= 2;

+    if x != y {

+      assert 2 <= |{x,y}|;

+    } else {

+      assert 2 <= |{x,y}|;  // error

+    }

+  } else {

+    assert |multiset{x,y}| == 2;

+  }

+}

diff --git a/Test/dafny0/MultiSets.dfy.expect b/Test/dafny0/MultiSets.dfy.expect
index cdee5d20..30534b11 100644
--- a/Test/dafny0/MultiSets.dfy.expect
+++ b/Test/dafny0/MultiSets.dfy.expect
@@ -18,5 +18,11 @@ Execution trace:
     (0,0): anon3

     (0,0): anon12_Then

     (0,0): anon14_Else

+MultiSets.dfy(292,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

+    (0,0): anon3

+    (0,0): anon9_Else

 

-Dafny program verifier finished with 54 verified, 4 errors

+Dafny program verifier finished with 59 verified, 5 errors