diff options
| author |  rustanleino <unknown> | 2010-07-06 23:08:37 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-07-06 23:08:37 +0000 |
| commit | 0cd554f0b5c748b76263dac4b4ff8bce559339e4 (patch) | |
| tree | 5662d1b37ebd47901950a1212e408d765a26690a /Test | |
| parent | a2844f2e24d7e90ba8fc2f0307a02d6ba68f4c7f (diff) | |
Dafny:
* changed rule about scoping of out-parameters
* added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 17 |
2 files changed, 22 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0f980af2..82f1da59 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -75,7 +75,11 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-10 resolution/type errors detected in TypeTests.dfy
+TypeTests.dfy(64,6): Error: Duplicate local-variable name: z
+TypeTests.dfy(66,6): Error: Duplicate local-variable name: x
+TypeTests.dfy(69,8): Error: Duplicate local-variable name: x
+TypeTests.dfy(72,6): Error: Duplicate local-variable name: y
+14 resolution/type errors detected in TypeTests.dfy
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,7): Error: RHS expression must be well defined
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index fe8644be..ccdbcb91 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -55,3 +55,20 @@ class ArrayTests { a[7] := 13; // error: array elements are not ghost locations
}
}
+
+// ---------------------
+
+method DuplicateVarName(x: int) returns (y: int)
+{
+ var z: int;
+ var z: int; // error: redeclaration of local
+ var x := x; // redeclaration of in-parameter is fine
+ var x := x; // error: but a redeclaration of that local is not fine
+ {
+ var x := x; // an inner local variable of the same name is fine
+ var x := x; // error: but a redeclaration thereof is not okay
+ var y := y; // duplicating an out-parameter here is fine
+ }
+ var y := y; // error: redeclaration of an out-parameter is not allowed (it is
+ // treated like an outermost-scoped local in this regard)
+}
|