diff options
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/BinaryTree.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/DTypes.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny0/ListContents.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/ListReverse.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/SchorrWaite.dfy | 12 |
5 files changed, 16 insertions, 16 deletions
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy index b3bcc823..7a5fb3c7 100644 --- a/Test/dafny0/BinaryTree.dfy +++ b/Test/dafny0/BinaryTree.dfy @@ -12,7 +12,7 @@ class IntSet { (root != null ==>
root in footprint && root.Valid() &&
contents == root.contents &&
- root.footprint <= footprint && !(this in root.footprint))
+ root.footprint <= footprint && this !in root.footprint)
}
method Init()
@@ -112,14 +112,14 @@ class Node { reads this, footprint;
{
this in footprint &&
- !(null in footprint) &&
+ null !in footprint &&
(left != null ==>
left in footprint && left.Valid() &&
- left.footprint <= footprint && !(this in left.footprint) &&
+ left.footprint <= footprint && this !in left.footprint &&
(forall y :: y in left.contents ==> y < data)) &&
(right != null ==>
right in footprint && right.Valid() &&
- right.footprint <= footprint && !(this in right.footprint) &&
+ right.footprint <= footprint && this !in right.footprint &&
(forall y :: y in right.contents ==> data < y)) &&
(left == null && right == null ==>
contents == {data}) &&
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index f6e0a2b4..c468cff4 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -5,14 +5,14 @@ class C { requires v != null;
{
var o: object := v;
- assert !(o in n); // should be known from the types involved
+ assert o !in n; // should be known from the types involved
}
method N(v: Stack)
/* this time without the precondition */
{
var o: object := v;
- assert !(o in n); // error: v may be null
+ assert o !in n; // error: v may be null
}
method A0(a: CP<int,C>, b: CP<int,object>)
@@ -31,7 +31,7 @@ class C { var a2x: set<CP<C,Node>>;
method A2(b: set<CP<Node,C>>)
- requires !(null in b);
+ requires null !in b;
{
var x: set<object> := a2x;
var y: set<object> := b;
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy index 6cb7c5a0..01d8b63b 100644 --- a/Test/dafny0/ListContents.dfy +++ b/Test/dafny0/ListContents.dfy @@ -8,11 +8,11 @@ class Node<T> { function Valid(): bool
reads this, footprint;
{
- this in this.footprint && !(null in this.footprint) &&
+ this in this.footprint && null !in this.footprint &&
(next == null ==> list == [data]) &&
(next != null ==>
next in footprint && next.footprint <= footprint &&
- !(this in next.footprint) &&
+ this !in next.footprint &&
list == [data] + next.list &&
next.Valid())
}
diff --git a/Test/dafny0/ListReverse.dfy b/Test/dafny0/ListReverse.dfy index af61a7a3..08b14751 100644 --- a/Test/dafny0/ListReverse.dfy +++ b/Test/dafny0/ListReverse.dfy @@ -3,7 +3,7 @@ class Node { var nxt: Node;
method ReverseInPlace(x: Node, r: set<Node>) returns (reverse: Node)
- requires !(null in r);
+ requires null !in r;
requires x == null || x in r;
requires (forall y :: y in r ==> y.nxt == null || y.nxt in r); // region closure
modifies r;
diff --git a/Test/dafny0/SchorrWaite.dfy b/Test/dafny0/SchorrWaite.dfy index db5928f4..20db882a 100644 --- a/Test/dafny0/SchorrWaite.dfy +++ b/Test/dafny0/SchorrWaite.dfy @@ -92,7 +92,7 @@ class Main { var stackNodes := [];
var unmarkedNodes := S - {t}; // used as ghost variable
while (true)
- invariant root.marked && t in S && !(t in stackNodes);
+ invariant root.marked && t in S && t !in stackNodes;
// stackNodes has no duplicates:
invariant (forall i, j :: 0 <= i && i < j && j < |stackNodes| ==>
stackNodes[i] != stackNodes[j]);
@@ -108,9 +108,9 @@ class Main { stackNodes[j].children[stackNodes[j].childrenVisited] == stackNodes[j+1]);
invariant 0 < |stackNodes| ==>
stackNodes[|stackNodes|-1].children[stackNodes[|stackNodes|-1].childrenVisited] == t;
- invariant (forall n :: n in S && n.marked && !(n in stackNodes) && n != t ==>
+ invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
- invariant (forall n :: n in S && !(n in stackNodes) && n != t ==>
+ invariant (forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited));
invariant (forall n: Node :: n.children == old(n.children));
invariant (forall n :: n in S && !n.marked ==> n in unmarkedNodes);
@@ -161,7 +161,7 @@ class Main { var stackNodes := []; // used as ghost variable
var unmarkedNodes := S - {t}; // used as ghost variable
while (true)
- invariant root.marked && t != null && t in S && !(t in stackNodes);
+ invariant root.marked && t != null && t in S && t !in stackNodes;
invariant |stackNodes| == 0 <==> p == null;
invariant 0 < |stackNodes| ==> p == stackNodes[|stackNodes|-1];
// stackNodes has no duplicates:
@@ -174,9 +174,9 @@ class Main { (forall j :: 0 <= j && j < n.childrenVisited ==>
n.children[j] == null || n.children[j].marked));
invariant (forall n :: n in stackNodes ==> n.childrenVisited < |n.children|);
- invariant (forall n :: n in S && n.marked && !(n in stackNodes) && n != t ==>
+ invariant (forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
(forall ch :: ch in n.children && ch != null ==> ch in S && ch.marked));
- invariant (forall n :: n in S && !(n in stackNodes) && n != t ==>
+ invariant (forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited));
invariant (forall n :: n in stackNodes || n.children == old(n.children));
invariant (forall n :: n in stackNodes ==>
|