diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-17 16:32:16 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-17 16:32:16 -0800 |
| commit | cba00e514d09e4fbc1e571a334ce33102a83a6e4 (patch) | |
| tree | 17684e60a21eb750f13903c8a51a8513d77d3918 /Test/dafny0/Parallel.dfy | |
| parent | 9550c7c8ad15e6d9d5ec9e4b9bec16c34739a258 (diff) | |
Dafny: allow parallel statements with an empty list of bound variables
Diffstat (limited to 'Test/dafny0/Parallel.dfy')
| -rw-r--r-- | Test/dafny0/Parallel.dfy | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index 24f85e5d..ac11c1eb 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -269,3 +269,40 @@ method TwoState_Main3() }
assert false; // error: this location is indeed reachable (if the translation before it is sound)
}
+
+// ------- empty parallel statement -----------------------------------------
+
+var emptyPar: int;
+
+method Empty_Parallel0()
+ modifies this;
+ ensures emptyPar == 8;
+{
+ parallel () {
+ this.emptyPar := 8;
+ }
+}
+
+function EmptyPar_P(x: int): bool
+ghost method EmptyPar_Lemma(x: int)
+ ensures EmptyPar_P(x);
+
+method Empty_Parallel1()
+ ensures EmptyPar_P(8);
+{
+ parallel () {
+ EmptyPar_Lemma(8);
+ }
+}
+
+method Empty_Parallel2()
+{
+ parallel ()
+ ensures exists k :: EmptyPar_P(k);
+ {
+ var y := 8;
+ assume EmptyPar_P(y);
+ }
+ assert exists k :: EmptyPar_P(k); // yes
+ assert EmptyPar_P(8); // error: the parallel statement's ensures clause does not promise this
+}
|