Initial commit.

demonstration/a_minimum_of_three.dfy

+method minimum_of_three(first: real, second: real, third: real) returns (minimum: real)
+  ensures minimum in {first, second, third}
+  ensures minimum <= first
+  ensures minimum <= second
+  ensures minimum <= third
+{
+  var result := first;
+  if second < first && second < third {
+    result := second;
+  }
+  if third < first && third < second {
+    result := third;
+  }
+  return result;
+}

demonstration/b_count_leading_zeros.dfy

+method count_leading_zeros(sequence: seq<nat>) returns (count: nat)
+  ensures count <= |sequence|
+  ensures
+    forall i | 0 <= i < count ::
+    sequence[i] == 0
+  ensures count < |sequence| ==> sequence[count] != 0
+{
+  var index := 0;
+  while index < |sequence| {
+    if sequence[index] != 0 {
+      break;
+    }
+    index := index + 1;
+  }
+  return index;
+}

demonstration/c_list_to_set.dfy

+method list_to_set<T>(list: seq<T>) returns (as_set: set<T>)
+  requires
+    forall i | 0 <= i < |list| ::
+    forall j | i < j < |list| ::
+    list[i] != list[j]
+  ensures |as_set| == |list|
+{
+  var result := {};
+  var index := 0;
+  while index < |list| {
+    result := result + {list[index]};
+    index := index + 1;
+  }
+  return result;
+}

demonstration/d_set_to_list.dfy

+method set_to_list<T>(collection: set<T>) returns (as_list: seq<T>)
+  ensures |as_list| == |collection|
+  ensures
+    forall x | x in collection ::
+    x in as_list
+{
+  var result := [];
+  var remaining := collection;
+  while |remaining| > 0 {
+    var element :| element in remaining;
+    remaining := remaining - {element};
+    result := result + [element];
+  }
+  return result;
+}

demonstration/e_induct.dfy

+method induct<T>(seed: T, update: T -> T, property: T -> bool) returns (iterates: set<T>)
+  requires property(seed)
+  requires
+    forall x | property(x) ::
+    property(update(x))
+  ensures
+    forall x | x in iterates ::
+    property(x)
+  decreases *
+{
+  var current := seed;
+  var results := {current};
+  while true
+    decreases *
+  {
+    current := update(current);
+    if current in results {
+      return results;
+    }
+    results := results + {current};
+  }
+}

demonstration/f_fixed_points.dfy

+method fixed_points<T(==)>(mapping: map<T, T>) returns (fixed_points: set<T>)
+  ensures
+    forall k | k in fixed_points ::
+    k in mapping
+  ensures
+    forall k | k in mapping ::
+    k in fixed_points <==> mapping[k] == k
+{
+  var result := {};
+  var keys := set key | key in mapping;
+  var remaining_keys := keys;
+  while |remaining_keys| > 0 {
+    var key :| key in remaining_keys;
+    remaining_keys := remaining_keys - {key};
+    if mapping[key] == key {
+      result := result + {key};
+    }
+  }
+  return result;
+}

practice/c_map.dfy

+method map_f<T, U>(f: T -> U, inputs: seq<T>) returns (outputs: seq<U>)
+  ensures |outputs| == |inputs|
+  ensures
+    forall i | 0 <= i < |outputs| ::
+    outputs[i] == f(inputs[i])
+{
+  var results := [];
+  var index := 0;
+  while index < |inputs| {
+    results := results + [f(inputs[index])];
+    index := index + 1;
+  }
+  return results;
+}

practice/d_reverse.dfy

+method reverse<T>(list: seq<T>) returns (reversed: seq<T>)
+  ensures |reversed| == |list|
+  ensures
+    forall i | 0 <= i < |reversed| ::
+    reversed[i] == list[|list| - i - 1]
+{
+  var result := [];
+  var index := |list|;
+  while index > 0 {
+    index := index - 1;
+    result := result + [list[index]];
+  }
+  return result;
+}

practice/e_primes.dfy

+method primes(count: nat) returns (primes: seq<nat>)
+  ensures
+    forall i | 0 <= i < |primes| ::
+    forall j | 0 <= j < i ::
+    primes[i] > primes[j]
+  decreases *
+{
+  var results := [];
+  var candidate := 2;
+  while |results| < count
+    decreases *
+  {
+    var is_prime := true;
+    var index := 0;
+    while index < |results| {
+      assume results[index] > 0; // to be proven in lab
+      if candidate % results[index] == 0 {
+        is_prime := false;
+      }
+      index := index + 1;
+    }
+    if is_prime {
+      results := results + [candidate];
+    }
+    candidate := candidate + 1;
+  }
+  return results;
+}