diff --git a/demonstration/a_minimum_of_three.dfy b/demonstration/aMinimumOfThree.dfy
similarity index 77%
rename from demonstration/a_minimum_of_three.dfy
rename to demonstration/aMinimumOfThree.dfy
index 1aa08b85abe24cf3d15ec17fbaa89cf554983265..5b779003eef62bc0a1230fa9c3ad85b8fd71bbf3 100644
--- a/demonstration/a_minimum_of_three.dfy
+++ b/demonstration/aMinimumOfThree.dfy
@@ -1,4 +1,4 @@
-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
diff --git a/demonstration/b_count_leading_zeros.dfy b/demonstration/bCountLeadingZeros.dfy
similarity index 81%
rename from demonstration/b_count_leading_zeros.dfy
rename to demonstration/bCountLeadingZeros.dfy
index f53a9f14ab7d9cb71443e3080333583b805aebd8..e002aafe5e69d6aaca9bd2c5bff602f006f3f3b4 100644
--- a/demonstration/b_count_leading_zeros.dfy
+++ b/demonstration/bCountLeadingZeros.dfy
@@ -1,4 +1,4 @@
-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 ::
diff --git a/demonstration/c_list_to_set.dfy b/demonstration/cListToSet.dfy
similarity index 73%
rename from demonstration/c_list_to_set.dfy
rename to demonstration/cListToSet.dfy
index d12846eae9ff624716b14f9ccfd736d847f0e1d7..6e474654440df3a3d02745fee5dcadd825a079a0 100644
--- a/demonstration/c_list_to_set.dfy
+++ b/demonstration/cListToSet.dfy
@@ -1,9 +1,9 @@
-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;
diff --git a/demonstration/d_set_to_list.dfy b/demonstration/dSetToList.dfy
similarity index 68%
rename from demonstration/d_set_to_list.dfy
rename to demonstration/dSetToList.dfy
index 4f62df1fe4253bdda0322785682d8726605fbeb8..e218635878bbf0fd4cbb200e9ece44f7f0099fd0 100644
--- a/demonstration/d_set_to_list.dfy
+++ b/demonstration/dSetToList.dfy
@@ -1,8 +1,8 @@
-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;
diff --git a/demonstration/eCopyValues.dfy b/demonstration/eCopyValues.dfy
new file mode 100644
index 0000000000000000000000000000000000000000..db27048513abe793b84ce5d9604d37894392a5f7
--- /dev/null
+++ b/demonstration/eCopyValues.dfy
@@ -0,0 +1,18 @@
+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
+{
+  var result := map[];
+  var remaining := set key | key in mapping :: key;
+  while |remaining| > 0 {
+    var destinationKey :| destinationKey in remaining;
+    remaining := remaining - {destinationKey};
+    var sourceKey := destinationKey;
+    if destinationKey in sources {
+      sourceKey := sources[destinationKey];
+    }
+    result := result[destinationKey := mapping[sourceKey]];
+  }
+  return result;
+}
diff --git a/demonstration/e_copy_values.dfy b/demonstration/e_copy_values.dfy
deleted file mode 100644
index e5639af31a26f1b0cc892b6bbb6fb68412375e79..0000000000000000000000000000000000000000
--- a/demonstration/e_copy_values.dfy
+++ /dev/null
@@ -1,18 +0,0 @@
-method copy_values<T, U>(mapping: map<T, U>, sources: map<T, T>) returns (updated_mapping: map<T, U>)
-  requires
-    forall k | k in mapping && k in sources ::
-    sources[k] in mapping
-{
-  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];
-    }
-    result := result[destination_key := mapping[source_key]];
-  }
-  return result;
-}
diff --git a/practice/c_map.dfy b/practice/cMapOverSequence.dfy
similarity index 76%
rename from practice/c_map.dfy
rename to practice/cMapOverSequence.dfy
index 72809269d60c639d219330803cc06ecd326aa52d..f0237aab46c73ad167fee473b3391fc4e218c6f3 100644
--- a/practice/c_map.dfy
+++ b/practice/cMapOverSequence.dfy
@@ -1,4 +1,4 @@
-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| ::
diff --git a/practice/d_reverse.dfy b/practice/dReverse.dfy
similarity index 82%
rename from practice/d_reverse.dfy
rename to practice/dReverse.dfy
index 90786444e2666102f9dd05085ef8f973f483f225..f25c41abd3ec8e2adff00f5c0c61757ec90b9aec 100644
--- a/practice/d_reverse.dfy
+++ b/practice/dReverse.dfy
@@ -1,4 +1,4 @@
-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| ::