Make invariants more precise (#371)

Summary:
The previously listed invariants were weak on two counts. First, it was
unstated that the keys of `_inEdges`, `_outEdges`, and `_nodes` should
coincide. Second, the “exactly once” condition on edge inclusion had the
unintentional effect that edge absent in `_edges` but present twice or
more in each of `_inEdges` and `_outEdges` would not violate the
invariant.

Test Plan:
Stay tuned.

wchargin-branch: strengthen-invariants
This commit is contained in:
William Chargin 2018-06-08 15:19:25 -07:00 committed by GitHub
parent d9e2850eb3
commit 831f5f571c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -52,13 +52,21 @@ export class Graph {
// An edge `e` is in the graph if `_edges.get(e.address)`
// is deep-equal to `e`.
//
// Invariant: For a node `n`, the following are equivalent:
// 1. `n` is in the graph;
// 2. `_inEdges.has(n)`;
// 3. `_outEdges.has(n)`.
//
// Invariant: If an edge `e` is in the graph, then `e.src` and `e.dst`
// are both in the graph.
//
// Invariant: For an edge `e`, the following are equivalent:
// - `e` is in the graph;
// - `_inEdges.get(e.dst)` contains `e` exactly once;
// - `_outEdges.get(e.src)` contains `e` exactly once.
// Invariant: For an edge `e`, if `e.dst` and `e.src` are in the
// graph, the following are equivalent:
// 1. `e` is in the graph;
// 2. `_inEdges.get(e.dst)` contains `e`;
// 3. `_inEdges.get(e.dst)` contains `e` exactly once;
// 4. `_outEdges.get(e.src)` contains `e`;
// 5. `_outEdges.get(e.src)` contains `e` exactly once.
_nodes: Set<NodeAddressT>;
_edges: Map<EdgeAddressT, Edge>;
_inEdges: Map<NodeAddressT, Edge[]>;