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