why3doc index index

GraphSetSucc

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

GraphListSucc

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

GraphListArraySucc

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