Merge

16 files changed, 317 insertions, 166 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index 2a4587f4..e2456408 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -7,10 +7,6 @@ Dafny program verifier finished with 10 verified, 0 errors
 

 Dafny program verifier finished with 6 verified, 0 errors

 

--------------------- b3.dfy --------------------

-

-Dafny program verifier finished with 10 verified, 0 errors

-

 -------------------- b4.dfy --------------------

 

 Dafny program verifier finished with 11 verified, 0 errors

@@ -22,11 +18,3 @@ Dafny program verifier finished with 22 verified, 0 errors
 -------------------- b6.dfy --------------------

 

 Dafny program verifier finished with 21 verified, 0 errors

-

--------------------- b7.dfy --------------------

-

-Dafny program verifier finished with 23 verified, 0 errors

-

--------------------- b8.dfy --------------------

-

-Dafny program verifier finished with 42 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index a733a1c0..799e1d40 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -6,7 +6,9 @@ set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
 set BPLEXE=%BOOGIEDIR%\Boogie.exe

 set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

-for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

+REM b3, b7 and b8 need reworking to not use body-less functions and methods.

+

+for %%f in (b1.dfy b2.dfy b4.dfy b5.dfy b6.dfy) do (

   echo.

   echo -------------------- %%f --------------------

 

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/Answer b/Test/dafny0/Answer
index 7a972f22..0723bcba 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -74,12 +74,14 @@ TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
 TypeTests.dfy(61,6): Error: Duplicate local-variable name: y

 TypeTests.dfy(68,17): Error: member F in type C does not refer to a method

 TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(78,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

-TypeTests.dfy(79,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+TypeTests.dfy(78,10): Error: cannot assign to multiple array elements (try a foreach).

+TypeTests.dfy(78,10): Error: cannot assign to multiple array elements (try a foreach).

+TypeTests.dfy(79,10): Error: cannot assign to multiple array elements (try a foreach).

+TypeTests.dfy(79,10): Error: cannot assign to multiple array elements (try a foreach).

 TypeTests.dfy(85,9): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(86,8): Error: sorry, cannot instantiate 'array' type with a subrange type

 TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-21 resolution/type errors detected in TypeTests.dfy

+23 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

@@ -102,20 +104,20 @@ NatTypes.dfy(40,14): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon4_Then

-NatTypes.dfy(54,16): Error: assertion violation

+NatTypes.dfy(57,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-NatTypes.dfy(68,16): Error: assertion violation

+NatTypes.dfy(71,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

-NatTypes.dfy(86,19): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(89,19): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-NatTypes.dfy(101,45): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

@@ -231,149 +233,167 @@ Execution trace:
 Definedness.dfy(50,18): Error: target object may be null

 Execution trace:

     (0,0): anon0

-Definedness.dfy(55,18): Error: target object may be null

+Definedness.dfy(51,3): Error BP5003: A postcondition might not hold on this return path.

+Definedness.dfy(50,22): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Definedness.dfy(77,7): Error: target object may be null

+Definedness.dfy(57,18): Error: target object may be null

 Execution trace:

     (0,0): anon0

-Definedness.dfy(78,5): Error: possible violation of function precondition

+Definedness.dfy(58,3): Error BP5003: A postcondition might not hold on this return path.

+Definedness.dfy(57,22): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Definedness.dfy(79,10): Error: possible violation of function precondition

+Definedness.dfy(65,3): Error BP5003: A postcondition might not hold on this return path.

+Definedness.dfy(64,22): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Definedness.dfy(84,14): Error: possible division by zero

+Definedness.dfy(85,7): Error: target object may be null

 Execution trace:

     (0,0): anon0

-Definedness.dfy(84,23): Error: possible division by zero

+Definedness.dfy(86,5): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-Definedness.dfy(85,15): Error: possible division by zero

+Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-Definedness.dfy(90,12): Error: possible division by zero

+Definedness.dfy(86,10): Error: target object may be null

 Execution trace:

     (0,0): anon0

-Definedness.dfy(97,15): Error: possible division by zero

+Definedness.dfy(87,10): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(97,5): anon8_LoopHead

+Definedness.dfy(92,14): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(92,23): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(93,15): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(98,12): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(105,15): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(105,5): anon8_LoopHead

     (0,0): anon8_LoopBody

-    Definedness.dfy(97,5): anon9_Else

+    Definedness.dfy(105,5): anon9_Else

     (0,0): anon3

-Definedness.dfy(106,23): Error: possible violation of function precondition

+Definedness.dfy(114,23): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(105,5): anon13_LoopHead

+    Definedness.dfy(113,5): anon13_LoopHead

     (0,0): anon13_LoopBody

     (0,0): anon14_Then

-Definedness.dfy(112,17): Error: possible violation of function precondition

+Definedness.dfy(120,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(105,5): anon13_LoopHead

+    Definedness.dfy(113,5): anon13_LoopHead

     (0,0): anon13_LoopBody

-    Definedness.dfy(105,5): anon14_Else

+    Definedness.dfy(113,5): anon14_Else

     (0,0): anon3

     (0,0): anon15_Then

     (0,0): anon6

-    Definedness.dfy(111,5): anon16_LoopHead

+    Definedness.dfy(119,5): anon16_LoopHead

     (0,0): anon16_LoopBody

     (0,0): anon17_Then

-Definedness.dfy(122,17): Error: possible violation of function precondition

+Definedness.dfy(130,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(121,5): anon7_LoopHead

+    Definedness.dfy(129,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(130,22): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

-Definedness.dfy(123,17): Error: possible violation of function precondition

+Definedness.dfy(131,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(121,5): anon7_LoopHead

+    Definedness.dfy(129,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(132,15): Error: possible division by zero

+Definedness.dfy(140,15): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(132,5): anon9_LoopHead

+    Definedness.dfy(140,5): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Definedness.dfy(132,5): anon10_Else

+    Definedness.dfy(140,5): anon10_Else

     (0,0): anon3

-Definedness.dfy(151,15): Error: possible division by zero

+Definedness.dfy(159,15): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(145,5): anon17_LoopHead

+    Definedness.dfy(153,5): anon17_LoopHead

     (0,0): anon17_LoopBody

-    Definedness.dfy(145,5): anon18_Else

+    Definedness.dfy(153,5): anon18_Else

     (0,0): anon3

     (0,0): anon19_Then

     (0,0): anon5

     (0,0): anon20_Then

     (0,0): anon8

-    Definedness.dfy(151,5): anon21_LoopHead

+    Definedness.dfy(159,5): anon21_LoopHead

     (0,0): anon21_LoopBody

-    Definedness.dfy(151,5): anon22_Else

+    Definedness.dfy(159,5): anon22_Else

     (0,0): anon11

-Definedness.dfy(170,17): Error: possible violation of function precondition

+Definedness.dfy(172,28): Error BP5004: This loop invariant might not hold on entry.

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(178,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(162,5): anon19_LoopHead

+    Definedness.dfy(170,5): anon19_LoopHead

     (0,0): anon19_LoopBody

-    Definedness.dfy(162,5): anon20_Else

+    Definedness.dfy(170,5): anon20_Else

     (0,0): anon3

     (0,0): anon21_Then

     (0,0): anon6

-    Definedness.dfy(169,5): anon22_LoopHead

+    Definedness.dfy(177,5): anon22_LoopHead

     (0,0): anon22_LoopBody

     (0,0): anon23_Then

     (0,0): anon24_Then

     (0,0): anon11

-Definedness.dfy(191,24): Error: possible violation of function precondition

-Execution trace:

-    (0,0): anon0

-Definedness.dfy(193,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+Definedness.dfy(199,24): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-Definedness.dfy(195,33): Error: range expression must be well defined

+Definedness.dfy(201,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

-Definedness.dfy(201,18): Error: RHS of assignment must be well defined

+Definedness.dfy(203,33): Error: range expression must be well defined

 Execution trace:

     (0,0): anon0

-Definedness.dfy(210,19): Error: possible division by zero

+Definedness.dfy(218,19): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(208,5): anon7_LoopHead

+    Definedness.dfy(216,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(218,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

-Definedness.dfy(210,28): Error: possible division by zero

+Definedness.dfy(218,28): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(208,5): anon7_LoopHead

+    Definedness.dfy(216,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(231,46): Error: possible violation of function postcondition

+Definedness.dfy(239,46): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-Definedness.dfy(238,22): Error: target object may be null

+Definedness.dfy(246,22): Error: target object may be null

 Execution trace:

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Definedness.dfy(254,24): Error: possible violation of function postcondition

+Definedness.dfy(262,24): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon7_Then

     (0,0): anon2

     (0,0): anon8_Else

 

-Dafny program verifier finished with 23 verified, 34 errors

+Dafny program verifier finished with 23 verified, 39 errors

 

 -------------------- FunctionSpecifications.dfy --------------------

 FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition

@@ -484,27 +504,24 @@ Execution trace:
     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Array.dfy(95,18): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-Array.dfy(107,6): Error: insufficient reads clause to read array element

+Array.dfy(97,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(115,6): Error: insufficient reads clause to read array element

+Array.dfy(105,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(131,6): Error: assignment may update an array element not in the enclosing context's modifies clause

+Array.dfy(121,6): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-Array.dfy(138,6): Error: assignment may update an array element not in the enclosing context's modifies clause

+Array.dfy(128,6): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 22 verified, 11 errors

+Dafny program verifier finished with 21 verified, 10 errors

 

 -------------------- MultiDimArray.dfy --------------------

 MultiDimArray.dfy(53,21): Error: assertion violation

@@ -812,61 +829,61 @@ Execution trace:
 Dafny program verifier finished with 18 verified, 10 errors

 

 -------------------- Termination.dfy --------------------

-Termination.dfy(100,3): Error: cannot prove termination; try supplying a decreases clause for the loop

+Termination.dfy(105,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(100,3): anon7_LoopHead

+    Termination.dfy(105,3): anon7_LoopHead

     (0,0): anon7_LoopBody

-    Termination.dfy(100,3): anon8_Else

+    Termination.dfy(105,3): anon8_Else

     (0,0): anon3

-    Termination.dfy(100,3): anon9_Else

+    Termination.dfy(105,3): anon9_Else

     (0,0): anon5

-Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop

+Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(108,3): anon9_LoopHead

+    Termination.dfy(113,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(108,3): anon10_Else

+    Termination.dfy(113,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(108,3): anon12_Else

+    Termination.dfy(113,3): anon12_Else

     (0,0): anon7

-Termination.dfy(117,3): Error: decreases expression might not decrease

+Termination.dfy(122,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

-    Termination.dfy(117,3): anon9_LoopHead

+    Termination.dfy(122,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(117,3): anon10_Else

+    Termination.dfy(122,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(117,3): anon12_Else

+    Termination.dfy(122,3): anon12_Else

     (0,0): anon7

-Termination.dfy(118,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

+Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

 Execution trace:

     (0,0): anon0

-    Termination.dfy(117,3): anon9_LoopHead

+    Termination.dfy(122,3): anon9_LoopHead

     (0,0): anon9_LoopBody

-    Termination.dfy(117,3): anon10_Else

+    Termination.dfy(122,3): anon10_Else

     (0,0): anon11_Then

     (0,0): anon5

-    Termination.dfy(117,3): anon12_Else

+    Termination.dfy(122,3): anon12_Else

     (0,0): anon7

-Termination.dfy(246,35): Error: cannot prove termination; try supplying a decreases clause

+Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

-Termination.dfy(286,3): Error: decreases expression might not decrease

+Termination.dfy(291,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

-    Termination.dfy(286,3): anon10_LoopHead

+    Termination.dfy(291,3): anon10_LoopHead

     (0,0): anon10_LoopBody

-    Termination.dfy(286,3): anon11_Else

-    Termination.dfy(286,3): anon12_Else

+    Termination.dfy(291,3): anon11_Else

+    Termination.dfy(291,3): anon12_Else

     (0,0): anon13_Else

     (0,0): anon8

 

-Dafny program verifier finished with 44 verified, 6 errors

+Dafny program verifier finished with 45 verified, 6 errors

 

 -------------------- DTypes.dfy --------------------

 DTypes.dfy(15,14): Error: assertion violation

@@ -898,46 +915,46 @@ Execution trace:
 Dafny program verifier finished with 27 verified, 6 errors

 

 -------------------- TypeParameters.dfy --------------------

-TypeParameters.dfy(41,22): Error: assertion violation

+TypeParameters.dfy(44,22): Error: assertion violation

 Execution trace:

     (0,0): anon0

-TypeParameters.dfy(63,27): Error: assertion violation

+TypeParameters.dfy(66,27): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-TypeParameters.dfy(130,12): Error: assertion violation

-TypeParameters.dfy(130,28): Related location: Related location

+TypeParameters.dfy(138,12): Error: assertion violation

+TypeParameters.dfy(138,28): Related location: Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon14_Then

-    TypeParameters.dfy(130,32): anon15_Else

+    TypeParameters.dfy(138,32): anon15_Else

     (0,0): anon5

-TypeParameters.dfy(132,12): Error: assertion violation

-TypeParameters.dfy(132,33): Related location: Related location

+TypeParameters.dfy(140,12): Error: assertion violation

+TypeParameters.dfy(140,33): Related location: Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon17_Then

-    TypeParameters.dfy(132,37): anon18_Else

+    TypeParameters.dfy(140,37): anon18_Else

     (0,0): anon11

-TypeParameters.dfy(146,15): Error BP5005: This loop invariant might not be maintained by the loop.

-TypeParameters.dfy(146,38): Related location: Related location

+TypeParameters.dfy(154,15): Error BP5005: This loop invariant might not be maintained by the loop.

+TypeParameters.dfy(154,38): Related location: Related location

 Execution trace:

     (0,0): anon0

-    TypeParameters.dfy(139,3): anon17_LoopHead

+    TypeParameters.dfy(147,3): anon17_LoopHead

     (0,0): anon17_LoopBody

-    TypeParameters.dfy(139,3): anon18_Else

+    TypeParameters.dfy(147,3): anon18_Else

     (0,0): anon5

     (0,0): anon20_Then

     (0,0): anon8

-    TypeParameters.dfy(145,3): anon21_LoopHead

+    TypeParameters.dfy(153,3): anon21_LoopHead

     (0,0): anon21_LoopBody

-    TypeParameters.dfy(145,3): anon22_Else

+    TypeParameters.dfy(153,3): anon22_Else

     (0,0): anon13

-    TypeParameters.dfy(145,3): anon24_Else

+    TypeParameters.dfy(153,3): anon24_Else

     (0,0): anon15

 

-Dafny program verifier finished with 33 verified, 5 errors

+Dafny program verifier finished with 35 verified, 5 errors

 

 -------------------- Datatypes.dfy --------------------

 Datatypes.dfy(79,20): Error: assertion violation

@@ -1108,3 +1125,7 @@ Dafny program verifier finished with 6 verified, 0 errors
 CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable

 CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable

 2 resolution/type errors detected in CallStmtTests.dfy

+

+-------------------- MultiSets.dfy --------------------

+

+Dafny program verifier finished with 22 verified, 0 errors

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 60854f63..f667e699 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -72,27 +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)

+    var a := new int[5];

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

+	

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

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

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

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

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

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

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

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

   }

 }

 

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 2063eec4..44b54f3d 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -48,27 +48,35 @@ class SoWellformed {
     requires next != null;

     modifies this;

     ensures next.xyz < 100;  // error: may not be well-defined (if body sets next to null)

+  {

 

+  }

   method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)

     requires next != null;

     modifies s;

     ensures next.xyz < 100;  // error: may not be well-defined (if this in s and body sets next to null)

-

+  {

+  

+  }

   method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)

     requires next != null && this !in s;

     modifies s;

     ensures next.xyz < 100;  // fine

+  {

+

+  }

 }

 

 // ---------------------- welldefinedness checks for statements -------------------

 

 class StatementTwoShoes {

   var x: int;

-

+  var s: StatementTwoShoes;

   function method F(b: int): StatementTwoShoes

     requires 0 <= b;

+	reads this;

   {

-    this

+    s

   }

 

   method M(p: StatementTwoShoes, a: int)

@@ -175,7 +183,7 @@ class StatementTwoShoes {
   }

 

   function G(w: int): int { 5 }

-  function method H(x: int): int

+  function method H(x: int): int { -x }

 

   method V(s: set<StatementTwoShoes>, a: int, b: int)

     modifies s;

diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy
new file mode 100644
index 00000000..0bc1004f
--- /dev/null
+++ b/Test/dafny0/MultiSets.dfy
@@ -0,0 +1,103 @@
+

+method test1()

+{

+   var ms: multiset<int> := multiset{1,1,1};

+   var ms2: multiset<int> := multiset{3};

+   assert 1 in ms;

+   assert forall i :: i != 1 ==> i !in ms; // 1 is the only thing in ms.

+   

+   assert ((ms - multiset{1}) - multiset {1}) != multiset{}; // it has more than 2 ones

+   assert ((ms - multiset{1}) - multiset {1}) - multiset{1} == multiset{}; // and exactly three

+

+   assert ms2 - ms == ms2; // set difference works correctly.

+   assert ms - multiset{1} == multiset{1,1};

+   assert !(multiset{1} !! multiset{1});

+   assert exists m :: !(m !! multiset{1});

+   assert forall m :: m !! multiset{};

+

+   assert forall s :: (s == set x: int | x in ms :: x) ==> s == {1};

+}

+

+method test2(ms: multiset<int>)

+{

+   var s := set x | x in ms :: x; // seems to be a reasonable conversion

+   assert forall x :: x in s <==> x in ms;

+   assert ms !! multiset{};

+}

+

+method test3(s: set<int>)

+{

+   assert forall x :: x in s <==> x in multiset(s);

+}

+method test4(sq: seq<int>, a: array<int>)

+   requires a != null;

+   modifies a;

+{

+   assert sq == sq[..|sq|];

+   assert sq == sq[0..];

+   assert sq == sq[..];

+

+   assert a.Length >= 0;

+   var s := a[..];

+}

+

+method test5()

+{

+   assert multiset({1,1}) == multiset{1};

+   assert multiset([1,1]) == multiset{1,1};

+}

+

+method test6(a: array<int>, n: int, e: int)

+   requires a != null && 0 <= n < a.Length;

+   modifies a;

+   ensures multiset(a[..n+1]) == multiset(a[..n]) + multiset{e};

+{

+  a[n] := e;

+  assert a[..n+1] == a[..n] + [e];

+}

+method test7(a: array<int>, i: int, j: int)

+   requires a != null && 0 <= i < j < a.Length;

+   modifies a;

+   ensures old(multiset(a[..])) == multiset(a[..]);

+   ensures a[j] == old (a[i]) && a[i] == old(a[j]);

+   ensures forall k :: 0 <= k < a.Length && k !in {i, j} ==> a[k] == old(a[k]);

+{

+   ghost var s := a[..i] + [a[i]] + a[i+1 .. j] + [a[j]] + a[j+1..];

+   assert a[..] == s;

+   a[i], a[j] := a[j], a[i];

+   assert a[..] == a[..i] + [a[i]] + a[i+1 .. j] + [a[j]] + a[j+1..];

+   assert s == a[..i] + [old(a[i])] + a[i+1 .. j] + [old(a[j])] + a[j+1..];

+}

+method test8(a: array<int>, i: int, j: int)

+   requires a != null && 0 <= i < j < a.Length;

+   modifies a;

+   ensures old(multiset(a[..])) == multiset(a[..]);

+   ensures a[j] == old (a[i]) && a[i] == old(a[j]);

+   ensures forall k :: 0 <= k < a.Length && k !in {i, j} ==> a[k] == old(a[k]);

+{

+   a[i], a[j] := a[j], a[i];

+}

+method test9(a: array<int>, i: int, j: int, limit: int)

+   requires a != null && 0 <= i < j < limit <= a.Length;

+   modifies a;

+   ensures old(multiset(a[0..limit])) == multiset(a[0..limit]);

+   ensures a[j] == old (a[i]) && a[i] == old(a[j]);

+   ensures forall k :: 0 <= k < limit && k !in {i, j} ==> a[k] == old(a[k]);

+{

+   a[i], a[j] := a[j], a[i];

+}

+method test10(s: seq<int>)

+   requires |s| > 4;

+{

+   assert multiset( s[3 := 2] ) == multiset(s) - multiset{s[3]} + multiset{2};

+   assert multiset( (s[2 := 1])[3 := 2] ) == (((multiset(s) - multiset{s[2]}) + multiset{1})  - multiset{s[3]}) + multiset{2};

+   assert multiset( (s[2 := s[3]])[3 := s[2]] ) == (((multiset(s) - multiset{s[2]}) + multiset{s[3]})  - multiset{s[3]}) + multiset{s[2]};

+}

+

+method test11(a: array<int>, n: int, c: int)

+   requires a != null && 0 <= c < n <= a.Length;

+   modifies a;

+   ensures multiset(a[c..n-1]) == multiset(a[c..n]) - multiset{a[n-1]};

+{

+

+}
\ No newline at end of file
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index e56b4122..47bc22e1 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -43,6 +43,9 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
 }

 

 function method FenEric<T>(t0: T, t1: T): T

+{

+  t1

+}

 

 datatype Pair<T> = Pr(T, T);

 

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index f31935af..1482dc24 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -90,6 +90,11 @@ class Termination {
   method Traverse<T>(a: List<T>) returns (val: T, b: List<T>)

     requires a != List.Nil;

     ensures a == List.Cons(val, b);

+  {

+    match a {

+	  case Cons(v, r) => val := v; b := r;

+	}

+  }

 }

 

 datatype List<T> = Nil | Cons(T, List<T>);

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 710e9838..5982a9e6 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -87,8 +87,8 @@ method N() returns (k: MyClass)
 {

   k := new MyClass;

 }

-

-function NF(): MyClass

+var a: MyClass;

+function NF(): MyClass reads this; { a }

 

 function TakesADatatype(a: List): int { 12 }

 

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 8f3f8b87..d6804661 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -14,10 +14,13 @@ class C<U> {
   {

     var t := F(3,u) && F(this,u);

     var kz := M(t,u);

-    assert kz && (G() || !G());

+	var a := G();

+    assert kz && (a || !a);

+  }

+  method G<Y>() returns (a: Y)

+  {

+    

   }

-

-  function G<Y>(): Y

 }

 

 class SetTest {

@@ -101,6 +104,9 @@ class CClient {
 

 static function IsCelebrity<Person>(c: Person, people: set<Person>): bool

   requires c == c || c in people;

+{

+  false

+}

 

 method FindCelebrity3(people: set<int>, ghost c: int)

   requires IsCelebrity(c, people);  // once upon a time, this caused the translator to produce bad Boogie

@@ -112,7 +118,9 @@ method FindCelebrity3(people: set<int>, ghost c: int)
 

 static function F(c: int, people: set<int>): bool

   requires IsCelebrity(c, people);

-

+{

+  false

+}

 function RogerThat<G>(g: G): G

 {

   g

@@ -154,7 +162,14 @@ method LoopyRoger(n: int)
 class TyKn_C<T> {

   var x: T;

   function G(): T

+    reads this;

+  {

+     x

+  }

   method M() returns (t: T)

+  {

+

+  }

 }

 

 class TyKn_K {

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 7aa1b38e..8aaa143b 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -20,7 +20,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy LoopModifies.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

-            CallStmtTests.dfy) do (

+            CallStmtTests.dfy MultiSets.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 %* %%f

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 5ee9f921..5bb746d8 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -85,12 +85,12 @@ Dafny program verifier finished with 29 verified, 0 errors
 

 -------------------- Rippling.dfy --------------------

 

-Dafny program verifier finished with 132 verified, 0 errors

+Dafny program verifier finished with 122 verified, 0 errors

 

 -------------------- Celebrity.dfy --------------------

 

-Dafny program verifier finished with 10 verified, 0 errors

+Dafny program verifier finished with 8 verified, 0 errors

 

 -------------------- UltraFilter.dfy --------------------

 

-Dafny program verifier finished with 19 verified, 0 errors

+Dafny program verifier finished with 20 verified, 0 errors

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 21b895aa..a10c4324 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,15 +1,26 @@
 // Celebrity example, inspired by the Rodin tutorial

 

-static function method Knows<Person>(a: Person, b: Person): bool

-  requires a != b;  // forbid asking about the reflexive case

+class Person

+{

+

+}

+

+var pa: seq<Person>;

 

-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool

+function method Knows(a: Person, b: Person): bool

+  reads this;

+  requires a != b;  // forbid asking about the reflexive case

+{

+   exists i | 0 <= i && i < |pa| :: 0 <= i < |pa| / 2 ==> pa[2*i] == a && pa[2*i+1] == b

+}

+function IsCelebrity(c: Person, people: set<Person>): bool

+  reads this;

 {

   c in people &&

   (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))

 }

 

-method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+method FindCelebrity0(people: set<Person>, ghost c: Person) returns (r: Person)

   requires (exists c :: IsCelebrity(c, people));

   ensures r == c;

 {

@@ -17,7 +28,7 @@ method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r:
   r := cc;

 }

 

-method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+method FindCelebrity1(people: set<Person>, ghost c: Person) returns (r: Person)

   requires IsCelebrity(c, people);

   ensures r == c;

 {

@@ -40,7 +51,7 @@ method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r:
   r := x;

 }

 

-method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

+method FindCelebrity2(people: set<Person>, ghost c: Person) returns (r: Person)

   requires IsCelebrity(c, people);

   ensures r == c;

 {

@@ -64,7 +75,7 @@ method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r:
   }

   r := b;

 }

-

+/*

 method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)

   requires 0 < n;

   requires (forall p :: p in people <==> 0 <= p && p < n);

@@ -88,3 +99,4 @@ method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)
   }

   r := b;

 }

+*/
\ No newline at end of file
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 0a4d541d..78905b6e 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -157,13 +157,14 @@ function last(xs: List): Nat
     case Cons(z, zs) => last(ys)

 }

 

+/*

 function mapF(xs: List): List

 {

   match xs

   case Nil => Nil

   case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))

 }

-function HardcodedUninterpretedFunction(n: Nat): Nat

+function HardcodedUninterpretedFunction(n: Nat): Nat*/

 

 function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List

 {

@@ -186,7 +187,7 @@ function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List
     else Cons(y, ys)

 }

 

-function filterP(xs: List): List

+/*function filterP(xs: List): List

 {

   match xs

   case Nil => Nil

@@ -195,7 +196,7 @@ function filterP(xs: List): List
     then Cons(y, filterP(ys))

     else filterP(ys)

 }

-function HardcodedUninterpretedPredicate(n: Nat): Bool

+function HardcodedUninterpretedPredicate(n: Nat): Bool*/

 

 function insort(n: Nat, xs: List): List

 {

@@ -327,21 +328,22 @@ ghost method P11()
 {

 }

 

+/*

 ghost method P12()

   ensures (forall n, xs :: drop(n, mapF(xs)) == mapF(drop(n, xs)));

 {

-}

+}*/

 

 ghost method P13()

   ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs));

 {

 }

-

+/*

 ghost method P14()

   ensures (forall xs, ys :: filterP(concat(xs, ys)) == concat(filterP(xs), filterP(ys)));

 {

 }

-

+*/

 ghost method P15()

   ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs)));

 {

@@ -478,12 +480,12 @@ ghost method P40()
   ensures (forall xs :: take(Zero, xs) == Nil);

 {

 }

-

+/*

 ghost method P41()

   ensures (forall n, xs :: take(n, mapF(xs)) == mapF(take(n, xs)));

 {

 }

-

+*/

 ghost method P42()

   ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs)));

 {

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index c8419890..0dfb6683 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -31,6 +31,9 @@ class UltraFilter<G> {
   // Dafny currently does not have a set comprehension expression, so this method stub will have to do

   method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)

     ensures (forall X :: X in h <==> M + X in f);

+  {

+    assume false;

+  }

 

   method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

     requires IsFilter(f, S);