Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

This module provides a representation of closed boxes in a classical vector space over a field 𝕂.

Parameters

module K : Field.S

Signature

type 'n t = {
  1. center : 'n Linear.Space(K).vector;
  2. radius : 'n Linear.Space(K).vector;
}

Boxes are represented as a center and a radius. The radius components are always all positives.

The call make center radius returns a box of center center and of radius abs radius, with abs the componentwise absolute value on vectors as defined in Linear.

The call point center returns a box of radius zero and of center center, i.e a point in the vector space.

val zero : 'n Nat.succ Nat.nat -> 'n Nat.succ t

The call zero n returns the point zero in a n dimensionnal vector space.

Pretty printer.

Boxes can also be seen as a collection of intervals. The call bounds b returns thus the bounds in each dimension of the closed space defined by b. The lower b (resp. upper b) function returns only the lower bounds (resp. upper bounds).

val lower : 'n t -> 'n Linear.Space(K).vector
val upper : 'n t -> 'n Linear.Space(K).vector
val is_included : 'n t -> 'n t -> bool

The call is_included l r returns true if and only if all points in the box l are also in the box r.

val (+) : 'n t -> 'n t -> 'n t

Minkowsky sum of two boxes, i.e l + r is the box z such as \forall x \in l, y \in r, x + y \in z.