Frama-C API - Logic
First Order Logic Definition
type 'a operator = {
invertible : bool;
associative : bool;
commutative : bool;
idempotent : bool;
neutral : 'a element;
absorbant : 'a element;
}
Algebraic properties for user operators.
type 'a category =
| Function
(*logic function
*)| Constructor
(*
*)f xs = g ys
ifff=g && xi=yi
| Injection
(*
*)f xs = f ys
iffxi=yi
| Operator of 'a operator
Algebraic properties for functions.
module type Symbol = sig ... end
Ordered, hash-able and pretty-printable symbols
module type Data = sig ... end
module type Field = sig ... end
module type Function = sig ... end
module type Variable = sig ... end
Representation of Patterns, Functions and Terms
type ('f, 'a, 'd, 'x, 'b, 'e) term_repr =
| True
| False
| Kint of Z.t
| Kreal of Q.t
| Times of Z.t * 'e
(*mult: k1 * e2
*)| Add of 'e list
(*add: e11 + ... + e1n
*)| Mul of 'e list
(*mult: e11 * ... * e1n
*)| Div of 'e * 'e
| Mod of 'e * 'e
| Eq of 'e * 'e
| Neq of 'e * 'e
| Leq of 'e * 'e
| Lt of 'e * 'e
| Aget of 'e * 'e
(*access: array1
*)idx2
| Aset of 'e * 'e * 'e
(*update: array1
*)idx2 -> elem3
| Acst of ('f, 'a) datatype * 'e
(*constant array
*)type -> value
| Rget of 'e * 'f
| Rdef of ('f * 'e) list
| And of 'e list
(*and: e11 && ... && e1n
*)| Or of 'e list
(*or: e11 || ... || e1n
*)| Not of 'e
| Imply of 'e list * 'e
(*imply: (e11 && ... && e1n) ==> e2
*)| If of 'e * 'e * 'e
(*ite: if c1 then e2 else e3
*)| Fun of 'd * 'e list
(*Complete call (no partial app.)
*)| Fvar of 'x
| Bvar of int * ('f, 'a) datatype
| Apply of 'e * 'e list
(*High-Order application (Cf. binder)
*)| Bind of binder * ('f, 'a) datatype * 'b
representation of terms. type arguments are the following:
- 'z: representation of integral constants
- 'f: representation of fields
- 'a: representation of abstract data types
- 'd: representation of functions
- 'x: representation of free variables
- 'b: representation of bound term (phantom type equal to 'e)
- 'e: sub-expression
module type Term = sig ... end