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/AssumptionVariables1.dfy | |
| parent | a46e249e18ca7aac82818b565b9f828cb6f118d3 (diff) | |
Add support for assumption variables.
Diffstat (limited to 'Test/dafny0/AssumptionVariables1.dfy')
| -rw-r--r-- | Test/dafny0/AssumptionVariables1.dfy | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/Test/dafny0/AssumptionVariables1.dfy b/Test/dafny0/AssumptionVariables1.dfy new file mode 100644 index 00000000..135c2699 --- /dev/null +++ b/Test/dafny0/AssumptionVariables1.dfy @@ -0,0 +1,34 @@ +method test0(x: int)
+{
+ ghost var {:assumption} a0: bool;
+ ghost var {:assumption} a1: bool, a2: bool, {:assumption} a3: bool;
+
+ assert a0 && a1 && a3;
+
+ a0 := a0 && (0 < x);
+
+ a1 := a1 && true;
+}
+
+
+method test1(x: int)
+{
+ ghost var {:assumption} a0: bool;
+
+ assert a0;
+
+ a0 := a0 && (0 < x);
+
+ var y := x;
+
+ while (y < 0)
+ {
+ ghost var {:assumption} a0: bool;
+
+ assert a0;
+
+ a0 := a0 && (0 < y);
+
+ y := y + 1;
+ }
+}
|