module GraphSetSucc
A graph is represented by a pair (vertices
, successor
)
vertices
: this constant is the set of graph vertices
successor
: this function gives for each vertex the set of vertices directly joinable from it
use export set.Fset type vertex constant vertices: set vertex function successors vertex : set vertex axiom successors_vertices: forall x. mem x vertices -> subset (successors x) vertices predicate edge (x y: vertex) = mem x vertices /\ mem y (successors x) clone export graph.Path with type vertex = vertex, predicate edge = edge end
module GraphListSucc
A graph is represented by a pair (vertices
, successor
)
vertices
: this constant is the set of graph vertices
successor
: this function gives for each vertex the list of vertices directly joinable from it
use import list.List use import list.Mem as L use import list.Elements as E use export set.Fset type vertex constant vertices: set vertex function successors vertex : list vertex axiom successors_vertices: forall x. mem x vertices -> subset (elements (successors x)) vertices predicate edge (x y: vertex) = mem x vertices /\ L.mem y (successors x) clone export graph.Path with type vertex = vertex, predicate edge = edge end
module GraphListArraySucc
A graph is represented by a pair (vertices
, successor
)
vertices
: this constant is the set of integers representing the graph vertices
successor
: this function gives for each vertex the list of vertices directly joinable from it
use import int.Int use import list.List use import list.Mem as L use import list.Elements as E use export set.Fset type vertex = int constant vertices: set vertex axiom vertices_number: forall x. mem x vertices <-> 0 <= x < cardinal vertices function successors vertex : list vertex axiom successors_vertices: forall x. mem x vertices -> subset (elements (successors x)) vertices predicate edge (x y: vertex) = mem x vertices /\ L.mem y (successors x) clone export graph.Path with type vertex = vertex, predicate edge = edge end
Generated by why3doc 0.88.3