an abstract representation of a solution

create constraints default creates an initial approximation of a solution. The default parameter defines the default value of all variables unspecified in the initial constraints.

• parameter constraints

  a finite mapping from variables to their value approximations.

For the returned value s the following is true:

• not(is_fixpoint s)
• iterations s = 0
• get s x = constraints[x] if x in constraints else default

equal s1 s2 is true if s1 and s2 are equal solutions.

Two solutions are equal if for all x in the data domain 'd, we have that equal s1[x] s2[x].

iterations s returns the total number of iterations that was made to obtain the current solution.

default s return the default value assigned to all variables not in the internal finite mapping. This is usually a bottom or top value, depending on whether iteration increases or decreases.

enum xs enumerates all non-trivial values in the solution.

A value is non-trivial if it differs from the default value.

is_fixpoint s is true if the solution is a fixed point solution, i.e., is a solution that stabilizes the system of equations.

get s x returns a value of x.

derive s ~f default creates a new solution from an old one with a new default and where for each node n in s's finite map, if f n (get s n) = Some v then n maps to v.