module Why3:S
A certificate generator for the deductive platform Why3. These certificates can be verified by a herd of automated provers
val certificate : Ast.t_system -> Node.t list -> unitthis takes a system in input and the list of visited nodes, of which the disjunction constitutes an inductive invariant for the system.
certificate s visited must write on the disk a certificate of induction
(initialization, preservation, and implication) and print the location
of the generated certificate on stdout.