package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

First Order Logic Definition

type 'a element =
  1. | E_none
  2. | E_true
  3. | E_false
  4. | E_int of int
  5. | E_fun of 'a * 'a element list
type 'a operator = {
  1. invertible : bool;
  2. associative : bool;
  3. commutative : bool;
  4. idempotent : bool;
  5. neutral : 'a element;
  6. absorbant : 'a element;
}

Algebraic properties for user operators.

type 'a category =
  1. | Function
    (*

    logic function

    *)
  2. | Constructor
    (*

    f xs = g ys iff f=g && xi=yi

    *)
  3. | Injection
    (*

    f xs = f ys iff xi=yi

    *)
  4. | Operator of 'a operator

Algebraic properties for functions.

type binder =
  1. | Forall
  2. | Exists
  3. | Lambda

Quantifiers and Binders

type ('f, 'a) datatype =
  1. | Prop
  2. | Bool
  3. | Int
  4. | Real
  5. | Tvar of int
    (*

    ranges over 1..arity

    *)
  6. | Array of ('f, 'a) datatype * ('f, 'a) datatype
  7. | Record of ('f * ('f, 'a) datatype) list
  8. | Data of 'a * ('f, 'a) datatype list
type sort =
  1. | Sprop
  2. | Sbool
  3. | Sint
  4. | Sreal
  5. | Sdata
  6. | Sarray of sort
type maybe =
  1. | Yes
  2. | No
  3. | Maybe
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) funtype = {
  1. result : ('f, 'a) datatype;
    (*

    Type of returned value

    *)
  2. params : ('f, 'a) datatype list;
    (*

    Type of parameters

    *)
}
type ('f, 'a, 'd, 'x, 'b, 'e) term_repr =
  1. | True
  2. | False
  3. | Kint of Z.t
  4. | Kreal of Q.t
  5. | Times of Z.t * 'e
    (*

    mult: k1 * e2

    *)
  6. | Add of 'e list
    (*

    add: e11 + ... + e1n

    *)
  7. | Mul of 'e list
    (*

    mult: e11 * ... * e1n

    *)
  8. | Div of 'e * 'e
  9. | Mod of 'e * 'e
  10. | Eq of 'e * 'e
  11. | Neq of 'e * 'e
  12. | Leq of 'e * 'e
  13. | Lt of 'e * 'e
  14. | Aget of 'e * 'e
    (*

    access: array1idx2

    *)
  15. | Aset of 'e * 'e * 'e
    (*

    update: array1idx2 -> elem3

    *)
  16. | Acst of ('f, 'a) datatype * 'e
    (*

    constant array type -> value

    *)
  17. | Rget of 'e * 'f
  18. | Rdef of ('f * 'e) list
  19. | And of 'e list
    (*

    and: e11 && ... && e1n

    *)
  20. | Or of 'e list
    (*

    or: e11 || ... || e1n

    *)
  21. | Not of 'e
  22. | Imply of 'e list * 'e
    (*

    imply: (e11 && ... && e1n) ==> e2

    *)
  23. | If of 'e * 'e * 'e
    (*

    ite: if c1 then e2 else e3

    *)
  24. | Fun of 'd * 'e list
    (*

    Complete call (no partial app.)

    *)
  25. | Fvar of 'x
  26. | Bvar of int * ('f, 'a) datatype
  27. | Apply of 'e * 'e list
    (*

    High-Order application (Cf. binder)

    *)
  28. | 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
type 'a affine = Z.t * (Z.t * 'a) list
module type Term = sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct