~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0x87443356945470112b78ad5f17a0cfb9/LAWS.bend as LAWS

2 imports
import Base
import ./lib.bend as G

Laws

law empty_nodes provedin PROOF.bendsource · line 5 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.nodes(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty) == [] : List<&2, U32>}

Empty graph is defined with no nodes or edges.

law empty_edge_count provedin PROOF.bendsource · line 8 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.edge_count(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty) == 0n : Nat}

law empty_neighbors provedin PROOF.bendsource · line 11 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.neighbors(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 0) == [] : List<&2, U32>}

law empty_has_edge provedin PROOF.bendsource · line 14 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.has_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 0, 1) == False{} : Bool}

law singleton_nodes provedin PROOF.bendsource · line 18 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.nodes(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_node(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 7)) == [7] : List<&2, U32>}

A singleton graph contains exactly its node and no edges.

law singleton_edge_count provedin PROOF.bendsource · line 21 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.edge_count(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_node(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 7)) == 0n : Nat}

law singleton_neighbors provedin PROOF.bendsource · line 24 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.neighbors(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_node(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 7), 7) == [] : List<&2, U32>}

law singleton_has_edge provedin PROOF.bendsource · line 27 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.has_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_node(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 7), 7, 7) == False{} : Bool}

law edge_adds_nodes provedin PROOF.bendsource · line 31 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.nodes(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 1, 2)) == [1, 2] : List<&2, U32>}

add_edge adds missing endpoints in insertion order.

law edge_adds_one_edge provedin PROOF.bendsource · line 34 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.edge_count(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 1, 2)) == 1n : Nat}

law edge_is_present provedin PROOF.bendsource · line 37 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.has_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 1, 2), 1, 2) == True{} : Bool}

law edge_neighbors provedin PROOF.bendsource · line 40 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.neighbors(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 1, 2), 1) == [2] : List<&2, U32>}

law reverse_edge_is_absent provedin PROOF.bendsource · line 43 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.has_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 1, 2), 2, 1) == False{} : Bool}

law duplicate_edge_count provedin PROOF.bendsource · line 47 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.edge_count(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 3, 3), 3, 3)) == 1n : Nat}

Re-adding an existing self-loop does not duplicate the edge.

law self_loop_neighbors provedin PROOF.bendsource · line 50 · raw

{0x87443356945470112b78ad5f17a0cfb9/lib.Graph.neighbors(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.add_edge(0x87443356945470112b78ad5f17a0cfb9/lib.Graph.empty, 3, 3), 3) == [3] : List<&2, U32>}