Recased Dafny code per the current style guide.

formal-verification/seek.dfy → formal-verification/Seek.dfy

 // Types
 
 datatype Maybe<T> = Nothing | Just(value: T)
-datatype Seek = Seek(rating: nat, creation_time: nat)
+datatype Seek = Seek(rating: nat, creationTime: nat)
 datatype Event = Event(time: nat, first: Seek, second: Seek)
 
 // Uninterpreted Methods
 
-function method get_time_controls(seek: Seek): set<nat>
+function method GetTimeControls(seek: Seek): set<nat>
 
-predicate method can_pair(first: Seek, second: Seek)
+predicate method CanPair(first: Seek, second: Seek)
   ensures // trivial postcondition as reasoning hint
-    get_time_controls(first) * get_time_controls(second) == get_time_controls(second) * get_time_controls(first)
+    GetTimeControls(first) * GetTimeControls(second) == GetTimeControls(second) * GetTimeControls(first)
   ensures
-    can_pair(first, second) <==>
+    CanPair(first, second) <==>
     first != second &&
-    |get_time_controls(first) * get_time_controls(second)| > 0
+    |GetTimeControls(first) * GetTimeControls(second)| > 0
 
 // Helper Methods
 
-function method abs(value: int): nat
-  ensures abs(value) == value || abs(value) == -value
-function method min(first: nat, second: nat): nat
-  ensures min(first, second) == first || min(first, second) == second
-  ensures min(first, second) <= first
-  ensures min(first, second) <= second
+function method Abs(value: int): nat
+  ensures Abs(value) == value || Abs(value) == -value
+function method Min(first: nat, second: nat): nat
+  ensures Min(first, second) == first || Min(first, second) == second
+  ensures Min(first, second) <= first
+  ensures Min(first, second) <= second
 
-function method get_match_time(first: Seek, second: Seek): int
-  ensures get_match_time(first, second) == abs(first.rating - second.rating) + min(first.creation_time, second.creation_time)
+function method GetMatchTime(first: Seek, second: Seek): int
+  ensures GetMatchTime(first, second) == Abs(first.rating - second.rating) + Min(first.creationTime, second.creationTime)
 
-function method earliest(events: set<Event>): Event
+function method Earliest(events: set<Event>): Event
   requires |events| > 0
-  ensures earliest(events) in events
+  ensures Earliest(events) in events
   ensures
     forall e | e in events ::
-    earliest(events).time <= e.time
+    Earliest(events).time <= e.time
 
 // Class to Verify
 
 class Server {
-  ghost var oldest_seek: Maybe<Seek>;
+  ghost var oldestSeek: Maybe<Seek>;
   var seeks: set<Seek>;
   var events: set<Event>;
   var now: nat;
 
-  predicate no_future_seeks()
+  predicate NoFutureSeeks()
     reads this
   {
     forall s | s in this.seeks ::
-    s.creation_time <= this.now
+    s.creationTime <= this.now
   }
 
-  predicate no_past_events()
+  predicate NoPastEvents()
     reads this
   {
     forall e | e in this.events ::
     e.time >= this.now
   }
 
-  predicate no_reflexive_events()
+  predicate NoReflexiveEvents()
     reads this
   {
     forall e | e in this.events ::
     e.first != e.second
   }
 
-  predicate events_with_distinct_first_seeks()
+  predicate EventsWithDistinctFirstSeeks()
     reads this
   {
     forall e | e in this.events ::
@@ -73,101 +73,101 @@ class Server {
     e.first != f.first
   }
 
-  predicate no_early_timers()
+  predicate NoEarlyTimers()
     reads this
   {
     forall e | e in this.events ::
     (e.first in this.seeks && e.second in this.seeks) ==>
-    e.time == get_match_time(e.first, e.second)
+    e.time == GetMatchTime(e.first, e.second)
   }
 
-  predicate no_late_timers()
+  predicate NoLateTimers()
     reads this
   {
     forall s | s in this.seeks ::
     forall t | t in this.seeks ::
-    can_pair(s, t) ==>
+    CanPair(s, t) ==>
     exists e | e in this.events ::
     (e.first == s || e.first == t) &&
-    e.time <= get_match_time(s, t)
+    e.time <= GetMatchTime(s, t)
   }
 
-  predicate semistable()
+  predicate SemiStable()
     reads this
   {
-    this.no_future_seeks() &&
-    this.no_past_events() &&
-    this.no_reflexive_events() &&
-    this.events_with_distinct_first_seeks() &&
-    this.no_early_timers()
+    this.NoFutureSeeks() &&
+    this.NoPastEvents() &&
+    this.NoReflexiveEvents() &&
+    this.EventsWithDistinctFirstSeeks() &&
+    this.NoEarlyTimers()
   }
 
-  predicate stable()
+  predicate Stable()
     reads this
   {
-    this.no_future_seeks() &&
-    this.no_past_events() &&
-    this.no_reflexive_events() &&
-    this.events_with_distinct_first_seeks() &&
-    this.no_early_timers() &&
-    this.no_late_timers()
+    this.NoFutureSeeks() &&
+    this.NoPastEvents() &&
+    this.NoReflexiveEvents() &&
+    this.EventsWithDistinctFirstSeeks() &&
+    this.NoEarlyTimers() &&
+    this.NoLateTimers()
   }
 
   constructor()
-    ensures this.stable()
+    ensures this.Stable()
   {
-    this.oldest_seek := Nothing();
+    this.oldestSeek := Nothing();
     this.seeks := {};
     this.events := {};
     this.now := 0;
   }
 
-  method get_closest(seek: Seek) returns (closest: Maybe<Seek>)
-    requires this.stable()
-    ensures this.stable()
-    ensures closest.Nothing? <==> !exists s | s in this.seeks :: can_pair(seek, s)
+  method GetClosest(seek: Seek) returns (closest: Maybe<Seek>)
+    requires this.Stable()
+    ensures this.Stable()
+    ensures closest.Nothing? <==> !exists s | s in this.seeks :: CanPair(seek, s)
     ensures closest.Nothing? || closest.value in this.seeks
-    ensures closest.Nothing? || can_pair(seek, closest.value)
+    ensures closest.Nothing? || CanPair(seek, closest.value)
     ensures
       closest.Nothing? ||
       forall s | s in this.seeks ::
-      can_pair(seek, s) ==>
-      get_match_time(seek, closest.value) <= get_match_time(seek, s)
+      CanPair(seek, s) ==>
+      GetMatchTime(seek, closest.value) <= GetMatchTime(seek, s)
   {
     var result := Nothing;
     var remaining := this.seeks;
     while |remaining| > 0
       invariant remaining <= this.seeks
-      invariant result.Nothing? <==> !exists s | s in this.seeks - remaining :: can_pair(seek, s)
+      invariant result.Nothing? <==> !exists s | s in this.seeks - remaining :: CanPair(seek, s)
       invariant result.Nothing? || result.value in this.seeks
-      invariant result.Nothing? || can_pair(seek, result.value)
+      invariant result.Nothing? || CanPair(seek, result.value)
       invariant
         result.Nothing? ||
         forall s | s in this.seeks - remaining ::
-        can_pair(seek, s) ==>
-        get_match_time(seek, result.value) <= get_match_time(seek, s)
+        CanPair(seek, s) ==>
+        GetMatchTime(seek, result.value) <= GetMatchTime(seek, s)
     {
       var candidate :| candidate in remaining;
       remaining := remaining - {candidate};
-      if can_pair(seek, candidate) && (result.Nothing? || get_match_time(seek, candidate) < get_match_time(seek, result.value)) {
+      if CanPair(seek, candidate) && (result.Nothing? || GetMatchTime(seek, candidate) < GetMatchTime(seek, result.value)) {
         result := Just(candidate);
       }
     }
     return result;
   }
 
-  method pair(seek: Seek, closest: Seek)
-    requires this.semistable()
+  method Pair(seek: Seek, closest: Seek)
+    requires this.SemiStable()
     requires seek != closest
     requires seek in this.seeks
     requires closest in this.seeks
     requires
       forall s | s in this.seeks ::
       forall t | t in this.seeks ::
-      can_pair(s, t) ==>
-      get_match_time(seek, closest) <= get_match_time(s, t)
-    ensures this.semistable()
-    ensures this.oldest_seek == old(this.oldest_seek)
+      CanPair(s, t) ==>
+      GetMatchTime(seek, closest) <= GetMatchTime(s, t)
+    ensures this.SemiStable()
+    ensures this.oldestSeek == old(this.oldestSeek)
     ensures this.seeks == old(this.seeks) - {seek, closest}
     ensures this.events == old(this.events)
     ensures this.now == old(this.now)
@@ -176,8 +176,8 @@ class Server {
     this.seeks := this.seeks - {seek, closest};
   }
 
-  method add_seek(seek: Seek)
-    requires this.stable()
+  method AddSeek(seek: Seek)
+    requires this.Stable()
     requires
       forall s | s in seeks ::
       s != seek
@@ -187,64 +187,64 @@ class Server {
     requires
       forall e | e in this.events ::
       (e.first in this.seeks && e.second == seek) ==>
-      e.time == get_match_time(e.first, e.second)
-    requires seek.creation_time <= this.now
-    ensures this.stable()
+      e.time == GetMatchTime(e.first, e.second)
+    requires seek.creationTime <= this.now
+    ensures this.Stable()
     modifies this
   {
-    var closest := this.get_closest(seek);
+    var closest := this.GetClosest(seek);
     this.seeks := this.seeks + {seek};
     if closest.Nothing? {
-      this.oldest_seek := Just(seek);
+      this.oldestSeek := Just(seek);
     } else {
-      var match_time := get_match_time(seek, closest.value);
-      if match_time <= this.now {
-        this.pair(seek, closest.value);
+      var matchTime := GetMatchTime(seek, closest.value);
+      if matchTime <= this.now {
+        this.Pair(seek, closest.value);
       } else {
-        this.events := this.events + {Event(match_time, seek, closest.value)};
+        this.events := this.events + {Event(matchTime, seek, closest.value)};
       }
     }
   }
 
-  method remove_seek(seek: Seek)
-    requires this.stable()
-    ensures this.stable()
+  method RemoveSeek(seek: Seek)
+    requires this.Stable()
+    ensures this.Stable()
     modifies this
   {
     this.seeks := this.seeks - {seek};
   }
 
-  method seek(rating: nat)
-    requires this.stable()
+  method PlaceSeek(rating: nat)
+    requires this.Stable()
     requires
       forall s | s in seeks ::
       s != Seek(rating, this.now)
     requires
       forall e | e in this.events ::
       e.first != Seek(rating, this.now) && e.second != Seek(rating, this.now)
-    ensures this.stable()
+    ensures this.Stable()
     modifies this
   {
-    this.add_seek(Seek(rating, this.now));
+    this.AddSeek(Seek(rating, this.now));
   }
 
-  method tick()
-    requires this.stable()
+  method Tick()
+    requires this.Stable()
     requires |this.events| > 0
-    ensures this.stable()
+    ensures this.Stable()
     modifies this
   {
-    var event := earliest(this.events);
+    var event := Earliest(this.events);
     this.events := this.events - {event};
     this.now := event.time;
     var seek := event.first;
     var closest := event.second;
     if seek in this.seeks {
       if closest in this.seeks {
-        this.pair(seek, closest);
+        this.Pair(seek, closest);
       } else {
         this.seeks := this.seeks - {seek};
-        this.add_seek(seek);
+        this.AddSeek(seek);
       }
     }
   }