diff options
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/Answer | 54 | ||||
-rw-r--r-- | Test/dafny0/Calculations.dfy | 37 | ||||
-rw-r--r-- | Test/dafny0/CoPredicates.dfy | 11 | ||||
-rw-r--r-- | Test/dafny0/ParseErrors.dfy | 58 | ||||
-rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 29 | ||||
-rw-r--r-- | Test/dafny0/runtest.bat | 2 |
6 files changed, 175 insertions, 16 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 671c7c91..140f642f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -332,10 +332,10 @@ Execution trace: Definedness.dfy(86,5): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Definedness.dfy(86,10): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: target object may be null
+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(87,10): Error: possible violation of function precondition
@@ -542,7 +542,16 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-48 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)
+ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+57 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -553,7 +562,13 @@ ParseErrors.dfy(15,18): error: this operator cannot be part of a chain ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
-8 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(46,8): error: the main operator of a calculation must be transitive
+ParseErrors.dfy(62,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(63,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(68,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(69,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(75,2): error: this operator cannot continue this calculation
+14 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
@@ -857,19 +872,19 @@ Execution trace: Dafny program verifier finished with 32 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
-ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Else
- (0,0): anon9_Then
-ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
+ (0,0): anon8_Then
+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Then
+ (0,0): anon8_Else
+ (0,0): anon9_Then
ControlStructures.dfy(14,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
@@ -1305,7 +1320,7 @@ CoPredicates.dfy(30,22): Related location: Related location Execution trace:
(0,0): anon0
-Dafny program verifier finished with 14 verified, 1 error
+Dafny program verifier finished with 12 verified, 1 error
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
@@ -1615,6 +1630,25 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods
5 resolution/type errors detected in TailCalls.dfy
+-------------------- Calculations.dfy --------------------
+Calculations.dfy(3,4): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+Calculations.dfy(8,13): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(8,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(36,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Calculations.dfy(31,2): anon5_Else
+
+Dafny program verifier finished with 4 verified, 4 errors
-------------------- IteratorResolution.dfy --------------------
IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy new file mode 100644 index 00000000..9e44f62e --- /dev/null +++ b/Test/dafny0/Calculations.dfy @@ -0,0 +1,37 @@ +method CalcTest0(s: seq<int>) { + calc { + s[0]; // error: ill-formed line + } + + calc { + 2; + { assert s[0] == 1; } // error: ill-formed hint + 1 + 1; + } + + if (|s| > 0) { + calc { + s[0]; // OK: well-formed in this context + { assert s[0] == s[0]; } + <= s[0]; + } + } +} + +method CalcTest1(x: int, y: int) { + calc { + x + y; + { assume x == 0; } + y; + } + assert x == 0; // OK: follows from x + y == y; +} + +method CalcTest2(x: int, y: int) { + calc { + x + y; + { assume x == 0; } + y + x; + } + assert x == 0; // error: even though assumed above, is not exported by the calculation +}
\ No newline at end of file diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy index 67dff91b..c5651c90 100644 --- a/Test/dafny0/CoPredicates.dfy +++ b/Test/dafny0/CoPredicates.dfy @@ -51,8 +51,9 @@ function U2(n: int): Stream<int> UpwardBy2(n)
}
-ghost method Lemma2(n: int)
- ensures Even(UpwardBy2(2*n)); // this is true, but Dafny can't prove it
-{
- assert Even(U2(2*n)); // ... thanks to this lemma
-}
+// Postponed:
+//ghost method Lemma2(n: int)
+// ensures Even(UpwardBy2(2*n)); // this is true, and Dafny can prove it
+//{
+// assert Even(U2(2*n)); // ... thanks to this lemma
+//}
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy index 41df50eb..9a3cc18b 100644 --- a/Test/dafny0/ParseErrors.dfy +++ b/Test/dafny0/ParseErrors.dfy @@ -18,3 +18,61 @@ method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set ensures x in s == t; // error: 'in' is not chaining
{
}
+
+// ---------------------- calc statements -----------------------------------
+
+method TestCalc()
+{
+ calc {} // OK, empty calculations are allowed
+ calc {
+ 2 + 3; // OK, single-line calculations are allowed
+ }
+ calc {
+ 2 + 3;
+ calc { // OK: a calc statement is allowed as a sub-hint
+ 2;
+ 1 + 1;
+ }
+ calc {
+ 3;
+ 1 + 2;
+ }
+ { assert true; } // OK: multiple subhints are allowed between two lines
+ 1 + 1 + 1 + 2;
+ { assert 1 + 1 + 1 == 3; }
+ { assert true; }
+ 3 + 2;
+ }
+ calc != { // error: != is not allowed as the main operator of a calculation
+ 2 + 3;
+ 4;
+ }
+ calc { // OK, these operators are compatible
+ 2 + 3;
+ > 4;
+ >= 2 + 2;
+ }
+ calc < { // OK, these operators are compatible
+ 2 + 3;
+ == 5;
+ <= 3 + 3;
+ }
+ calc < { // error: cannot mix < and >= or >
+ 2 + 3;
+ >= 5;
+ > 2 + 2;
+ 6;
+ }
+ calc >= { // error: cannot mix >= and <= or !=
+ 2 + 3;
+ <= 5;
+ != 2 + 2;
+ 3;
+ }
+ calc { // error: cannot have more than one != per calc
+ 2 + 3;
+ != 4;
+ != 1 + 2;
+ 3;
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 274cc95a..c615c5ec 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -354,3 +354,32 @@ method MG1(l: GList, n: nat) var t := GCons(100, GNil);
t := GCons(120, l); // error: types don't match up (List<T$0> versus List<int>)
}
+
+// ------------------- calc statements ------------------------------
+
+method TestCalc(m: int, n: int, a: bool, b: bool)
+{
+ calc {
+ a + b; // error: invalid line
+ n + m;
+ }
+ calc {
+ a && b;
+ n + m; // error: all lines must have the same type
+ }
+ calc ==> {
+ n + m; // error: ==> operator requires boolean lines
+ n + m + 1;
+ n + m + 2;
+ }
+ calc {
+ n + m;
+ n + m + 1;
+ ==> n + m + 2; // error: ==> operator requires boolean lines
+ }
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints
+ m + n;
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 9789e7d7..9118e388 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -24,7 +24,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
RefinementModificationChecking.dfy TailCalls.dfy
- IteratorResolution.dfy Iterators.dfy) do (
+ Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
|