diff --git a/exhaustive-search.md b/exhaustive-search.md index 983318e06dd4d4c0fb4bf8257baff2f97bfc6eb2..bf3704f12ed4120e0d8c447644e7d99e630a8301 100644 --- a/exhaustive-search.md +++ b/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; } ```