From c92b4f35a14d89fd91e56f026647d183de0e5ea1 Mon Sep 17 00:00:00 2001 From: "Brady J. Garvin" <bgarvin@cse.unl.edu> Date: Tue, 27 Sep 2022 19:47:25 -0500 Subject: [PATCH] Designed exhaustive searches for the first two example problems. --- exhaustive-search.md | 38 ++++++++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 14 deletions(-) diff --git a/exhaustive-search.md b/exhaustive-search.md index 983318e..bf3704f 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; } ``` -- GitLab