Designed exhaustive searches for the first two example problems.

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:
 
 ```
 function filter(posts, tag) {
-  // …
+  const results = [];
+  for (const post of posts) { // "generate"
+    if (post.tags.has(tag)) { // "check"
+      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.)
 
 ```
 function color(graph) {
-  // …
   for (const coloring of mappings(graph.vertices, PALETTE)) {
     if (isValidColoring(graph, coloring)) {
-      // …
+      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.)
 
 ```
 function isValidColoring(graph, coloring) {
-  // …
+  for (const [source, destination] of graph.edges) {
+    if (coloring.get(source) === coloring.get(destination)) {
+      return false;
+    }
+  }
+  return true;
 }
 ```