Added multiset from sequence axioms, removed array range RHSs. Fixed issue with duplicate array.Length functions in generated Boogie file.

2 files changed, 11 insertions, 25 deletions

diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy
index cc07cbb5..f1fc7d48 100644
--- a/Test/dafny0/AdvancedLHS.dfy
+++ b/Test/dafny0/AdvancedLHS.dfy
@@ -34,7 +34,6 @@ class C {
 

     if (a != null && 10 <= a.Length) {

       a[2] := new C;

-      a[4..8] := null;

       a[3] := *;

     }

     if (b != null && 10 <= b.Length0 && 20 <= b.Length1) {

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 5f366d10..1a18be6d 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -72,30 +72,17 @@ class A {
   }

 

   method Q() {

-    var y := new object[100];

-    y[5] := null;

-    y[0..] := null;

-    y[..83] := null;

-    y[0..y.Length] := null;

-  }

-

-  method R() {

-    var y := new int[100];

-    y[55] := 80;

-    y[10..] := 25;

-    y[..83] := 30;

-    y[50..60] := 35;

-    y[55] := 90;

-

-    assert y[54] == 35;

-    assert y[55] == 90;

-    assert y[83] == 25;

-    assert y[8] == 30;

-    assert y[90] + y[91] + y[0] + 20 == y.Length;

-    assert y[93] == 24;  // error (it's 25)

-

-    y[..] := 4; // assign to all elements.

-    assert forall i :: 0 <= i < y.Length ==> y[i] == 4;

+    var a := new int[5];

+    y[0],y[1],y[2],y[3],y[4] := 0,1,2,3,4;

+	

+	assert [1,2,3,4] == y[1..];

+	assert [1,2,3,4] == y[1.. y.Length];

+	assert [1] == y[1..2];

+	assert [0,1] == y[..2];

+	assert [0,1] == y[0..2];

+	assert forall i :: 0 <= i <= y.Length ==> [] == y[i..i];

+    assert [0,1,2,3,4] == y[..];

+    assert forall i :: 0 <= i < y.Length ==> y[i] == i;

   }

 }