diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-21 18:22:59 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-21 18:22:59 -0700 |
| commit | 17d0de36bf0f125ecac2ac6142c226f32f5370a5 (patch) | |
| tree | 1cf71d18f583ab14252b0a29badf3a2e0c270f57 /Test/dafny0/Parallel.dfy | |
| parent | 253ace40ff7f3382f1f413020069fcaae7a966e0 (diff) | |
Dafny: changed triggers (which are never really used, anyhow) from having a special syntactic form to being just an attribute
Dafny: added "parallel" statement (so far, only parsing and resolving)
Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them)
Diffstat (limited to 'Test/dafny0/Parallel.dfy')
| -rw-r--r-- | Test/dafny0/Parallel.dfy | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy new file mode 100644 index 00000000..0928c070 --- /dev/null +++ b/Test/dafny0/Parallel.dfy @@ -0,0 +1,84 @@ +/*
+method ParallelStatement_Syntax()
+{
+ parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {
+ a[i] := a[(i + 1) % a.Length] + 3;
+ }
+
+ parallel (o | o in spine) {
+ o.f := o.f + Repr;
+ }
+
+ parallel (x, y | x in S && 0 <= y+x < 100) {
+ Lemma(x, y);
+ }
+
+ parallel (p | 0 <= p)
+ ensures F(p) <= Sum(p) * (p-1) + 100;
+ {
+ assert G(p);
+ ghost var t;
+ if (p % 2 == 0) {
+ assert G(p) == F(p+2);
+ t := p*p;
+ } else {
+ assume H(p, 20) < 100; // don't know how to justify this
+ t := p;
+ }
+ PowerLemma(p, t);
+ t := t + 1;
+ PowerLemma(p, t);
+ }
+}
+*/
+
+class C {
+ var f: set<object>;
+}
+
+method ParallelStatement_Resolve(
+ a: array<int>,
+ spine: set<C>,
+ Repr: set<object>,
+ S: set<int>
+ )
+ requires a != null;
+ modifies a, spine;
+{
+ parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {
+ a[i] := a[(i + 1) % a.Length] + 3;
+ }
+
+ parallel (o | o in spine) {
+ o.f := o.f + Repr;
+ }
+
+ parallel (x, y | x in S && 0 <= y+x < 100) {
+ Lemma(x, y);
+ }
+
+ parallel (p | 0 <= p)
+ ensures F(p) <= Sum(p) * (p-1) + 100;
+ {
+ assert 0 <= G(p);
+ ghost var t;
+ if (p % 2 == 0) {
+ assert G(p) == F(p+2);
+ t := p*p;
+ } else {
+ assume H(p, 20) < 100; // don't know how to justify this
+ t := p;
+ }
+ PowerLemma(p, t);
+ t := t + 1;
+ PowerLemma(p, t);
+ }
+}
+
+method Lemma(x: int, y: int)
+ghost method PowerLemma(x: int, y: int)
+
+function F(x: int): int
+function G(x: int): int
+function H(x: int, y: int): int
+function Sum(x: int): int
|