From a296062bc9a44d5207862a2f176f4745ff2413e9 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 3 Jan 2014 17:18:58 -0800 Subject: 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. --- Test/vstte2012/Answer | 2 +- Test/vstte2012/BreadthFirstSearch.dfy | 216 +++++++++++++++------------------- Test/vstte2012/runtest.bat | 6 +- 3 files changed, 102 insertions(+), 122 deletions(-) (limited to 'Test') 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 // 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): bool + predicate IsPath(source: Vertex, dest: Vertex, p: List) { - 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): bool // says that S is closed under Succ + predicate IsClosed(S: set) // says that S is closed under Succ { forall v :: v in S ==> Succ(v) <= S } @@ -25,7 +24,7 @@ class BreadthFirstSearch // 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) - returns (d: int, ghost path: seq) + returns (d: int, ghost path: List) // source and dest are among AllVertices requires source in AllVertices && dest in AllVertices; // AllVertices is closed under Succ @@ -34,14 +33,15 @@ class BreadthFirstSearch // 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 // 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 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 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 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 { 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 // property of IsPath - ghost method Lemma_IsPath_Closure(source: Vertex, dest: Vertex, - p: seq, AllVertices: set) + lemma Lemma_IsPath_Closure(source: Vertex, dest: Vertex, + p: List, AllVertices: set) 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): set + function R(source: Vertex, n: nat, AllVertices: set): set { - 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, AllVertices: set): set @@ -185,92 +159,94 @@ class BreadthFirstSearch 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) - 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) + 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) - 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) + 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, AllVertices: set) + lemma Lemma_IsPath_R(source: Vertex, x: Vertex, p: List, AllVertices: set) 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): set - { -// 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): bool + predicate ValidMap(source: Vertex, m: map>) { - 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): seq - requires ValidMap(source, m) && x in Domain(m); + function Find(source: Vertex, x: Vertex, m: map>): List + 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, source: Vertex, - paths: Map, v: Vertex, pathToV: seq) - returns (newPaths: Map) + paths: map>, v: Vertex, pathToV: List) + returns (newPaths: map>) 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 = Empty | Maplet(dom: set, T, seq, next: Map); +static function domain(m: map): set +{ + set t | t in m +} + +datatype List = 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(list: List): set +{ + 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 -- cgit v1.2.3