From ddede5ad5f9236d8ee4e1e75ba3ecfd7077d9296 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Thu, 5 Nov 2009 01:24:43 +0000 Subject: Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "!(x in S)". Changed Dafny test files to use the new operator. Included the file b8.dfy into the VSI-Benchmarks test harness. --- Test/VSI-Benchmarks/Answer | 4 ++++ Test/VSI-Benchmarks/b4.dfy | 10 +++++----- Test/VSI-Benchmarks/b6.dfy | 2 +- Test/VSI-Benchmarks/b7.dfy | 4 ++-- Test/VSI-Benchmarks/b8.dfy | 32 ++++++++++++++++---------------- Test/VSI-Benchmarks/runtest.bat | 3 ++- Test/dafny0/BinaryTree.dfy | 8 ++++---- Test/dafny0/DTypes.dfy | 6 +++--- Test/dafny0/ListContents.dfy | 4 ++-- Test/dafny0/ListReverse.dfy | 2 +- Test/dafny0/SchorrWaite.dfy | 12 ++++++------ 11 files changed, 46 insertions(+), 41 deletions(-) (limited to 'Test') diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index 0149855c..a9fd2367 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -26,3 +26,7 @@ Dafny program verifier finished with 12 verified, 0 errors -------------------- b7.dfy -------------------- Dafny program verifier finished with 11 verified, 0 errors + +-------------------- b8.dfy -------------------- + +Dafny program verifier finished with 21 verified, 0 errors diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index b0b370a0..ac58b7d1 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -26,7 +26,7 @@ class Map { method Find(key: Key) returns (present: bool, val: Value) requires Valid(); - ensures !present ==> !(key in keys); + ensures !present ==> key !in keys; ensures present ==> (exists i :: 0 <= i && i < |keys| && keys[i] == key && values[i] == val); { @@ -78,9 +78,9 @@ class Map { ensures (forall k :: k in old(keys) ==> k in keys || k == key); // the given key is not there: // other values don't change: - ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values); + ensures key !in old(keys) ==> keys == old(keys) && values == old(values); ensures key in old(keys) ==> - !(key in keys) && + key !in keys && (exists h :: 0 <= h && h <= |keys| && keys[..h] == old(keys)[..h] && @@ -99,13 +99,13 @@ class Map { method FindIndex(key: Key) returns (idx: int) requires Valid(); ensures -1 <= idx && idx < |keys|; - ensures idx == -1 ==> !(key in keys); + ensures idx == -1 ==> key !in keys; ensures 0 <= idx ==> keys[idx] == key; { var j := 0; while (j < |keys|) invariant j <= |keys|; - invariant !(key in keys[..j]); + invariant key !in keys[..j]; decreases |keys| -j; { if (keys[j] == key) { diff --git a/Test/VSI-Benchmarks/b6.dfy b/Test/VSI-Benchmarks/b6.dfy index e5d061d2..f6e7879f 100644 --- a/Test/VSI-Benchmarks/b6.dfy +++ b/Test/VSI-Benchmarks/b6.dfy @@ -63,7 +63,7 @@ class Iterator { function Valid():bool reads this, footprint; { - this in footprint && c!= null && -1<= pos && !(null in footprint) + this in footprint && c!= null && -1<= pos && null !in footprint } method Init(coll:Collection) diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index 13a8ccd2..95267823 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -36,7 +36,7 @@ class Stream { function Valid():bool reads this, footprint; { - !(null in footprint) && this in footprint && isOpen + null !in footprint && this in footprint && isOpen } method GetCount() returns (c:int) @@ -152,7 +152,7 @@ class Client { var wr:= new Stream; call wr.Create(); while (0<|q.contents|) - invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && !(q in wr.footprint); + invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint; decreases |q.contents|; { call ch:= q.Dequeue(); diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index d499d017..643609d0 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -54,10 +54,10 @@ class Glossary { while (true) invariant rs.Valid() && fresh(rs.footprint); invariant glossary.Valid(); - invariant !(glossary in rs.footprint); - invariant !(null in glossary.keys); + invariant glossary !in rs.footprint; + invariant null !in glossary.keys; //to do add invariant invariant (forall d:: d in glossary.values ==>!(null in d)); *** - invariant !(q in rs.footprint); + invariant q !in rs.footprint; // ** invariant q.contents == glossary.keys; need a quantifer to express this (map doesnt necessarily add to end) // we leave out the decreases clause - unbounded stream { @@ -80,8 +80,8 @@ class Glossary { while (0<|q.contents|) invariant wr.Valid() && fresh(wr.footprint); invariant glossary.Valid(); - invariant !(glossary in wr.footprint) && !(null in glossary.keys); - invariant !(q in wr.footprint); + invariant glossary !in wr.footprint && null !in glossary.keys; + invariant q !in wr.footprint; decreases |q.contents|; { var term, present, definition; @@ -97,8 +97,8 @@ class Glossary { while (i < |definition|) invariant wr.Valid() && fresh(wr.footprint); invariant glossary.Valid(); - invariant !(glossary in wr.footprint) && !(null in glossary.keys); - invariant !(q in wr.footprint); + invariant glossary !in wr.footprint && null !in glossary.keys; + invariant q !in wr.footprint; invariant qcon == q.contents; decreases |definition| -i; { @@ -125,7 +125,7 @@ class Glossary { requires rs != null && rs.Valid(); modifies rs.footprint; ensures rs.Valid() && fresh(rs.footprint - old(rs.footprint)); - ensures term != null ==> !(null in definition); + ensures term != null ==> null !in definition; { call term := rs.GetWord(); if (term != null) @@ -133,7 +133,7 @@ class Glossary { definition := []; while (true) invariant rs.Valid() && fresh(rs.footprint - old(rs.footprint)); - invariant !(null in definition); + invariant null !in definition; { var w; call w := rs.GetWord(); @@ -159,7 +159,7 @@ class ReaderStream { function Valid():bool reads this, footprint; { - !(null in footprint) && this in footprint && isOpen + null !in footprint && this in footprint && isOpen } method Open() //reading @@ -193,7 +193,7 @@ class WriterStream { function Valid():bool reads this, footprint; { - !(null in footprint) && this in footprint && isOpen + null !in footprint && this in footprint && isOpen } method Create() //writing @@ -271,7 +271,7 @@ class Map { method Find(key: Key) returns (present: bool, val: Value) requires Valid(); - ensures !present ==> !(key in keys); + ensures !present ==> key !in keys; ensures present ==> (exists i :: 0 <= i && i < |keys| && keys[i] == key && values[i] == val); { @@ -323,9 +323,9 @@ class Map { ensures (forall k :: k in old(keys) ==> k in keys || k == key); // the given key is not there: // other values don't change: - ensures !(key in old(keys)) ==> keys == old(keys) && values == old(values); + ensures key !in old(keys) ==> keys == old(keys) && values == old(values); ensures key in old(keys) ==> - !(key in keys) && + key !in keys && (exists h :: 0 <= h && h <= |keys| && keys[..h] == old(keys)[..h] && @@ -344,13 +344,13 @@ class Map { method FindIndex(key: Key) returns (idx: int) requires Valid(); ensures -1 <= idx && idx < |keys|; - ensures idx == -1 ==> !(key in keys); + ensures idx == -1 ==> key !in keys; ensures 0 <= idx ==> keys[idx] == key; { var j := 0; while (j < |keys|) invariant j <= |keys|; - invariant !(key in keys[..j]); + invariant key !in keys[..j]; decreases |keys| -j; { if (keys[j] == key) { diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index a8658aef..fa737dca 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -7,7 +7,8 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe -for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy) do ( +for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy + b8.dfy ) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% %* %%f 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, b: CP) @@ -31,7 +31,7 @@ class C { var a2x: set>; method A2(b: set>) - requires !(null in b); + requires null !in b; { var x: set := a2x; var y: set := 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 { 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) 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 ==> -- cgit v1.2.3