Recased code per the current draft of the Dafny style guide.

demonstration/a_minimum_of_three.dfy → demonstration/aMinimumOfThree.dfy

-method minimum_of_three(first: real, second: real, third: real) returns (minimum: real)
+method MinimumOfThree(first: real, second: real, third: real) returns (minimum: real)
   ensures minimum in {first, second, third}
   ensures minimum <= first
   ensures minimum <= second

demonstration/b_count_leading_zeros.dfy → demonstration/bCountLeadingZeros.dfy

-method count_leading_zeros(sequence: seq<nat>) returns (count: nat)
+method CountLeadingZeros(sequence: seq<nat>) returns (count: nat)
   ensures count <= |sequence|
   ensures
     forall i | 0 <= i < count ::

demonstration/c_list_to_set.dfy → demonstration/cListToSet.dfy

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

demonstration/d_set_to_list.dfy → demonstration/dSetToList.dfy

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

demonstration/e_copy_values.dfy → demonstration/eCopyValues.dfy

-method copy_values<T, U>(mapping: map<T, U>, sources: map<T, T>) returns (updated_mapping: map<T, U>)
+method CopyValues<T, U>(mapping: map<T, U>, sources: map<T, T>) returns (updatedMapping: map<T, U>)
   requires
     forall k | k in mapping && k in sources ::
     sources[k] in mapping
@@ -6,13 +6,13 @@ method copy_values<T, U>(mapping: map<T, U>, sources: map<T, T>) returns (update
   var result := map[];
   var remaining := set key | key in mapping :: key;
   while |remaining| > 0 {
-    var destination_key :| destination_key in remaining;
-    remaining := remaining - {destination_key};
-    var source_key := destination_key;
-    if destination_key in sources {
-      source_key := sources[destination_key];
+    var destinationKey :| destinationKey in remaining;
+    remaining := remaining - {destinationKey};
+    var sourceKey := destinationKey;
+    if destinationKey in sources {
+      sourceKey := sources[destinationKey];
     }
-    result := result[destination_key := mapping[source_key]];
+    result := result[destinationKey := mapping[sourceKey]];
   }
   return result;
 }

practice/c_map.dfy → practice/cMapOverSequence.dfy

-method map_f<T, U>(f: T -> U, inputs: seq<T>) returns (outputs: seq<U>)
+method MapOverSequence<T, U>(f: T -> U, inputs: seq<T>) returns (outputs: seq<U>)
   ensures |outputs| == |inputs|
   ensures
     forall i | 0 <= i < |outputs| ::

practice/d_reverse.dfy → practice/dReverse.dfy

-method reverse<T>(list: seq<T>) returns (reversed: seq<T>)
+method Reverse<T>(list: seq<T>) returns (reversed: seq<T>)
   ensures |reversed| == |list|
   ensures
     forall i | 0 <= i < |reversed| ::