module ChaoticIteration:`sig`

..`end`

Fixpoint computation with widenings using weak topological
orderings as defined by François Bourdoncle and implemented
in

`WeakTopological`

.
`Fixpoint`

is another (simpler) fixpoint computation module, with
general references.

The general idea of fixpoint computation is to iteratively compute
the result of the analysis a vertex from the results of its
predecessors, until stabilisation is achieved on every vertex. The
way to determine, at each step, the next vertex to analyse is
called a *chaotic iteration strategy*. A good strategy can make
the analysis much faster. To enforce the termination of the
analyse and speed it up when it terminates in too many steps, one
can also use a *widening*, to ensure that there is no infinite
(nor too big) sequence of intermediary results for a given
vertex. However, it usually results in a loss of precision, which
is why choosing a good widening set (the set of points on which
the widening will be performed) is mandatory.

This module computes a fixpoint over a graph using weak
topological ordering, which can be used to get both the iteration
strategy and the widening set. The module `WeakTopological`

aims
to compute weak topological orderings which are known to be
excellent decompositions w.r.t these two critical points.

**Author(s):** Thibault Suzanne

**See also** *Efficient chaotic iteration strategies with widenings* ,
François Bourdoncle,
Formal Methods in Programming and their Applications,
Springer Berlin Heidelberg, 1993

`type ``'a`

widening_set =

`|` |
`FromWto` |

`|` |
`Predicate of ` |

How to determine which vertices are to be considered as widening
points.

`FromWto`

indicates to use as widening points the heads of the weak topological ordering given as a parameter of the analysis function. This will always be a safe choice, and in most cases it will also be a good one with respect to the precision of the analysis.

`Predicate f`

indicates to use`f`

as the characteristic function of the widening set.`Predicate (fun _ -> false)`

can be used if a widening is not needed. This variant can be used when there is a special knowledge of the graph to achieve a better precision of the analysis. For instance, if the graph happens to be the flow graph of a program, the predicate should be true for control structures heads. In any case, a condition for a safe widening predicate is that every cycle of the graph should go through at least one widening point. Otherwise, the analysis may not terminate. Note that even with a safe predicate, ensuring the termination does still require a correct widening definition.

module type G =`sig`

..`end`

Minimal graph signature for the algorithm.

module type Data =`sig`

..`end`

Parameters of the analysis.

module Make: