summaryrefslogtreecommitdiff
path: root/Test/dafny0/Parallel.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Parallel.dfy')
-rw-r--r--Test/dafny0/Parallel.dfy150
1 files changed, 75 insertions, 75 deletions
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 030eb350..00a1514c 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -1,14 +1,14 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class C {
- var data: int;
- var n: nat;
- var st: set<object>;
+ var data: int
+ var n: nat
+ var st: set<object>
ghost method CLemma(k: int)
- requires k != -23;
- ensures data < k; // magic, isn't it (or bogus, some would say)
+ requires k != -23
+ ensures data < k // magic, isn't it (or bogus, some would say)
}
// This method more or less just tests the syntax, resolution, and basic verification
@@ -19,31 +19,31 @@ method ParallelStatement_Resolve(
S: set<int>,
clx: C, cly: C, clk: int
)
- requires a != null && null !in spine;
- modifies a, spine;
+ requires a != null && null !in spine
+ modifies a, spine
{
- forall (i: int | 0 <= i < a.Length && i % 2 == 0) {
+ forall i | 0 <= i < a.Length && i % 2 == 0 {
a[i] := a[(i + 1) % a.Length] + 3;
}
- forall (o | o in spine) {
+ forall o | o in spine {
o.st := o.st + Repr;
}
- forall (x, y | x in S && 0 <= y+x < 100) {
+ forall x, y | x in S && 0 <= y+x < 100 {
Lemma(clx, x, y); // error: precondition does not hold (clx may be null)
}
- forall (x, y | x in S && 0 <= y+x < 100) {
+ forall x, y | x in S && 0 <= y+x < 100 {
cly.CLemma(x + y); // error: receiver might be null
}
- forall (p | 0 <= p)
- ensures F(p) <= Sum(p) + p - 1; // error (no connection is known between F and Sum)
+ forall p | 0 <= p
+ ensures F(p) <= Sum(p) + p - 1 // error (no connection is known between F and Sum)
{
assert 0 <= G(p);
ghost var t;
- if (p % 2 == 0) {
+ if p % 2 == 0 {
assert G(p) == F(p+2); // error (there's nothing that gives any relation between F and G)
t := p+p;
} else {
@@ -56,11 +56,11 @@ method ParallelStatement_Resolve(
}
}
-ghost method Lemma(c: C, x: int, y: int)
- requires c != null;
- ensures c.data <= x+y;
-ghost method PowerLemma(x: int, y: int)
- ensures Pred(x, y);
+lemma Lemma(c: C, x: int, y: int)
+ requires c != null
+ ensures c.data <= x+y
+lemma PowerLemma(x: int, y: int)
+ ensures Pred(x, y)
function F(x: int): int
function G(x: int): nat
@@ -71,54 +71,54 @@ function Pred(x: int, y: int): bool
// ---------------------------------------------------------------------
method M0(S: set<C>)
- requires null !in S;
- modifies S;
- ensures forall o :: o in S ==> o.data == 85;
- ensures forall o :: o != null && o !in S ==> o.data == old(o.data);
+ requires null !in S
+ modifies S
+ ensures forall o :: o in S ==> o.data == 85
+ ensures forall o :: o != null && o !in S ==> o.data == old(o.data)
{
- forall (s | s in S) {
+ forall s | s in S {
s.data := 85;
}
}
method M1(S: set<C>, x: C)
- requires null !in S && x in S;
+ requires null !in S && x in S
{
- forall (s | s in S)
- ensures s.data < 100;
+ forall s | s in S
+ ensures s.data < 100
{
assume s.data == 85;
}
- if (*) {
+ if * {
assert x.data == 85; // error (cannot be inferred from forall ensures clause)
} else {
assert x.data < 120;
}
- forall (s | s in S)
- ensures s.data < 70; // error
+ forall s | s in S
+ ensures s.data < 70 // error
{
assume s.data == 85;
}
}
method M2() returns (a: array<int>)
- ensures a != null;
- ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j];
+ ensures a != null
+ ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j]
{
a := new int[250];
- forall (i: nat | i < 125) {
+ forall i: nat | i < 125 {
a[i] := 423;
}
- forall (i | 125 <= i < 250) {
+ forall i | 125 <= i < 250 {
a[i] := 300 + i;
}
}
method M4(S: set<C>, k: int)
- modifies S;
+ modifies S
{
- forall (s | s in S && s != null) {
+ forall s | s in S && s != null {
s.n := k; // error: k might be negative
}
}
@@ -127,25 +127,25 @@ method M5()
{
if {
case true =>
- forall (x | 0 <= x < 100) {
+ forall x | 0 <= x < 100 {
PowerLemma(x, x);
}
assert Pred(34, 34);
case true =>
- forall (x,y | 0 <= x < 100 && y == x+1) {
+ forall x,y | 0 <= x < 100 && y == x+1 {
PowerLemma(x, y);
}
assert Pred(34, 35);
case true =>
- forall (x,y | 0 <= x < y < 100) {
+ forall x,y | 0 <= x < y < 100 {
PowerLemma(x, y);
}
assert Pred(34, 35);
case true =>
- forall (x | x in set k | 0 <= k < 100) {
+ forall x | x in set k | 0 <= k < 100 {
PowerLemma(x, x);
}
assert Pred(34, 34);
@@ -155,22 +155,22 @@ method M5()
method Main()
{
var a := new int[180];
- forall (i | 0 <= i < 180) {
+ forall i | 0 <= i < 180 {
a[i] := 2*i + 100;
}
var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];
- forall (i | 0 <= i < |sq|) {
+ forall i | 0 <= i < |sq| {
a[20+i] := sq[i];
}
- forall (t | t in sq) {
+ forall t | t in sq {
a[t] := 1000;
}
- forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
+ forall t,u | t in sq && t < 4 && 10 <= u < 10+t {
a[u] := 6000 + t;
}
var k := 0;
- while (k < 180) {
- if (k != 0) { print ", "; }
+ while k < 180 {
+ if k != 0 { print ", "; }
print a[k];
k := k + 1;
}
@@ -180,50 +180,50 @@ method Main()
method DuplicateUpdate() {
var a := new int[180];
var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];
- if (*) {
- forall (t,u | t in sq && 10 <= u < 10+t) {
+ if * {
+ forall t,u | t in sq && 10 <= u < 10+t {
a[u] := 6000 + t; // error: a[10] (and a[11]) are assigned more than once
}
} else {
- forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
+ forall t,u | t in sq && t < 4 && 10 <= u < 10+t {
a[u] := 6000 + t; // with the 't < 4' conjunct in the line above, this is fine
}
}
}
-ghost method DontDoMuch(x: int)
+lemma DontDoMuch(x: int)
{
}
method OmittedRange() {
- forall (x: int) { } // a type is still needed for the bound variable
- forall (x) {
+ forall x: int { } // a type is still needed for the bound variable
+ forall x {
DontDoMuch(x);
}
}
// ----------------------- two-state postconditions ---------------------------------
-class TwoState_C { ghost var data: int; }
+class TwoState_C { ghost var data: int }
// It is not possible to achieve this postcondition in a ghost method, because ghost
// contexts are not allowed to allocate state. Callers of this ghost method will know
// that the postcondition is tantamount to 'false'.
ghost method TwoState0(y: int)
- ensures exists o: TwoState_C :: o != null && fresh(o);
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
method TwoState_Main0() {
- forall (x) { TwoState0(x); }
+ forall x { TwoState0(x); }
assert false; // no prob, because the postcondition of TwoState0 implies false
}
method X_Legit(c: TwoState_C)
- requires c != null;
- modifies c;
+ requires c != null
+ modifies c
{
c.data := c.data + 1;
- forall (x | c.data <= x)
- ensures old(c.data) < x; // note that the 'old' refers to the method's initial state
+ forall x | c.data <= x
+ ensures old(c.data) < x // note that the 'old' refers to the method's initial state
{
}
}
@@ -235,8 +235,8 @@ method X_Legit(c: TwoState_C)
// method, not the beginning of the 'forall' statement.
method TwoState_Main2()
{
- forall (x: int)
- ensures exists o: TwoState_C :: o != null && fresh(o);
+ forall x: int
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
{
TwoState0(x);
}
@@ -251,8 +251,8 @@ method TwoState_Main2()
// statement's effect on the heap is not optimized away.
method TwoState_Main3()
{
- forall (x: int)
- ensures exists o: TwoState_C :: o != null && fresh(o);
+ forall x: int
+ ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)
{
assume false; // (there's no other way to achieve this forall-statement postcondition)
}
@@ -262,11 +262,11 @@ method TwoState_Main3()
// ------- empty forall statement -----------------------------------------
class EmptyForallStatement {
- var emptyPar: int;
+ var emptyPar: int
method Empty_Parallel0()
- modifies this;
- ensures emptyPar == 8;
+ modifies this
+ ensures emptyPar == 8
{
forall () {
this.emptyPar := 8;
@@ -274,11 +274,11 @@ class EmptyForallStatement {
}
function EmptyPar_P(x: int): bool
- ghost method EmptyPar_Lemma(x: int)
- ensures EmptyPar_P(x);
+ lemma EmptyPar_Lemma(x: int)
+ ensures EmptyPar_P(x)
method Empty_Parallel1()
- ensures EmptyPar_P(8);
+ ensures EmptyPar_P(8)
{
forall {
EmptyPar_Lemma(8);
@@ -288,7 +288,7 @@ class EmptyForallStatement {
method Empty_Parallel2()
{
forall
- ensures exists k :: EmptyPar_P(k);
+ ensures exists k :: EmptyPar_P(k)
{
var y := 8;
assume EmptyPar_P(y);
@@ -309,12 +309,12 @@ predicate ThProperty(step: nat, t: Nat, r: nat)
{
match t
case Zero => true
- case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)
+ case Succ(o) => step>0 && exists ro:nat, ss | ss == step-1 :: ThProperty(ss, o, ro) //WISH: ss should be autogrnerated. Note that step is not a bound variable.
}
-ghost method Th(step: nat, t: Nat, r: nat)
- requires t.Succ? && ThProperty(step, t, r);
+lemma Th(step: nat, t: Nat, r: nat)
+ requires t.Succ? && ThProperty(step, t, r)
// the next line follows from the precondition and the definition of ThProperty
- ensures exists ro:nat :: ThProperty(step-1, t.tail, ro);
+ ensures exists ro:nat, ss | ss == step-1 :: ThProperty(ss, t.tail, ro) //WISH same as above
{
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 22:32:31 +0000