module WP_HoareRef: CfgWP.Computer(MHoareRef)
CfgWP.Computer
(
MHoareRef
)
module VCG: CfgWP.VC(M)
CfgWP.VC
M
module WP: Calculus.Cfg(VCG)
Calculus.Cfg
VCG
class thecomputer : Model.t -> object .. end
Model.t ->
object
end
val create : Model.t -> Generator.computer
Model.t -> Generator.computer