From 572b11dddba3bfbdc4e90beb4d7f2e076878f717 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 21 May 2010 18:38:47 +0000 Subject: Dafny: * Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks --- Test/VSI-Benchmarks/Answer | 2 +- Test/VSI-Benchmarks/b2.dfy | 74 +++++++++++----------------------------------- Test/VSI-Benchmarks/b3.dfy | 3 -- Test/VSI-Benchmarks/b4.dfy | 1 - Test/VSI-Benchmarks/b7.dfy | 1 - Test/VSI-Benchmarks/b8.dfy | 2 -- 6 files changed, 19 insertions(+), 64 deletions(-) (limited to 'Test/VSI-Benchmarks') diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index 1efeba04..2a4587f4 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -5,7 +5,7 @@ Dafny program verifier finished with 10 verified, 0 errors -------------------- b2.dfy -------------------- -Dafny program verifier finished with 12 verified, 0 errors +Dafny program verifier finished with 6 verified, 0 errors -------------------- b3.dfy -------------------- diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index ec255ed1..fd20a72b 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -1,27 +1,23 @@ -// Note:Implemented arrays as Dafny does not provide them - class Benchmark2 { - method BinarySearch(a: Array, key: int) returns (result: int) + method BinarySearch(a: array, key: int) returns (result: int) requires a != null; - requires (forall i, j :: - 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j)); - ensures -1 <= result && result < a.Length(); - ensures 0 <= result ==> a.Get(result) == key; - ensures result == -1 ==> - (forall i :: 0 <= i && i < a.Length() ==> a.Get(i) != key); + requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]); + ensures -1 <= result && result < |a|; + ensures 0 <= result ==> a[result] == key; + ensures result == -1 ==> (forall i :: 0 <= i && i < |a| ==> a[i] != key); { var low := 0; - var high := a.Length(); + var high := |a|; while (low < high) - invariant 0 <= low && low <= high && high <= a.Length(); - invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key); - invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i)); + invariant 0 <= low && low <= high && high <= |a|; + invariant (forall i :: 0 <= i && i < low ==> a[i] < key); + invariant (forall i :: high <= i && i < |a| ==> key < a[i]); decreases high - low; { var mid := low + (high - low) / 2; - var midVal := a.Get(mid); + var midVal := a[mid]; if (midVal < key) { low := mid + 1; @@ -36,47 +32,13 @@ class Benchmark2 { } } -class Array { - var contents: seq; - method Init(n: int) - requires 0 <= n; - modifies this; - ensures |contents| == n; - { - var i := 0; - contents := []; - while (i < n) - invariant i <= n && i == |contents|; - decreases n - i; - { - contents := contents + [0]; - i := i + 1; - } - } - function method Length(): int - reads this; - { |contents| } - function method Get(i: int): int - requires 0 <= i && i < |contents|; - reads this; - { contents[i] } - method Set(i: int, x: int) - requires 0 <= i && i < |contents|; - modifies this; - ensures contents == old(contents)[i := x]; - { - contents := contents[i := x]; - } -} - method Main() { - var a := new Array; - call a.Init(5); - call a.Set(0, -4); - call a.Set(1, -2); - call a.Set(2, -2); - call a.Set(3, 0); - call a.Set(4, 25); + var a := new int[5]; + a[0] := -4; + a[1] := -2; + a[2] := -2; + a[3] := 0; + a[4] := 25; call TestSearch(a, 4); call TestSearch(a, -8); call TestSearch(a, -2); @@ -86,9 +48,9 @@ method Main() { call TestSearch(a, 27); } -method TestSearch(a: Array, key: int) +method TestSearch(a: array, key: int) requires a != null; - requires (forall i, j :: 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j)); + requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]); { var b := new Benchmark2; call r := b.BinarySearch(a, key); diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 37b73cba..6d9c3ddd 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -64,7 +64,6 @@ class Benchmark3 { invariant n <= |q.contents|; invariant n == |p|; invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i); - decreases |q.contents| - n; { p := p + [n]; n := n + 1; @@ -121,7 +120,6 @@ class Benchmark3 { 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 - decreases n-j; { call x:= q.Dequeue(); call q.Enqueue(x); @@ -134,7 +132,6 @@ class Benchmark3 { while (j < k) invariant j <= k; invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; - decreases k-j; { call x := q.Dequeue(); call q.Enqueue(x); diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index ab1285f6..d2fca9bc 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -95,7 +95,6 @@ class Map { while (j < |keys|) invariant j <= |keys|; invariant key !in keys[..j]; - decreases |keys| -j; { if (keys[j] == key) { idx := j; diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index e5af6357..2304e602 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -142,7 +142,6 @@ class Client { call wr.Create(); while (0 < |q.contents|) invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint; - decreases |q.contents|; { call ch := q.Dequeue(); call wr.PutChar(ch); diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index d8ee2013..34e0cfef 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -104,7 +104,6 @@ class Glossary { invariant q !in wr.footprint; invariant qcon == q.contents; invariant (forall k :: k in q.contents ==> k in glossary.keys); - decreases |definition| -i; { var w := definition[i]; call present, d := glossary.Find(w); @@ -342,7 +341,6 @@ class Map { while (j < |keys|) invariant j <= |keys|; invariant key !in keys[..j]; - decreases |keys| -j; { if (keys[j] == key) { idx := j; -- cgit v1.2.3