module Transfer_logic:sig
..end
kf
for a given behavior b
.
This may result in splitting post_states
if the postconditions contain
disjunctions.module type S =sig
..end
module Make:functor (
Domain
:
Abstract_domain.S
) ->
functor (
States
:
Partitioning.StateSet
with type state = Domain.t
) ->
S
with type state = Domain.t and type states = States.t