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.

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