Designed and implemented exhaustive searches.

exhaustive-search.md

@@ -9,8 +9,8 @@ with a given tag.
 
 Signature: filterPosts(X: list<Post>, t: string) → R: list<Post>
 Precondition: [none]
-Postcondition:
-Postcondition:
+Postcondition: R ⊆ X
+Postcondition: ∀x∈X. x ∈ R ↔ t ∈ tags(x)
 
 ### JavaScript
 
@@ -18,7 +18,13 @@ Postcondition:
 
 ```js
 function filter(posts, tag) {
-  // …
+  const results = [];
+  for (const post of posts) { // "generate" step
+    if (post.tags.has(tag)) { // "check" step
+      results.push(post);
+    }
+  }
+  return results;
 }
 ```
 
@@ -37,12 +43,12 @@ and blue.)
 
 Signature: color(G = (V, E): graph) → C: map<vertex, color>
 Happy path:
- Precondition:
- Postcondition:
- Postcondition:
+ Precondition: ∃X∈P^V. isValidColoring(G, X)
+ Postcondition: C ∈ P^V
+ Postcondition: isValidColoring(G, C)
 Sad path:
- Precondition:
- Postcondition:
+ Precondition: ¬∃X∈P^V. isValidColoring(G, X)
+ Postcondition: C = ⊥
 
 ### JavaScript
 
@@ -53,13 +59,12 @@ green, and blue.)
 
 ```js
 function color(graph) {
-  // …
-  for (const coloring of mappings(graph.vertices, PALETTE)) {
-    if (isValidColoring(graph, coloring)) {
-      // …
+  for (const coloring of mappings(graph.vertices, PALETTE)) { // combinatorial enumeration
+    if (isValidColoring(graph, coloring)) { // helper function
+      return coloring;
     }
   }
-  // …
+  return undefined;
 }
 ```
 
@@ -74,8 +79,8 @@ color).
 #### Contract
 
 Signature: isValidColoring(G = (V, E): graph, C: map<vertex, color>) → r: boolean
-Precondition:
-Postcondition:
+Precondition: C ∈ P^V
+Postcondition: r ↔ ¬∃(u, v)∈E. C[u] = C[v]
 
 #### JavaScript
 
@@ -87,7 +92,12 @@ vertices to colors.)
 
 ```js
 function isValidColoring(graph, coloring) {
-  // …
+  for (const [source, destination] of graph.edges) {
+    if (coloring.get(source) === coloring.get(destination)) {
+      return false;
+    }
+  }
+  return true;
 }
 ```
 
@@ -103,22 +113,24 @@ set of items not exceeding the weight limit.
 
 Signature: knapsack(I: set<item>, w: set<item> → number, W: number, v: set<item> → number) → K: set<item>
 Happy path:
- Precondition:
- Postcondition:
- Postcondition:
+ Precondition: |options(I, w, W)| > 0
+ Postcondition: K ∈ options(I, w, W)
+ Postcondition: ∀X∈options(I, w, W). v(K) ≥ v(X)
 Sad path:
- Precondition:
- Postcondition:
+ Precondition: |options(I, w, W)| = 0
+ Postcondition: K = ⊥
 
 ### JavaScript
 
 ```js
 function knapsack(items, getWeight, weightLimit, getValue) {
-  // …
+  const result = undefined;
   for (const option of options(items, getWeight, weightLimit)) {
-    // …
+    if (result === undefined || getValue(option) > getValue(result)) {
+      result = option;
     }
-  // …
+  }
+  return result;
 }
 ```
 
@@ -134,13 +146,19 @@ of items not exceeding the weight limit.
 
 Signature: options(I: set<item>, w: set<item> → number, W: number) → O: set<set<item>>
 Precondition: [none]
-Postcondition:
-Postcondition:
+Postcondition: O ⊆ 𝒫(I)
+Postcondition: ∀X∈𝒫(I). X ∈ O ↔ w(X) ≤ W
 
 #### JavaScript
 
 ```js
 function options(items, getWeight, weightLimit) {
-  // …
+  const results = new Set();
+  for (const candidate of powerset(items)) {
+    if (getWeight(candidate) <= weightLimit) {
+      results.add(candidate);
+    }
+  }
+  return results;
 }
 ```