summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-01-03 17:18:58 -0800
committerGravatar Rustan Leino <unknown>2014-01-03 17:18:58 -0800
commita296062bc9a44d5207862a2f176f4745ff2413e9 (patch)
treecd6f32c721343c7ab5f852d9b1492d00d338e0d6 /Test
parent62d86b585e62485a327c29bd25ffefbb7a508218 (diff)
Changed BreadthFirstSearch example to no longer use "inductive naturals", sequences, or roll-it-yourself maps. Instead, use "nat", List, and "map".
Use VC splitting to combat performance issues.
Diffstat (limited to 'Test')
-rw-r--r--Test/vstte2012/Answer2
-rw-r--r--Test/vstte2012/BreadthFirstSearch.dfy216
-rw-r--r--Test/vstte2012/runtest.bat6
3 files changed, 102 insertions, 122 deletions
diff --git a/Test/vstte2012/Answer b/Test/vstte2012/Answer
index bca270c3..43eddcb1 100644
--- a/Test/vstte2012/Answer
+++ b/Test/vstte2012/Answer
@@ -21,4 +21,4 @@ Dafny program verifier finished with 15 verified, 0 errors
-------------------- BreadthFirstSearch.dfy --------------------
-Dafny program verifier finished with 24 verified, 0 errors
+Dafny program verifier finished with 22 verified, 0 errors
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index ac070ac6..535a7d90 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -6,15 +6,14 @@ class BreadthFirstSearch<Vertex(==)>
// This is the definition of what it means to be a path "p" from vertex
// "source" to vertex "dest"
- function IsPath(source: Vertex, dest: Vertex, p: seq<Vertex>): bool
+ predicate IsPath(source: Vertex, dest: Vertex, p: List<Vertex>)
{
- if source == dest then
- p == []
- else
- p != [] && dest in Succ(p[|p|-1]) && IsPath(source, p[|p|-1], p[..|p|-1])
+ match p
+ case Nil => source == dest
+ case Cons(v, tail) => dest in Succ(v) && IsPath(source, v, tail)
}
- function IsClosed(S: set<Vertex>): bool // says that S is closed under Succ
+ predicate IsClosed(S: set<Vertex>) // says that S is closed under Succ
{
forall v :: v in S ==> Succ(v) <= S
}
@@ -25,7 +24,7 @@ class BreadthFirstSearch<Vertex(==)>
// witness. The method could equally well have been written using an
// existential quantifier and no ghost out-parameter.
method BFS(source: Vertex, dest: Vertex, ghost AllVertices: set<Vertex>)
- returns (d: int, ghost path: seq<Vertex>)
+ returns (d: int, ghost path: List<Vertex>)
// source and dest are among AllVertices
requires source in AllVertices && dest in AllVertices;
// AllVertices is closed under Succ
@@ -34,14 +33,15 @@ class BreadthFirstSearch<Vertex(==)>
// More precisely, "d" is non-negative iff "source" can reach "dest".
// The following postcondition says that under the "0 <= d" outcome,
// "path" denotes a path of length "d" from "source" to "dest":
- ensures 0 <= d ==> IsPath(source, dest, path) && |path| == d;
+ ensures 0 <= d ==> IsPath(source, dest, path) && length(path) == d;
// Moreover, that path is as short as any path from "source" to "dest":
- ensures 0 <= d ==> forall p :: IsPath(source, dest, p) ==> |path| <= |p|;
+ ensures 0 <= d ==> forall p :: IsPath(source, dest, p) ==> length(path) <= length(p);
// Finally, under the outcome "d < 0", there is no path from "source" to "dest":
ensures d < 0 ==> !exists p :: IsPath(source, dest, p);
{
var V, C, N := {source}, {source}, {};
- ghost var Processed, paths := {}, Maplet({source}, source, [], Empty);
+ ghost var Processed, paths := {}, map[source := Nil];
+ assert domain(paths) == {source};
// V - all encountered vertices
// Processed - vertices reachable from "source" is at most "d" steps
// C - unprocessed vertices reachable from "source" in "d" steps
@@ -49,8 +49,7 @@ class BreadthFirstSearch<Vertex(==)>
// N - vertices encountered and reachable from "source" in "d+1" steps
// (but no less)
d := 0;
- var dd := Zero;
- while (C != {})
+ while C != {}
// V, Processed, C, N are all subsets of AllVertices:
invariant V <= AllVertices && Processed <= AllVertices && C <= AllVertices && N <= AllVertices;
// source is encountered:
@@ -60,20 +59,18 @@ class BreadthFirstSearch<Vertex(==)>
invariant Processed !! C !! N; // Processed, C, and N are mutually disjoint
// "paths" records a path for every encountered vertex
invariant ValidMap(source, paths);
- invariant V == Domain(paths);
+ invariant V == domain(paths);
// shortest paths for vertices in C have length d, and for vertices in N
// have length d+1
- invariant forall x :: x in C ==> |Find(source, x, paths)| == d;
- invariant forall x :: x in N ==> |Find(source, x, paths)| == d + 1;
- // "dd" is just an inductive-looking way of writing "d":
- invariant Value(dd) == d;
+ invariant forall x :: x in C ==> length(Find(source, x, paths)) == d;
+ invariant forall x :: x in N ==> length(Find(source, x, paths)) == d + 1;
// "dest" is not reachable for any smaller value of "d":
- invariant dest in R(source, dd, AllVertices) ==> dest in C;
- invariant d != 0 ==> dest !in R(source, dd.predecessor, AllVertices);
+ invariant dest in R(source, d, AllVertices) ==> dest in C;
+ invariant d != 0 ==> dest !in R(source, d-1, AllVertices);
// together, Processed and C are all the vertices reachable in at most d steps:
- invariant Processed + C == R(source, dd, AllVertices);
+ invariant Processed + C == R(source, d, AllVertices);
// N are the successors of Processed that are not reachable within d steps:
- invariant N == Successors(Processed, AllVertices) - R(source, dd, AllVertices);
+ invariant N == Successors(Processed, AllVertices) - R(source, d, AllVertices);
// if we have exhausted C, then we have also exhausted N:
invariant C == {} ==> N == {};
// variant:
@@ -84,15 +81,14 @@ class BreadthFirstSearch<Vertex(==)>
C, Processed := C - {v}, Processed + {v};
ghost var pathToV := Find(source, v, paths);
- if (v == dest) {
+ if v == dest {
forall p | IsPath(source, dest, p)
- ensures |pathToV| <= |p|;
+ ensures length(pathToV) <= length(p);
{
Lemma_IsPath_R(source, dest, p, AllVertices);
- if (|p| < |pathToV|) {
+ if length(p) < length(pathToV) {
// show that this branch is impossible
- ToNat_Value_Bijection(|p|);
- RMonotonicity(source, ToNat(|p|), dd.predecessor, AllVertices);
+ RMonotonicity(source, length(p), d-1, AllVertices);
}
}
return d, pathToV;
@@ -103,20 +99,20 @@ class BreadthFirstSearch<Vertex(==)>
V, N := V + newlyEncountered, N + newlyEncountered;
paths := UpdatePaths(newlyEncountered, source, paths, v, pathToV);
- if (C == {}) {
- C, N, d, dd := N, {}, d+1, Suc(dd);
+ if C == {} {
+ C, N, d := N, {}, d+1;
}
}
// show that "dest" in not in any reachability set, no matter
// how many successors one follows
- forall nn
- ensures dest !in R(source, nn, AllVertices);
+ forall n: nat
+ ensures dest !in R(source, n, AllVertices);
{
- if (Value(nn) < Value(dd)) {
- RMonotonicity(source, nn, dd, AllVertices);
+ if n < d {
+ RMonotonicity(source, n, d, AllVertices);
} else {
- IsReachFixpoint(source, dd, nn, AllVertices);
+ IsReachFixpoint(source, d, n, AllVertices);
}
}
@@ -129,7 +125,7 @@ class BreadthFirstSearch<Vertex(==)>
{
Lemma_IsPath_R(source, dest, p, AllVertices);
// a consequence of Lemma_IsPath_R is:
- // dest in R(source, ToNat(|p|), AllVertices)
+ // dest in R(source, |p|), AllVertices)
// but that contradicts the conclusion of the preceding forall statement
}
@@ -138,46 +134,24 @@ class BreadthFirstSearch<Vertex(==)>
// property of IsPath
- ghost method Lemma_IsPath_Closure(source: Vertex, dest: Vertex,
- p: seq<Vertex>, AllVertices: set<Vertex>)
+ lemma Lemma_IsPath_Closure(source: Vertex, dest: Vertex,
+ p: List<Vertex>, AllVertices: set<Vertex>)
requires IsPath(source, dest, p) && source in AllVertices && IsClosed(AllVertices);
- ensures dest in AllVertices && forall v :: v in p ==> v in AllVertices;
+ ensures dest in AllVertices && forall v :: v in elements(p) ==> v in AllVertices;
{
- if (p != []) {
- var last := |p| - 1;
- Lemma_IsPath_Closure(source, p[last], p[..last], AllVertices);
+ match p {
+ case Nil =>
+ case Cons(v, tail) =>
+ Lemma_IsPath_Closure(source, v, tail, AllVertices);
}
}
- // operations on Nat
-
- function Value(nn: Nat): nat
- ensures ToNat(Value(nn)) == nn;
- {
- match nn
- case Zero => 0
- case Suc(mm) => Value(mm) + 1
- }
-
- function ToNat(n: nat): Nat
- {
- if n == 0 then Zero else Suc(ToNat(n - 1))
- }
-
- ghost method ToNat_Value_Bijection(n: nat)
- ensures Value(ToNat(n)) == n;
- {
- // Dafny automatically figures out the inductive proof of the postcondition
- }
-
// Reachability
- function R(source: Vertex, nn: Nat, AllVertices: set<Vertex>): set<Vertex>
+ function R(source: Vertex, n: nat, AllVertices: set<Vertex>): set<Vertex>
{
- match nn
- case Zero => {source}
- case Suc(mm) => R(source, mm, AllVertices) +
- Successors(R(source, mm, AllVertices), AllVertices)
+ if n == 0 then {source} else
+ R(source, n-1, AllVertices) + Successors(R(source, n-1, AllVertices), AllVertices)
}
function Successors(S: set<Vertex>, AllVertices: set<Vertex>): set<Vertex>
@@ -185,92 +159,94 @@ class BreadthFirstSearch<Vertex(==)>
set w | w in AllVertices && exists x :: x in S && w in Succ(x)
}
- ghost method RMonotonicity(source: Vertex, mm: Nat, nn: Nat, AllVertices: set<Vertex>)
- requires Value(mm) <= Value(nn);
- ensures R(source, mm, AllVertices) <= R(source, nn, AllVertices);
- decreases Value(nn) - Value(mm);
+ lemma RMonotonicity(source: Vertex, m: nat, n: nat, AllVertices: set<Vertex>)
+ requires m <= n;
+ ensures R(source, m, AllVertices) <= R(source, n, AllVertices);
+ decreases n - m;
{
- if (Value(mm) < Value(nn)) {
- RMonotonicity(source, Suc(mm), nn, AllVertices);
+ if m < n {
+ RMonotonicity(source, m + 1, n, AllVertices);
}
}
- ghost method IsReachFixpoint(source: Vertex, mm: Nat, nn: Nat, AllVertices: set<Vertex>)
- requires R(source, mm, AllVertices) == R(source, Suc(mm), AllVertices);
- requires Value(mm) <= Value(nn);
- ensures R(source, mm, AllVertices) == R(source, nn, AllVertices);
- decreases Value(nn) - Value(mm);
+ lemma IsReachFixpoint(source: Vertex, m: nat, n: nat, AllVertices: set<Vertex>)
+ requires R(source, m, AllVertices) == R(source, m+1, AllVertices);
+ requires m <= n;
+ ensures R(source, m, AllVertices) == R(source, n, AllVertices);
+ decreases n - m;
{
- if (Value(mm) < Value(nn)) {
- IsReachFixpoint(source, Suc(mm), nn, AllVertices);
+ if m < n {
+ IsReachFixpoint(source, m + 1, n, AllVertices);
}
}
- ghost method Lemma_IsPath_R(source: Vertex, x: Vertex,
- p: seq<Vertex>, AllVertices: set<Vertex>)
+ lemma Lemma_IsPath_R(source: Vertex, x: Vertex, p: List<Vertex>, AllVertices: set<Vertex>)
requires IsPath(source, x, p) && source in AllVertices && IsClosed(AllVertices);
- ensures x in R(source, ToNat(|p|), AllVertices);
+ ensures x in R(source, length(p), AllVertices);
{
- if (p != []) {
- Lemma_IsPath_Closure(source, x, p, AllVertices);
- var last := |p| - 1;
- Lemma_IsPath_R(source, p[last], p[..last], AllVertices);
+ match p {
+ case Nil =>
+ case Cons(v, tail) =>
+ Lemma_IsPath_Closure(source, x, p, AllVertices);
+ Lemma_IsPath_R(source, v, tail, AllVertices);
}
}
- // operations on Map's
-
- function Domain(m: Map<Vertex>): set<Vertex>
- {
-// if m.Maplet? then m.dom else {}
-// if m == Empty then {} else assert m.Maplet?; m.dom
- match m
- case Empty => {}
- case Maplet(dom, t, s, nxt) => dom
- }
-
// ValidMap encodes the consistency of maps (think, invariant).
// An explanation of this idiom is explained in the README file.
- function ValidMap(source: Vertex, m: Map<Vertex>): bool
+ predicate ValidMap(source: Vertex, m: map<Vertex, List<Vertex>>)
{
- match m
- case Empty => true
- case Maplet(dom, v, path, next) =>
- v in dom && dom == Domain(next) + {v} &&
- IsPath(source, v, path) &&
- ValidMap(source, next)
+ forall v :: v in m ==> IsPath(source, v, m[v])
}
- function Find(source: Vertex, x: Vertex, m: Map<Vertex>): seq<Vertex>
- requires ValidMap(source, m) && x in Domain(m);
+ function Find(source: Vertex, x: Vertex, m: map<Vertex, List<Vertex>>): List<Vertex>
+ requires ValidMap(source, m) && x in m;
ensures IsPath(source, x, Find(source, x, m));
{
- match m
- case Maplet(dom, v, path, next) =>
- if x == v then path else Find(source, x, next)
+ m[x]
}
ghost method UpdatePaths(vSuccs: set<Vertex>, source: Vertex,
- paths: Map<Vertex>, v: Vertex, pathToV: seq<Vertex>)
- returns (newPaths: Map<Vertex>)
+ paths: map<Vertex, List<Vertex>>, v: Vertex, pathToV: List<Vertex>)
+ returns (newPaths: map<Vertex, List<Vertex>>)
requires ValidMap(source, paths);
- requires vSuccs !! Domain(paths);
- requires forall succ :: succ in vSuccs ==> IsPath(source, succ, pathToV + [v]);
- ensures ValidMap(source, newPaths) && Domain(newPaths) == Domain(paths) + vSuccs;
- ensures forall x :: x in Domain(paths) ==>
+ requires vSuccs !! domain(paths);
+ requires forall succ :: succ in vSuccs ==> IsPath(source, succ, Cons(v, pathToV));
+ ensures ValidMap(source, newPaths) && domain(newPaths) == domain(paths) + vSuccs;
+ ensures forall x :: x in paths ==>
Find(source, x, paths) == Find(source, x, newPaths);
- ensures forall x :: x in vSuccs ==> Find(source, x, newPaths) == pathToV + [v];
+ ensures forall x :: x in vSuccs ==> Find(source, x, newPaths) == Cons(v, pathToV);
{
- if (vSuccs == {}) {
+ if vSuccs == {} {
newPaths := paths;
} else {
var succ :| succ in vSuccs;
- newPaths := Maplet(Domain(paths) + {succ}, succ, pathToV + [v], paths);
+ newPaths := paths[succ := Cons(v, pathToV)];
+ assert domain(newPaths) == domain(paths) + {succ};
newPaths := UpdatePaths(vSuccs - {succ}, source, newPaths, v, pathToV);
}
}
}
-datatype Map<T> = Empty | Maplet(dom: set<T>, T, seq<T>, next: Map<T>);
+static function domain<T, U>(m: map<T, U>): set<T>
+{
+ set t | t in m
+}
+
+datatype List<T> = Nil | Cons(head: T, tail: List)
+
+static function length(list: List): nat
+{
+ match list
+ case Nil => 0
+ case Cons(_, tail) => 1 + length(tail)
+}
+
+static function elements<T>(list: List<T>): set<T>
+{
+ match list
+ case Nil => {}
+ case Cons(x, tail) => {x} + elements(tail)
+}
-datatype Nat = Zero | Suc(predecessor: Nat);
+datatype Nat = Zero | Suc(predecessor: Nat)
diff --git a/Test/vstte2012/runtest.bat b/Test/vstte2012/runtest.bat
index 5d7953cc..7e597fd4 100644
--- a/Test/vstte2012/runtest.bat
+++ b/Test/vstte2012/runtest.bat
@@ -4,7 +4,11 @@ setlocal
set BINARIES=..\..\Binaries
set DAFNY_EXE=%BINARIES%\Dafny.exe
-%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Two-Way-Sort.dfy Combinators.dfy RingBuffer.dfy RingBufferAuto.dfy Tree.dfy BreadthFirstSearch.dfy
+%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /verifySeparately %* Two-Way-Sort.dfy Combinators.dfy RingBuffer.dfy RingBufferAuto.dfy Tree.dfy
+
+echo.
+echo -------------------- BreadthFirstSearch.dfy --------------------
+%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp /vcsMaxKeepGoingSplits:10 %* BreadthFirstSearch.dfy
rem for %%f in (
rem Two-Way-Sort.dfy