Update library state machine example

Author: tchajed

src/examples/library.dfy

@@ -6,9 +6,6 @@
 datatype Status = Shelf | Patron(name: string)
 datatype Book = Book(title: string)
 
-// no constants
-datatype Constants = Constants()
-
 // The state of the whole library is just the status of every book owned by the
 // library.
 datatype Variables = Variables(library: map<Book, Status>)
@@ -17,7 +14,7 @@ datatype Variables = Variables(library: map<Book, Status>)
   // a set of _member functions_, which can be called as v.f(), just like Java,
   // C++, or Rust methods. Just like in Java or C++, the body can use the `this`
   // keyword to refer to an implicit argument of type Variables.
-  ghost predicate WellFormed(c: Constants)
+  ghost predicate WellFormed()
   {
     // New syntax (x in m for maps): maps have a domain and we can write x in m
     // to say x is in the domain of m (similarly, `x !in m` is a more readable
@@ -30,20 +27,20 @@ datatype Variables = Variables(library: map<Book, Status>)
   }
 }
 
-ghost predicate Init(c: Constants, v: Variables)
+ghost predicate Init(v: Variables)
 {
-  && v.WellFormed(c)
+  && v.WellFormed()
   && forall b :: b in v.library ==> v.library[b].Shelf?
 }
 
 // The transitions of the library state machine.
 
 datatype Step = Checkout(b: Book, to: string) | Return(b: Book)
 
-ghost predicate CheckoutStep(c: Constants, v: Variables, v': Variables, step: Step)
+ghost predicate CheckoutStep(v: Variables, v': Variables, step: Step)
   requires step.Checkout?
 {
-  && v.WellFormed(c)
+  && v.WellFormed()
   && step.b in v.library
   && v.library[step.b].Shelf?
      // New syntax (datatype update): here we define the new Variables from the old
@@ -53,28 +50,33 @@ ghost predicate CheckoutStep(c: Constants, v: Variables, v': Variables, step: St
   && v' == v.(library := v.library[step.b := Patron(step.to)])
 }
 
-ghost predicate ReturnStep(c: Constants, v: Variables, v': Variables, step: Step)
+ghost predicate ReturnStep(v: Variables, v': Variables, step: Step)
   requires step.Return?
 {
-  && v.WellFormed(c)
+  && v.WellFormed()
   && step.b in v.library
   && v.library[step.b].Patron?
   && v' == v.(library := v.library[step.b := Shelf])
 }
 
-ghost predicate NextStep(c: Constants, v: Variables, v': Variables, step: Step)
+ghost predicate NextStep(v: Variables, v': Variables, step: Step)
 {
   match step {
-    case Checkout(_, _) => CheckoutStep(c, v, v', step)
-    case Return(_) => ReturnStep(c, v, v', step)
+    case Checkout(_, _) => CheckoutStep(v, v', step)
+    case Return(_) => ReturnStep(v, v', step)
   }
 }
 
-ghost predicate Next(c: Constants, v: Variables, v': Variables)
+ghost predicate Next(v: Variables, v': Variables)
 {
-  exists step :: NextStep(c, v, v', step)
+  exists step :: NextStep(v, v', step)
 }
 
+lemma NextStepDeterministicGivenStep(v:Variables, v':Variables, step: Step)
+  requires NextStep(v, v', step)
+  ensures forall v'' | NextStep(v, v'', step) :: v' == v''
+{}
+
 /*
 In this lemma we'll write a concrete sequence of states which forms a (short)
 execution of this state machine, and prove that it really is an execution.
@@ -83,24 +85,23 @@ This can be a good sanity check on the definitions (for example, to make sure
 that it's at least possible to take every transition).
 */
 lemma ExampleExec() {
-  var c := Constants();
   var e := [
-    Variables(map[Book("Snow Crash") := Shelf, Book("The Stand") := Shelf]),
-    Variables(map[Book("Snow Crash") := Patron("Jon"), Book("The Stand") := Shelf]),
-    Variables(map[Book("Snow Crash") := Patron("Jon"), Book("The Stand") := Patron("Tej")]),
-    Variables(map[Book("Snow Crash") := Shelf, Book("The Stand") := Patron("Tej")])
+    Variables(library := map[Book("Snow Crash") := Shelf, Book("The Stand") := Shelf]),
+    Variables(library := map[Book("Snow Crash") := Patron("Jon"), Book("The Stand") := Shelf]),
+    Variables(library := map[Book("Snow Crash") := Patron("Jon"), Book("The Stand") := Patron("Tej")]),
+    Variables(library := map[Book("Snow Crash") := Shelf, Book("The Stand") := Patron("Tej")])
   ];
 
   // Next we'll prove that e is a valid execution.
 
-  assert Init(c, e[0]);
+  assert Init(e[0]);
 
   // These steps will be witnesses to help prove Next between every pair of Variables.
   var steps := [
     Checkout(Book("Snow Crash"), "Jon"),
     Checkout(Book("The Stand"), "Tej"),
     Return(Book("Snow Crash"))
   ];
-  assert forall n: nat | n < |e|-1  :: NextStep(c, e[n], e[n+1], steps[n]);
-  assert forall n: nat | n < |e|-1  :: Next(c, e[n], e[n+1]);
+  assert forall n: nat | n < |e|-1  :: NextStep(e[n], e[n+1], steps[n]);
+  assert forall n: nat | n < |e|-1  :: Next(e[n], e[n+1]);
 }