From e10af1acf3bad4b74545f6609e659882b68fff83 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 26 Mar 2013 11:01:25 -0700 Subject: Enhanced the VSI-Benchmarks tests: - replaced the sequences used to specify permutations with multisets - used some of the newer syntax in Dafny --- Test/VSI-Benchmarks/b2.dfy | 14 +++++----- Test/VSI-Benchmarks/b3.dfy | 64 +++++++++++++--------------------------------- Test/VSI-Benchmarks/b4.dfy | 12 ++++----- Test/VSI-Benchmarks/b7.dfy | 17 ++++-------- Test/VSI-Benchmarks/b8.dfy | 33 +++++++++++------------- 5 files changed, 51 insertions(+), 89 deletions(-) (limited to 'Test/VSI-Benchmarks') diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 3046621b..a7f1ca9a 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -2,18 +2,18 @@ class Benchmark2 { method BinarySearch(a: array, key: int) returns (result: int) requires a != null; - requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]); - ensures -1 <= result && result < a.Length; + requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]; + ensures -1 <= result < a.Length; ensures 0 <= result ==> a[result] == key; - ensures result == -1 ==> (forall i :: 0 <= i && i < a.Length ==> a[i] != key); + ensures result == -1 ==> forall i :: 0 <= i < a.Length ==> a[i] != key; { var low := 0; var high := a.Length; while (low < high) - invariant 0 <= low && low <= high && high <= a.Length; - invariant (forall i :: 0 <= i && i < low ==> a[i] < key); - invariant (forall i :: high <= i && i < a.Length ==> key < a[i]); + invariant 0 <= low <= high <= a.Length; + invariant forall i :: 0 <= i < low ==> a[i] < key; + invariant forall i :: high <= i < a.Length ==> key < a[i]; { var mid := low + (high - low) / 2; var midVal := a[mid]; @@ -49,7 +49,7 @@ method Main() { method TestSearch(a: array, key: int) requires a != null; - requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]); + requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]; { var b := new Benchmark2; var r := b.BinarySearch(a, key); diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 7cf3de07..9fc8a10d 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -27,7 +27,7 @@ class Queue { reads this; { contents[0] } function method Get(i: int): T - requires 0 <= i && i < |contents|; + requires 0 <= i < |contents|; reads this; { contents[i] } } @@ -40,58 +40,30 @@ class Comparable { class Benchmark3 { - method Sort(q: Queue) returns (r: Queue, ghost perm: seq) + method Sort(q: Queue) returns (r: Queue) requires q != null; modifies q; ensures r != null && fresh(r); ensures |r.contents| == |old(q.contents)|; - ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==> - r.Get(i) <= r.Get(j)); - //perm is a permutation - ensures |perm| == |r.contents|; // ==|pperm| - ensures (forall i :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| ); - ensures (forall i, j :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]); + ensures forall i, j :: 0 <= i < j < |r.contents| ==> r.Get(i) <= r.Get(j); // the final Queue is a permutation of the input Queue - ensures (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]); + ensures multiset(r.contents) == multiset(old(q.contents)); { r := new Queue.Init(); - ghost var p := []; - - var n := 0; - while (n < |q.contents|) - invariant n <= |q.contents|; - invariant n == |p|; - invariant (forall i :: 0 <= i && i < n ==> p[i] == i); - { - p := p + [n]; - n := n + 1; - } - perm := []; - ghost var pperm := p + perm; - while (|q.contents| != 0) - invariant |r.contents| == |old(q.contents)| - |q.contents|; - invariant (forall i, j :: 0 <= i && i < j && j < |r.contents| ==> - r.contents[i] <= r.contents[j]); - invariant (forall i, j :: - 0 <= i && i < |r.contents| && - 0 <= j && j < |q.contents| - ==> r.contents[i] <= q.contents[j]); - - // pperm is a permutation - invariant pperm == p + perm && |p| == |q.contents| && |perm| == |r.contents|; - invariant (forall i :: 0 <= i && i < |perm| ==> 0 <= perm[i] && perm[i] < |pperm|); - invariant (forall i :: 0 <= i && i < |p| ==> 0 <= p[i] && p[i] < |pperm|); - invariant (forall i, j :: 0 <= i && i < j && j < |pperm| ==> pperm[i] != pperm[j]); + invariant |r.contents| + |q.contents| == |old(q.contents)|; + invariant forall i, j :: 0 <= i < j < |r.contents| ==> r.contents[i] <= r.contents[j]; + invariant forall i, j :: + 0 <= i < |r.contents| && + 0 <= j < |q.contents| + ==> r.contents[i] <= q.contents[j]; // the current array is that permutation of the input array - invariant (forall i :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]); - invariant (forall i :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]); - { + invariant multiset(r.contents + q.contents) == multiset(old(q.contents)); + { + ghost var qc := q.contents; var m,k := RemoveMin(q); - perm := perm + [p[k]]; //adds index of min to perm - p := p[k+1..] + p[..k]; //remove index of min from p + assert qc == qc[..k] + [m] + qc[k+1..]; r.Enqueue(m); - pperm := pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] + [pperm[k]]; } } @@ -100,8 +72,8 @@ class Benchmark3 { requires q != null && |q.contents| != 0; modifies q; ensures |old(q.contents)| == |q.contents| + 1; - ensures 0 <= k && k < |old(q.contents)| && old(q.contents[k]) == m; - ensures (forall i :: 0 <= i && i < |q.contents| ==> m <= q.contents[i]); + ensures 0 <= k < |old(q.contents)| && old(q.contents[k]) == m; + ensures forall i :: 0 <= i < |q.contents| ==> m <= q.contents[i]; ensures q.contents == old(q.contents)[k+1..] + old(q.contents)[..k]; { var n := |q.contents|; @@ -112,8 +84,8 @@ class Benchmark3 { while (j < n) invariant j <= n; invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated - invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m; - invariant (forall i :: 0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far + invariant 0 <= k < |old(q.contents)| && old(q.contents)[k] == m; + invariant forall i :: 0 <= i < j ==> m <= old(q.contents)[i]; //m is min so far { var x := q.Dequeue(); q.Enqueue(x); diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index d5a56df4..6830fd87 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -27,7 +27,7 @@ class Map { this in Repr && |Keys| == |Values| && |nodes| == |Keys| + 1 && head == nodes[0] && - (forall i :: 0 <= i && i < |Keys| ==> + (forall i :: 0 <= i < |Keys| ==> nodes[i] != null && nodes[i] in Repr && nodes[i].key == Keys[i] && nodes[i].key !in Keys[i+1..] && @@ -51,7 +51,7 @@ class Map { method Find(key: Key) returns (present: bool, val: Value) requires Valid(); ensures !present ==> key !in Keys; - ensures present ==> (exists i :: 0 <= i && i < |Keys| && Keys[i] == key && Values[i] == val); + ensures present ==> exists i :: 0 <= i < |Keys| && Keys[i] == key && Values[i] == val; { var p, n, prev := FindIndex(key); if (p == null) { @@ -66,11 +66,11 @@ class Map { requires Valid(); modifies Repr; ensures Valid() && fresh(Repr - old(Repr)); - ensures (forall i :: 0 <= i && i < |old(Keys)| && old(Keys)[i] == key ==> + ensures forall i :: 0 <= i < |old(Keys)| && old(Keys)[i] == key ==> |Keys| == |old(Keys)| && Keys[i] == key && Values[i] == val && - (forall j :: 0 <= j && j < |Values| && i != j ==> - Keys[j] == old(Keys)[j] && Values[j] == old(Values)[j])); + (forall j :: 0 <= j < |Values| && i != j ==> + Keys[j] == old(Keys)[j] && Values[j] == old(Values)[j]); ensures key !in old(Keys) ==> Keys == [key] + old(Keys) && Values == [val] + old(Values); { var p, n, prev := FindIndex(key); @@ -100,7 +100,7 @@ class Map { ensures key in old(Keys) ==> |Keys| == |old(Keys)| - 1 && key !in Keys && (exists h :: - 0 <= h && h < |old(Keys)| && + 0 <= h < |old(Keys)| && Keys[..h] == old(Keys)[..h] && Values[..h] == old(Values)[..h] && Keys[h..] == old(Keys)[h+1..] && diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index d6759c5f..8d218ec9 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -23,7 +23,7 @@ class Queue { reads this; { contents[0] } function Get(i: int): T - requires 0 <= i && i < |contents|; + requires 0 <= i < |contents|; reads this; { contents[i] } } @@ -101,20 +101,14 @@ class Stream { class Client { - method Sort(q: Queue) returns (r: Queue, perm:seq) + method Sort(q: Queue) returns (r: Queue) requires q != null; modifies q; ensures r != null && fresh(r); ensures |r.contents| == |old(q.contents)|; - ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==> - r.Get(i) <= r.Get(j)); - //perm is a permutation - ensures |perm| == |r.contents|; // ==|pperm| - ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| ); - ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]); + ensures forall i, j :: 0 <= i < j < |r.contents| ==> r.Get(i) <= r.Get(j); // the final Queue is a permutation of the input Queue - ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]); - + ensures multiset(r.contents) == multiset(old(q.contents)); method Main() { @@ -136,8 +130,7 @@ class Client { } rd.Close(); - var perm; - q,perm := Sort(q); + q := Sort(q); var wr := new Stream; wr.Create(); diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 2149df25..7608ed85 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -21,14 +21,14 @@ class Queue { reads this; { contents[0] } function Get(i: int): T - requires 0 <= i && i < |contents|; + requires 0 <= i < |contents|; reads this; { contents[i] } } class Glossary { - method Sort(q: Queue) returns (r: Queue, perm:seq) + method Sort(q: Queue) returns (r: Queue) requires q != null; modifies q; ensures r != null && fresh(r); @@ -36,12 +36,8 @@ class Glossary { ensures (forall i, j :: 0 <= i && i < j && j < |r.contents| ==> r.Get(i) != null && r.Get(i).AtMost(r.Get(j))); - //perm is a permutation - ensures |perm| == |r.contents|; // ==|pperm| - ensures (forall i: int :: 0 <= i && i < |perm|==> 0 <= perm[i] && perm[i] < |perm| ); - ensures (forall i, j: int :: 0 <= i && i < j && j < |perm| ==> perm[i] != perm[j]); // the final Queue is a permutation of the input Queue - ensures (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]); + ensures multiset(r.contents) == multiset(old(q.contents)); method Main() { @@ -70,20 +66,21 @@ class Glossary { q.Enqueue(term); } } - + rs.Close(); - var p; - q,p := Sort(q); + ghost var qc := q.contents; + q := Sort(q); + assert forall k :: k in q.contents ==> k in multiset(q.contents); var wr := new WriterStream; wr.Create(); - + while (0 < |q.contents|) invariant wr.Valid() && fresh(wr.footprint); invariant glossary.Valid(); invariant glossary !in wr.footprint && null !in glossary.keys; - invariant (forall d :: d in glossary.values ==> null !in d); + invariant forall d :: d in glossary.values ==> null !in d; invariant q !in wr.footprint; - invariant (forall k :: k in q.contents ==> k in glossary.keys); + invariant forall k :: k in q.contents ==> k in glossary.keys; { var term := q.Dequeue(); var present,definition := glossary.Find(term); @@ -258,7 +255,7 @@ class Map { reads this; { |keys| == |values| && - (forall i, j :: 0 <= i && i < j && j < |keys| ==> keys[i] != keys[j]) + (forall i, j :: 0 <= i < j < |keys| ==> keys[i] != keys[j]) } method Init() @@ -272,7 +269,7 @@ class Map { method Find(key: Key) returns (present: bool, val: Value) requires Valid(); ensures !present ==> key !in keys; - ensures present ==> (exists i :: 0 <= i && i < |keys| && + ensures present ==> (exists i :: 0 <= i < |keys| && keys[i] == key && values[i] == val); { var j := FindIndex(key); @@ -288,10 +285,10 @@ class Map { requires Valid(); modifies this; ensures Valid(); - ensures (forall i :: 0 <= i && i < |old(keys)| && old(keys)[i] == key ==> + ensures (forall i :: 0 <= i < |old(keys)| && old(keys)[i] == key ==> |keys| == |old(keys)| && keys[i] == key && values[i] == val && - (forall j :: 0 <= j && j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j])); + (forall j :: 0 <= j < |values| && i != j ==> keys[j] == old(keys)[j] && values[j] == old(values)[j])); ensures key !in old(keys) ==> keys == old(keys) + [key] && values == old(values) + [val]; { var j := FindIndex(key); @@ -317,7 +314,7 @@ class Map { ensures key in old(keys) ==> |keys| == |old(keys)| - 1 && key !in keys && (exists h :: - 0 <= h && h <= |keys| && + 0 <= h <= |keys| && keys[..h] == old(keys)[..h] && values[..h] == old(values)[..h] && keys[h..] == old(keys)[h+1..] && -- cgit v1.2.3