Frama-C API - Finite

The type n finite encodes all finite sets of cardinal n. It is used by the module Linear to represent accesses to vectors and matrices coefficients, statically ensuring that no out of bounds access can be performed.

The first element of any finite subset. The type encodes that for a finite subset to have an element, its cardinal must be at least one.

last n returns a value encoding the last element of any finite subset of cardinal n.

The call next f returns a value encoding the element right after f in a finite subset. The type encodes the relations between the cardinal of the finite subset containing f and the cardinal of the one containing its successor.

If f is an element of any finite subset of cardinal n, it is also an element of any finite subset of cardinal n + 1. The call weaken f allows to prove that fact to the type system.

If f is an element of any finite subset of cardinal n + 1, it may also be an element of any finite subset of cardinal n. The call strengthen n f allows to prove that fact to the type system. None is returned if and only if f is the last element of its subset.

The call of_int limit n returns a finite value representing the nth element of a finite set of cardinal limit. If n is not in the bounds, None is returned. This function complexity is O(1).

The call to_int n returns an integer equal to n. This function complexity is O(1).

The call fold f ?start ?stop size acc folds over each elements between start and stop of a finite set of cardinal size, computing f and accumulating its results at each step, starting with acc. The default values of start and stop are respectively Finite.first and Finite.last size, i.e by default, fold will go through all elements of a finite set of cardinal size. The function complexity is O(n).

The call iter f ?start ?stop limit iterates over each elements between start and stop of a finite set of cardinal size. As for fold, the default values of start and stop are respectively Finite.first and Finite.last size.

The call for_all f ?start ?stop limit returns true if and only if f i is true for all elements i between start and stop of a finite set of cardinal size. As for fold, the default values of start and stop are respectively Finite.first and Finite.last size. If size is zero or start is strictly greater than stop, the call returns true.