LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as G# Empty graph is defined with no nodes or edges.law empty_nodes:  { G.Graph.nodes(G.Graph.empty()) == Nil{} : List<&2, U32> }law empty_edge_count:  { G.Graph.edge_count(G.Graph.empty()) == 0n : Nat }law empty_neighbors:  { G.Graph.neighbors(G.Graph.empty(), 0) == Nil{} : List<&2, U32> }law empty_has_edge:  { G.Graph.has_edge(G.Graph.empty(), 0, 1) == False{} : Bool }# A singleton graph contains exactly its node and no edges.law singleton_nodes:  { G.Graph.nodes(G.Graph.add_node(G.Graph.empty(), 7)) == 7 <> Nil{} : List<&2, U32> }law singleton_edge_count:  { G.Graph.edge_count(G.Graph.add_node(G.Graph.empty(), 7)) == 0n : Nat }law singleton_neighbors:  { G.Graph.neighbors(G.Graph.add_node(G.Graph.empty(), 7), 7) == Nil{} : List<&2, U32> }law singleton_has_edge:  { G.Graph.has_edge(G.Graph.add_node(G.Graph.empty(), 7), 7, 7) == False{} : Bool }# add_edge adds missing endpoints in insertion order.law edge_adds_nodes:  { G.Graph.nodes(G.Graph.add_edge(G.Graph.empty(), 1, 2)) == 1 <> 2 <> Nil{} : List<&2, U32> }law edge_adds_one_edge:  { G.Graph.edge_count(G.Graph.add_edge(G.Graph.empty(), 1, 2)) == 1n : Nat }law edge_is_present:  { G.Graph.has_edge(G.Graph.add_edge(G.Graph.empty(), 1, 2), 1, 2) == True{} : Bool }law edge_neighbors:  { G.Graph.neighbors(G.Graph.add_edge(G.Graph.empty(), 1, 2), 1) == 2 <> Nil{} : List<&2, U32> }law reverse_edge_is_absent:  { G.Graph.has_edge(G.Graph.add_edge(G.Graph.empty(), 1, 2), 2, 1) == False{} : Bool }# Re-adding an existing self-loop does not duplicate the edge.law duplicate_edge_count:  { G.Graph.edge_count(G.Graph.add_edge(G.Graph.add_edge(G.Graph.empty(), 3, 3), 3, 3)) == 1n : Nat }law self_loop_neighbors:  { G.Graph.neighbors(G.Graph.add_edge(G.Graph.empty(), 3, 3), 3) == 3 <> Nil{} : List<&2, U32> }