diff options
| author |  wuestholz <unknown> | 2014-04-21 13:52:57 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-04-21 13:52:57 +0200 |
| commit | f6549ab8d0c6a93afeadbea6ba06694805fc3a6d (patch) | |
| tree | dc46b59b7daf4d53240e21a8844f4abc40cf9384 /Test/dafny0/AssumptionVariables0.dfy | |
| parent | a46e249e18ca7aac82818b565b9f828cb6f118d3 (diff) | |
Add support for assumption variables.
Diffstat (limited to 'Test/dafny0/AssumptionVariables0.dfy')
| -rw-r--r-- | Test/dafny0/AssumptionVariables0.dfy | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/Test/dafny0/AssumptionVariables0.dfy b/Test/dafny0/AssumptionVariables0.dfy new file mode 100644 index 00000000..2087b402 --- /dev/null +++ b/Test/dafny0/AssumptionVariables0.dfy @@ -0,0 +1,72 @@ +method test0(x: int)
+{
+ ghost var {:assumption} a0 := false; // error
+ ghost var a1, {:assumption} a2 := true, false; // error
+ ghost var {:assumption} a3: bool;
+ var {:assumption} a4; // 2 errors
+
+ a0 := a0 && (0 < x);
+
+ a1 := a1 && true;
+
+ a3 := true; // error
+
+ a3 := a2 && true; // error
+
+ a3 := a3 && true;
+}
+
+
+method test1()
+{
+ ghost var {:assumption} a0: bool;
+
+ a0 := true; // error
+
+ a0 := a0 && true;
+
+ a0 := a0 && true; // error
+}
+
+
+method test2()
+{
+ ghost var {:assumption} a0: bool;
+
+ a0 := a0 && true;
+
+ if (false)
+ {
+ var a0 := 1;
+
+ a0 := 2;
+
+ a0 := 3;
+
+ if (false)
+ {
+ ghost var {:assumption} a0: bool;
+
+ a0 := a0; // error
+
+ if (false)
+ {
+ var {:assumption} a0: bool; // error
+
+ if (false)
+ {
+ ghost var {:assumption} a0 := 1; // 2 errors
+
+ if (false)
+ {
+ ghost var {:assumption} a0: bool;
+
+ a0 := a0 && true;
+
+ a0 := a0 && true; // error
+ }
+ }
+ }
+ }
+ }
+}
|