From 562a6b54055df84baee3a9cdec2a20a1acd28497 Mon Sep 17 00:00:00 2001
From: "Brady J. Garvin" <bgarvin@cse.unl.edu>
Date: Tue, 9 Aug 2022 12:59:08 -0500
Subject: [PATCH] Recased code per the current draft of the Dafny style guide.
---
...inimum_of_three.dfy => aMinimumOfThree.dfy} | 2 +-
...eading_zeros.dfy => bCountLeadingZeros.dfy} | 2 +-
.../{c_list_to_set.dfy => cListToSet.dfy} | 4 ++--
.../{d_set_to_list.dfy => dSetToList.dfy} | 6 +++---
demonstration/eCopyValues.dfy | 18 ++++++++++++++++++
demonstration/e_copy_values.dfy | 18 ------------------
practice/{c_map.dfy => cMapOverSequence.dfy} | 2 +-
practice/{d_reverse.dfy => dReverse.dfy} | 2 +-
8 files changed, 27 insertions(+), 27 deletions(-)
rename demonstration/{a_minimum_of_three.dfy => aMinimumOfThree.dfy} (77%)
rename demonstration/{b_count_leading_zeros.dfy => bCountLeadingZeros.dfy} (81%)
rename demonstration/{c_list_to_set.dfy => cListToSet.dfy} (73%)
rename demonstration/{d_set_to_list.dfy => dSetToList.dfy} (68%)
create mode 100644 demonstration/eCopyValues.dfy
delete mode 100644 demonstration/e_copy_values.dfy
rename practice/{c_map.dfy => cMapOverSequence.dfy} (76%)
rename practice/{d_reverse.dfy => dReverse.dfy} (82%)
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 1aa08b8..5b77900 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 f53a9f1..e002aaf 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 d12846e..6e47465 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 4f62df1..e218635 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 0000000..db27048
--- /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 e5639af..0000000
--- 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 7280926..f0237aa 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 9078644..f25c41a 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| ::
--
GitLab