From ea97c0991ba933b0fca17c4791beca391d6621d9 Mon Sep 17 00:00:00 2001 From: Brady James Garvin <bgarvin@cse.unl.edu> Date: Wed, 7 Aug 2019 13:24:23 -0500 Subject: [PATCH] Added starter code for formal verification of parts of pseudoplanarity.js. --- formal_verification/find_pseudoface.dfy | 19 ++++ formal_verification/index_vertices.dfy | 17 ++++ formal_verification/prelude.dfy | 88 +++++++++++++++++++ formal_verification/pseudoface_equals.dfy | 9 ++ formal_verification/rotation_system_keys.dfy | 17 ++++ .../rotation_system_values.dfy | 17 ++++ 6 files changed, 167 insertions(+) create mode 100644 formal_verification/find_pseudoface.dfy create mode 100644 formal_verification/index_vertices.dfy create mode 100644 formal_verification/prelude.dfy create mode 100644 formal_verification/pseudoface_equals.dfy create mode 100644 formal_verification/rotation_system_keys.dfy create mode 100644 formal_verification/rotation_system_values.dfy diff --git a/formal_verification/find_pseudoface.dfy b/formal_verification/find_pseudoface.dfy new file mode 100644 index 0000000..48301fd --- /dev/null +++ b/formal_verification/find_pseudoface.dfy @@ -0,0 +1,19 @@ +// Prove that if `findPseudoface` from `pseudoplanarity.js` does not return `undefined`, then it returns a pseudoface built from a cycle. + +include "prelude.dfy" + +method find_pseudoface(indexing: map<Vertex, nat>, rotation_system: RotationSystem, edge: Edge) returns (result: Pseudoface) + requires has_adjacency(get_graph(rotation_system), get_source(edge), get_destination(edge)) + ensures result != undefined() ==> + |get_vertices(result)| > 2 + ensures + result != undefined() ==> + forall i | i in range(0, |get_vertices(result)| - 1) :: + has_adjacency(get_graph(rotation_system), get_vertices(result)[i], get_vertices(result)[i + 1]) + ensures + result != undefined() ==> + has_adjacency(get_graph(rotation_system), top(get_vertices(result), 0), get_vertices(result)[0]) + decreases * +{ + return undefined(); // TODO +} diff --git a/formal_verification/index_vertices.dfy b/formal_verification/index_vertices.dfy new file mode 100644 index 0000000..b9c6b47 --- /dev/null +++ b/formal_verification/index_vertices.dfy @@ -0,0 +1,17 @@ +// Prove that `indexVertices` from `pseudoplanarity.js` maps distinct keys to distinct values. + +include "prelude.dfy" + +method index_vertices(graph: Graph) returns (indexing: map<Vertex, nat>) + requires + forall i | i in range(0, |get_vertices(graph)|) :: + forall j | j in range(0, |get_vertices(graph)|) && i != j :: + get_vertices(graph)[i] != get_vertices(graph)[j] + ensures + forall key | key in indexing :: + forall other_key | other_key in indexing && other_key != key :: + indexing[key] != indexing[other_key] +{ + var result: map<Vertex, nat> := map[]; + return result; // TODO +} diff --git a/formal_verification/prelude.dfy b/formal_verification/prelude.dfy new file mode 100644 index 0000000..c9634e4 --- /dev/null +++ b/formal_verification/prelude.dfy @@ -0,0 +1,88 @@ +// This file provides various Dafny helper functions for the verification of code from pseudoplanarity.js. + +// Returns the equivalent to JavaScript's `undefined`. +function method undefined<T>(): T + +// Returns the set of integers between `low` (inclusive) and `high` (exclusive). +// (For use in specifications only.) +function range(low: int, high: int): set<int> + ensures forall i | low <= i < high :: i in range(low, high) + ensures forall i | i in range(low, high) :: low <= i < high + +// Returns the same as `range(low, high)`, but with every element reduced modulo `length`. +// For example: +// range(3, 8) == {3, 4, 5, 6, 7} +// wrapped_range(3, 8, 6) == {3, 4, 5, 0, 1} +// (For use in specifications only.) +function wrapped_range(low: nat, high: nat, length: nat): set<int> + ensures forall i | low <= i < high && i < length :: i in wrapped_range(low, high, length) + ensures forall i | 0 <= i < high - length :: i in wrapped_range(low, high, length) + ensures forall i | i in wrapped_range(low, high, length) :: 0 <= i < length + ensures forall i | i in wrapped_range(low, high, length) :: (low <= i < high && i < length) || (0 <= i < high - length) + +// Return the ith element from the end of a list. +function method top<T>(list: seq<T>, i: nat): T + requires |list| > i + ensures top(list, i) == list[|list| - i - 1] + +// Return a list with its last element removed. +function method popped<T>(stack: seq<T>): seq<T> + requires |stack| > 0 + ensures popped(stack) == stack[..|stack| - 1] + +// Returns the set of values in a map. +function method values<K, V>(mapping: map<K, V>): set<V> { + set key | key in mapping :: mapping[key] +} + +// Return a copy of a map with `new_key` mapped to `new_value`. +// (For use in imperative code only.) +method update<K, V>(mapping: map<K, V>, new_key: K, new_value: V) returns (result: map<K, V>) + ensures result == mapping[new_key := new_value]; + ensures forall key | key in mapping :: key in result + ensures new_key !in mapping ==> forall key | key in mapping :: result[key] == mapping[key] + ensures new_key in result + ensures result[new_key] == new_value + ensures new_key !in mapping ==> values(result) == values(mapping) + {new_value} +{ + return mapping[new_key := new_value]; +} + +// Various graph-related types, all of which support equality comparisons: +type Vertex(==) +type Edge(==) +type Pseudoface(==) +type Graph(==) +type RotationSystem(==) + +// Get an edge's source vertex. +function method get_source(edge: Edge): Vertex + +// Get an edge's destination vertex. +function method get_destination(edge: Edge): Vertex + +// Get all of the edges in a pseudoface or a graph. +function method get_vertices<T>(graphlike_object: T): seq<Vertex> + +// Create a Pseudoface from a vertex list and an indexing. +function method create_pseudoface(vertices: seq<Vertex>, indexing: map<Vertex, nat>): Pseudoface + ensures get_vertices(create_pseudoface(vertices, indexing)) == vertices + +// Compute a hash code from a list of vertices. +function method hash(vertices: seq<Vertex>): int + +// Get the hash code of a pseudoface. +function method get_hash_code(pseudoface: Pseudoface): int { + hash(get_vertices(pseudoface)) +} + +// Test whether two vertices are adjacent in a graph. +function method has_adjacency(graph: Graph, source: Vertex, destination: Vertex): bool + +// Recover a graph from its rotation system. +function method get_graph(rotation_system: RotationSystem): Graph + +// Get the neighbor of `vertex` that comes after `neighbor` according to `rotation_system`. +function method get_next_neighbor(rotation_system: RotationSystem, vertex: Vertex, neighbor: Vertex): Vertex + ensures has_adjacency(get_graph(rotation_system), vertex, get_next_neighbor(rotation_system, vertex, neighbor)) + ensures has_adjacency(get_graph(rotation_system), get_next_neighbor(rotation_system, vertex, neighbor), vertex) diff --git a/formal_verification/pseudoface_equals.dfy b/formal_verification/pseudoface_equals.dfy new file mode 100644 index 0000000..f6bed9b --- /dev/null +++ b/formal_verification/pseudoface_equals.dfy @@ -0,0 +1,9 @@ +// Prove that the `equals` method from `pseudoplanarity.js` tests whether two pseudofaces have the same vertex lists. + +include "prelude.dfy" + +method equals(self: Pseudoface, other: Pseudoface) returns (result: bool) + ensures result <==> get_vertices(self) == get_vertices(other) +{ + return true; // TODO +} diff --git a/formal_verification/rotation_system_keys.dfy b/formal_verification/rotation_system_keys.dfy new file mode 100644 index 0000000..b147ac6 --- /dev/null +++ b/formal_verification/rotation_system_keys.dfy @@ -0,0 +1,17 @@ +// Prove that the inner loop of the `RotationSystem` constructor from `pseudoplanarity.js` makes every neighbor into a map key. + +include "prelude.dfy" + +method find_successors(neighbors: seq<Vertex>) returns (result: map<Vertex, Vertex>) + requires |neighbors| > 0 + requires + forall i | i in range(0, |neighbors|) :: + forall j | j in range(0, |neighbors|) && i != j :: + neighbors[i] != neighbors[j] + ensures + forall i | i in range(0, |neighbors|) :: + neighbors[i] in result +{ + var successors: map<Vertex, Vertex> := map[]; + return successors; // TODO +} diff --git a/formal_verification/rotation_system_values.dfy b/formal_verification/rotation_system_values.dfy new file mode 100644 index 0000000..ca85fff --- /dev/null +++ b/formal_verification/rotation_system_values.dfy @@ -0,0 +1,17 @@ +// Prove that the inner loop of the `RotationSystem` constructor from `pseudoplanarity.js` makes every neighbor into a map value. + +include "prelude.dfy" + +method find_successors(neighbors: seq<Vertex>) returns (result: map<Vertex, Vertex>) + requires |neighbors| > 0 + requires + forall i | i in range(0, |neighbors|) :: + forall j | j in range(0, |neighbors|) && i != j :: + neighbors[i] != neighbors[j] + ensures + forall i | i in range(0, |neighbors|) :: + neighbors[i] in values(result) +{ + var successors: map<Vertex, Vertex> := map[]; + return successors; // TODO +} -- GitLab