module Make: functor (C : sigend) -> functor (Var : Var) -> sig .. end
| Parameters: |
C |
: |
sig
type t
val context : t context
end
|
Var |
: |
Var
|
|
type
There are two components in the representation of a transition: its transformand its guard. The transform maps each variable that is
written during the transition to a term over its input variables.
The guard is a formula that describes the condition under which the
transition may be executed. The set of variables that appear in the
transform or the guard are called the footprint of the
transition.
type Transition.Var.t
val equal : t -> t -> bool
Test whether two transitions are equal up to logical equivalence and
renaming skolem constants. The input transitions must be normal in the
sense that (1) the transform only assigns skolem constants to terms
(e.g., we may have x := x' with guard x' = x + 1, but may not have
x := x + 1) and (2) every skolem constant that appears in the guard
also appears in the transform.
val compare : t -> t -> int
Compare is a purely syntactic comparison. Two transitions tr and
tr' can be equivalent (equal tr tr' = true) but have compare tr tr'
!= 0.
val pp : Format.formatter -> t -> unit
val show : t -> string
val construct : C.t Syntax.formula ->
(var * C.t Syntax.term) list -> t
Guarded parallel assignment
val assume : C.t Syntax.formula -> t
assume phi is a transition that doesn't modify any variables, but can
only be executed when phi holds
val assign : var -> C.t Syntax.term -> t
assign v t is a transition that assigns the term t to the variable
v.
val parallel_assign : (var * C.t Syntax.term) list -> t
Parallel assignment of a list of terms to a list of variables. If a
variable appears multiple times as a target for an assignment, the rightmost
assignment is taken.
val havoc : var list -> t
Assign a list of variables non-deterministic values.
val mul : t -> t -> t
Sequentially compose two transitions.
val add : t -> t -> t
Non-deterministically choose between two transitions
val zero : t
Unexecutable transition (unit of add).
val one : t
Skip (unit of mul).
val widen : t -> t -> t
Widen abstracts both input transitions to the Cube abstract domain,
performs the Cube widening operator, and then converts back to a transition.
The resulting transition is normal in the sense described in equal.
val exists : (var -> bool) -> t -> t
exists ex tr removes the variables that do not satisfy the predicate
ex from the footprint of a transition. For example, projecting a
variable x out of a transition tr is logically equivalent to
(exists x. tr) && x' = x.
val is_zero : t -> bool
val is_one : t -> bool
val mem_transform : var -> t -> bool
Is a variable written to in a transition?
val get_transform : var -> t -> C.t Syntax.term
Retrieve the value of a variable after a transition as a term over input
variables (and Skolem constants)
val transform : t -> (var * C.t Syntax.term) BatEnum.t
Enumerate the variables and values assigned in a transition.
val guard : t -> C.t Syntax.formula
The condition under which a transition may be executed.
val interpolate : t list ->
C.t Syntax.formula ->
[ `Invalid | `Unknown | `Valid of C.t Syntax.formula list ]
Given a path (list of transitions tr_1 ... tr_n) and a post-condition
formula, determine whether the path implies the post-condition. If yes,
return a sequence of intermediate assertions phi_1 ... phi_n that
support the proof (for each i, { phi_{i-1} } tr_i { phi_i } holds,
where phi_0 is true and phi_n implies the post-condition).
val valid_triple : C.t Syntax.formula ->
t list ->
C.t Syntax.formula -> [ `Invalid | `Unknown | `Valid ]
Given a pre-condition P, a path path, and a post-condition Q,
determine whether the Hoare triple {P}path{Q} is valid.
val defines : t -> var list
val uses : t -> var list
val abstract_post : (C.t, 'abs) SrkApron.property ->
t -> (C.t, 'abs) SrkApron.property
module Iter:
Iteration domain.