pgm_wp.mli 233 Bytes
Newer Older
1 2 3 4

open Why
open Theory

5
val file : theory_uc -> Pgm_ttree.file -> theory
6 7 8
  (** takes as input the result of [Pgm_typing.file] and produces
      a theory containing the verification conditions as goals,
      one for each function *)