module Eval_funs:sig
..end
Evaluate kf
in state with_formals
, first by reducing by the
preconditions, then by evaluating the assigns, then by reducing
by the post-conditions.
The computation varies depending on the number of behaviors
(single or multiple). Both methods are correct for any number
of behaviors, but one is more efficient and the other is more precise.
val force_compute : unit -> unit
main
function.