diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-21 16:05:22 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-21 16:05:22 +0200 |
| commit | 33d178877dbde9371dc77144f8c3881751ad8553 (patch) | |
| tree | f9d3a0482f81df7e04523438e4df1e6c74567375 /Test/dafny0 | |
| parent | 1eb9803b383c5d245e1ed0ae43c0be951b2f1619 (diff) | |
Added tests for parsing and resolution of calc statements
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 18 | ||||
| -rw-r--r-- | Test/dafny0/ParseErrors.dfy | 58 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 24 |
3 files changed, 98 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index b7d48d7e..970f6d0f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -542,7 +542,15 @@ 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)
+56 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -553,7 +561,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
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..a7a84ebb 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -354,3 +354,27 @@ 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
+ }
+}
|