package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/qed/Qed/Logic/index.html

Module `Qed.Logic`Source

First Order Logic Definition

Sourcetype 'a element =

| E_none
| E_true
| E_false
| E_int of int
| E_fun of 'a * 'a element list

Sourcetype 'a operator = {

invertible : bool;
associative : bool;
commutative : bool;
idempotent : bool;
neutral : 'a element;
absorbant : 'a element;

}

Algebraic properties for user operators.

Sourcetype 'a category =

| Function
(*
logic function
*)
| Constructor
(*
f xs = g ys iff f=g && xi=yi
*)
| Injection
(*
f xs = f ys iff xi=yi
*)
| Operator of 'a operator

Algebraic properties for functions.

Sourcetype binder =

| Forall
| Exists
| Lambda

Quantifiers and Binders

Sourcetype ('f, 'a) datatype =

| Prop
| Bool
| Int
| Real
| Tvar of int
(*
ranges over 1..arity
*)
| Array of ('f, 'a) datatype * ('f, 'a) datatype
| Record of ('f * ('f, 'a) datatype) list
| Data of 'a * ('f, 'a) datatype list

Sourcetype sort =

| Sprop
| Sbool
| Sint
| Sreal
| Sdata
| Sarray of sort

Sourcetype maybe =

| Yes
| No
| Maybe

Sourcemodule type Symbol = sig ... end

Ordered, hash-able and pretty-printable symbols

Sourcemodule type Data = sig ... end

Sourcemodule type Field = sig ... end

Sourcemodule type Function = sig ... end

Sourcemodule type Variable = sig ... end

Representation of Patterns, Functions and Terms

Sourcetype ('f, 'a) funtype = {

result : ('f, 'a) datatype;
(*
Type of returned value
*)
params : ('f, 'a) datatype list;
(*
Type of parameters
*)

}

Sourcetype ('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: array1idx2
*)
| Aset of 'e * 'e * 'e
(*
update: array1idx2 -> 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

Sourcetype 'a affine = Z.t * (Z.t * 'a) list

Sourcemodule type Term = sig ... end

On This Page

First Order Logic Definition
1. Representation of Patterns, Functions and Terms