diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/VSI-Benchmarks/Answer | 12 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/dafny0/AdvancedLHS.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 225 | ||||
| -rw-r--r-- | Test/dafny0/Array.dfy | 32 | ||||
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny0/MultiSets.dfy | 103 | ||||
| -rw-r--r-- | Test/dafny0/NatTypes.dfy | 3 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 5 | ||||
| -rw-r--r-- | Test/dafny0/TypeAntecedents.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 23 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/dafny1/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny1/Celebrity.dfy | 26 | ||||
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 18 | ||||
| -rw-r--r-- | Test/dafny1/UltraFilter.dfy | 3 | ||||
| -rw-r--r-- | Test/sanity/Answer | 2 |
17 files changed, 318 insertions, 167 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);
diff --git a/Test/sanity/Answer b/Test/sanity/Answer index 98607529..41d2f18c 100644 --- a/Test/sanity/Answer +++ b/Test/sanity/Answer @@ -1,4 +1,4 @@ Boogie program verifier finished with 1 verified, 0 errors
-Dafny program verifier finished with 10 verified, 0 errors
+Dafny program verifier finished with 8 verified, 0 errors
|