Added starter code the formal verification homework.

formal-verification/a_strength_to_depth.dfy

+// Types
+
+type StrengthDepthPair(==)
+function method get_strength(pair: StrengthDepthPair): real
+function method get_depth(pair: StrengthDepthPair): real
+
+// Program Constants
+
+const STRENGTH_DEPTH_PAIRS: seq<StrengthDepthPair>
+
+// Constants to Make Assertions Easier to Write
+
+const MINIMUM_STRENGTH: real
+const MAXIMUM_STRENGTH: real
+const MINIMUM_DEPTH: real
+const MAXIMUM_DEPTH: real
+
+// Helper Methods
+
+method interpolate_depth(low_strength: real, high_strength: real, low_depth: real, high_depth: real, strength: real) returns (depth: real)
+  requires low_strength < high_strength
+  requires low_depth < high_depth
+  requires low_strength <= strength <= high_strength
+  ensures low_depth <= depth <= high_depth
+{
+  // break the computation into steps so that Dafny can trigger on individual subexpressions.
+  var numerator := strength - low_strength;
+  var denominator := high_strength - low_strength;
+  var ratio := numerator / denominator;
+  var range := high_depth - low_depth;
+  return low_depth + range * numerator / denominator;
+}
+
+// Method to Verify
+
+method strength_to_depth(strength: real) returns (depth: real)
+  requires |STRENGTH_DEPTH_PAIRS| >= 2
+  requires
+    forall i | 0 <= i < |STRENGTH_DEPTH_PAIRS| ::
+    get_strength(STRENGTH_DEPTH_PAIRS[i]) > 0.0
+  requires get_strength(STRENGTH_DEPTH_PAIRS[0]) == MINIMUM_STRENGTH
+  requires
+    forall i | 0 <= i < |STRENGTH_DEPTH_PAIRS| ::
+    forall j | i < j < |STRENGTH_DEPTH_PAIRS| ::
+    get_strength(STRENGTH_DEPTH_PAIRS[i]) < get_strength(STRENGTH_DEPTH_PAIRS[j])
+  requires get_strength(STRENGTH_DEPTH_PAIRS[|STRENGTH_DEPTH_PAIRS| - 1]) == MAXIMUM_STRENGTH
+  requires
+    forall i | 0 <= i < |STRENGTH_DEPTH_PAIRS| ::
+    get_depth(STRENGTH_DEPTH_PAIRS[i]) > 0.0
+  requires get_depth(STRENGTH_DEPTH_PAIRS[0]) == MINIMUM_DEPTH
+  requires
+    forall i | 0 <= i < |STRENGTH_DEPTH_PAIRS| ::
+    forall j | i < j < |STRENGTH_DEPTH_PAIRS| ::
+    get_depth(STRENGTH_DEPTH_PAIRS[i]) < get_depth(STRENGTH_DEPTH_PAIRS[j])
+  requires get_depth(STRENGTH_DEPTH_PAIRS[|STRENGTH_DEPTH_PAIRS| - 1]) == MAXIMUM_DEPTH
+  ensures MINIMUM_DEPTH <= depth <= MAXIMUM_DEPTH
+  ensures strength < MINIMUM_STRENGTH ==> depth == MINIMUM_DEPTH
+  ensures strength > MAXIMUM_STRENGTH ==> depth == MAXIMUM_DEPTH
+  ensures
+    MINIMUM_DEPTH < depth < MAXIMUM_DEPTH ==>
+    exists i | 0 <= i < |STRENGTH_DEPTH_PAIRS| - 1 ::
+    get_strength(STRENGTH_DEPTH_PAIRS[i]) <= strength <= get_strength(STRENGTH_DEPTH_PAIRS[i + 1]) &&
+    get_depth(STRENGTH_DEPTH_PAIRS[i]) <= depth <= get_depth(STRENGTH_DEPTH_PAIRS[i + 1])
+{
+  // TODO: Replace this comment with a translation of the JavaScript function `onSetStrength` that returns the chosen depth.
+}
+
+// Original JavaScript
+
+// onSetStrength(strength) {
+//   for (let i = 0; i < STRENGTH_DEPTH_PAIRS.length - 1; ++i) {
+//     const [lowStrength, lowDepth] = STRENGTH_DEPTH_PAIRS[i];
+//     const [highStrength, highDepth] = STRENGTH_DEPTH_PAIRS[i + 1];
+//     if (lowStrength <= strength && strength <= highStrength) {
+//       this.depth = lowDepth + (highDepth - lowDepth) * (strength - lowStrength) / (highStrength - lowStrength);
+//       return;
+//     }
+//   }
+//   this.depth = strength < STRENGTH_DEPTH_PAIRS[0][0] ?
+//     STRENGTH_DEPTH_PAIRS[0][1] :
+//     STRENGTH_DEPTH_PAIRS[STRENGTH_DEPTH_PAIRS.length - 1][1];
+// }

formal-verification/b_rotated_range.dfy

+// Generator Method to Verify
+
+// Based on the following signature, Dafny automatically creates a ghost variable called `values` to hold everything yielded so far.
+iterator rotated_range(start: nat, end: nat, rotation: nat) yields (value: nat)
+  requires start <= end
+  requires rotation <= end - start
+  ensures |values| == end - start
+  ensures
+    forall i | 0 <= i < end - (start + rotation) ::
+    values[i] == start + rotation + i
+  ensures
+    forall i | end - (start + rotation) <= i < |values| ::
+    values[i] == start + i - end + (start + rotation)
+{
+  var value: nat := start + rotation;
+  while value < end {
+    yield value;
+    value := value + 1;
+  }
+  value := start;
+  while value < start + rotation {
+    yield value;
+    value := value + 1;
+  }
+}
+
+// Original JavaScript
+
+// export function*rotatedRange(start, end, rotation) {
+//   for (let value = start + rotation; value < end; ++value) {
+//     yield value;
+//   }
+//   for (let value = start; value < start + rotation; ++value) {
+//     yield value;
+//   }
+// }

formal-verification/c_delimited_combinations.dfy

+// Types
+
+type Variant(==)
+
+// Language Constants
+
+const undefined: string
+
+// Functions to Make Assertions Easier to Write
+
+function parts(text: string): seq<string>
+
+// Library Methods
+
+function method join(strings: seq<string>, delimiter: string): string
+  ensures parts(join(strings, delimiter)) == strings
+
+// Helper Methods
+
+function method product(collections: seq<seq<Variant>>): seq<seq<Variant>>
+  ensures
+    forall combination | combination in product(collections) ::
+    |combination| == |collections|
+  ensures
+    forall combination | combination in product(collections) ::
+    forall i | 0 <= i < |combination| :: combination[i] in collections[i]
+  ensures
+    forall combination: seq<Variant> | |combination| == |collections| ::
+    (forall i | 0 <= i < |combination| :: combination[i] in collections[i]) ==>
+    combination in product(collections)
+
+// Method to Verify
+
+method delimited_combinations(template: seq<Variant> -> string, delimiter: string, collections: seq<seq<Variant>>) returns (text: string)
+  ensures
+    forall part | part in parts(text) ::
+    exists combination | |combination| == |collections| && template(combination) == part ::
+    forall i | 0 <= i < |combination| :: combination[i] in collections[i]
+  ensures
+    forall combination: seq<Variant> | |combination| == |collections| ::
+    (forall i | 0 <= i < |combination| :: combination[i] in collections[i]) ==>
+    template(combination) == undefined || template(combination) in parts(text)
+{
+  var results := [];
+  var combinations := product(collections);
+  var index := 0;
+  while index < |combinations| {
+    var code := template(combinations[index]);
+    if code != undefined {
+      results := results + [code];
+    }
+    index := index + 1;
+  }
+  return join(results, delimiter);
+}
+
+// Original JavaScript
+
+// export function delimitedCombinations(template, delimiter, ...collections) {
+//   const results = [];
+//   for (const values of product(...collections)) {
+//     const code = template(...values);
+//     if (code !== undefined) {
+//       results.push(code);
+//     }
+//   }
+//   return results.join(delimiter);
+// }

formal-verification/d_infall_tiebreak.dfy

+// Types
+
+type Move(==)
+
+// Library Constants
+
+const infinity: real
+
+// Library Methods
+
+function method with_push<T>(list: seq<T>, element: T): seq<T>
+  ensures with_push(list, element) == list + [element]
+  ensures element in with_push(list, element)
+
+// Helper Methods
+
+function method get_infall(move: Move): real
+  ensures get_infall(move) > -infinity
+
+// Method to Verify
+
+method tiebreak_by_infall(moves_parameter: seq<Move>) returns (rearranged_moves: seq<Move>)
+  requires |moves_parameter| > 0
+{
+  var moves := moves_parameter;
+  var best_indices := [];
+  var best_infall := -infinity;
+  var index := |moves| - 1;
+  while index >= 0 {
+    var infall := get_infall(moves[index]);
+    if infall > best_infall {
+      best_indices := [];
+      best_infall := infall;
+    }
+    if infall >= best_infall {
+      best_indices := with_push(best_indices, index);
+    }
+    index := index - 1;
+  }
+  index :| index in best_indices;
+  var best_move := moves[index];
+  moves := moves[index := moves[0]];
+  moves := moves[0 := best_move];
+  return moves;
+}
+
+// Original JavaScript
+
+// _tiebreakByInfall(moves) {
+//   let bestIndices = [];
+//   let bestInfall = -Infinity;
+//   for (let index = moves.length; index--;) {
+//     const infall = this._getInfall(moves[index]);
+//     if (infall > bestInfall) {
+//       bestIndices = [];
+//       bestInfall = infall;
+//     }
+//     if (infall >= bestInfall) {
+//       bestIndices.push(index);
+//     }
+//   }
+//   const index = bestIndices[Math.floor(Math.random() * bestIndices.length)];
+//   const bestMove = moves[index];
+//   moves[index] = moves[0];
+//   moves[0] = bestMove;
+//   return moves;
+// }

formal-verification/e_quantifiers_warmup.dfy

+// Method to Verify
+
+method nonempty_range(limit: nat) returns (values: seq<nat>)
+  requires limit > 0
+  ensures |values| == limit
+  ensures
+    forall i | 0 <= i < |values| - 1 ::
+    values[i] < values[i + 1]
+{
+  var results: seq<nat> := [0];
+  var counter := 1;
+  while counter < limit {
+    results := results + [counter];
+    counter := counter + 1;
+  }
+  return results;
+}

formal-verification/f_select_children.dfy

+// Types
+
+type Position(==)
+
+type PositionScorePair(==)
+function method get_position(pair: PositionScorePair): Position
+function method get_score(pair: PositionScorePair): real
+
+// Language Constants
+
+const undefined: real
+
+// Program Constants
+
+const PROBE_DEPTH: nat
+const FORWARD_PRUNING_TARGET: real
+
+// Functions to Make Assertions Easier to Write
+
+function minimum_count_for(position: Position, taboo: set<Position>): real
+  ensures minimum_count_for(position, taboo) == FORWARD_PRUNING_TARGET * |get_available_children(position, taboo)| as real
+
+function score_at(position: Position, depth: nat): real
+
+// Helper Methods
+
+function method sort_by_static_evaluation(positions: seq<Position>): seq<Position>
+  ensures |sort_by_static_evaluation(positions)| == |positions|
+
+function method get_available_children(position: Position, taboo: set<Position>): seq<Position>
+
+function method order_children_inexactly(request_number: nat, position: Position, taboo: set<Position>, depth: nat, is_book: Position -> bool): seq<PositionScorePair>
+  ensures
+    forall p | p in order_children_inexactly(request_number, position, taboo, depth, is_book) ::
+    get_score(p) == score_at(get_position(p), depth)
+  ensures
+    forall i | 0 <= i < |order_children_inexactly(request_number, position, taboo, depth, is_book)| ::
+    forall j | i < j < |order_children_inexactly(request_number, position, taboo, depth, is_book)|::
+    get_score(order_children_inexactly(request_number, position, taboo, depth, is_book)[i]) >= get_score(order_children_inexactly(request_number, position, taboo, depth, is_book)[j])
+  ensures |order_children_inexactly(request_number, position, taboo, depth, is_book)| == |get_available_children(position, taboo)|
+  ensures |order_children_inexactly(request_number, position, taboo, depth, is_book)| as real >= minimum_count_for(position, taboo)
+
+// Method to Verify
+
+method select_children(request_number: nat, position: Position, taboo: set<Position>, depth: nat, is_book: Position -> bool) returns (children: seq<Position>)
+  requires 0.0 < FORWARD_PRUNING_TARGET < 1.0
+  ensures |children| <= |get_available_children(position, taboo)|
+  ensures
+    depth > PROBE_DEPTH ==>
+    forall i | 0 <= i < |children| ::
+    children[i] == get_position(order_children_inexactly(request_number, position, taboo, PROBE_DEPTH, is_book)[i])
+  ensures
+    depth > PROBE_DEPTH ==>
+    forall i | 0 <= i < |children| ::
+    forall j | i < j < |children| ::
+    score_at(children[i], PROBE_DEPTH) >= score_at(children[j], PROBE_DEPTH)
+  ensures
+    depth > PROBE_DEPTH ==>
+    |children| as real >= minimum_count_for(position, taboo)
+  ensures
+    depth > PROBE_DEPTH ==>
+    forall i | 0 <= i < |children| ::
+    minimum_count_for(position, taboo) <= i as real ==>
+    score_at(children[i], PROBE_DEPTH) == score_at(children[i - 1], PROBE_DEPTH)
+{
+  if depth <= PROBE_DEPTH {
+    return sort_by_static_evaluation(get_available_children(position, taboo));
+  }
+  var candidates := order_children_inexactly(request_number, position, taboo, PROBE_DEPTH, is_book);
+  var minimum_count := FORWARD_PRUNING_TARGET * |candidates| as real;
+  var results := [];
+  var previous_score := undefined;
+  var index := 0;
+  while index < |candidates|
+    invariant index == |results|
+  {
+    var candidate := get_position(candidates[index]);
+    var score := get_score(candidates[index]);
+    if score != previous_score && |results| as real >= minimum_count {
+      break;
+    }
+    results := results + [candidate];
+    previous_score := score;
+    index := index + 1;
+  }
+  return results;
+}
+
+// Original JavaScript
+
+// async function selectChildren(requestNumber, position, taboo, depth, isBook) {
+//   if (depth <= PROBE_DEPTH) {
+//     return getAvailableChildren(position, taboo).sort(byStaticEvaluation);
+//   }
+//   const candidates = await orderChildrenInexactly(requestNumber, position, taboo, PROBE_DEPTH, isBook);
+//   const minimumCount = FORWARD_PRUNING_TARGET * candidates.length;
+//   const results = [];
+//   let previousScore = undefined;
+//   for (const [candidate, score] of candidates) {
+//     if (score !== previousScore && results.length >= minimumCount) {
+//       break;
+//     }
+//     results.push(candidate);
+//     previousScore = score;
+//   }
+//   return results;
+// }