Module Prover

module Prover: sig .. end

Must-subtraction implementation

This module implements the Must-subtraction algorithm, also known as frame inference, which is a generalization of entailment checking.

For efficiency purposes, the implementation differs substantially from (Berdine, Calcagno, O'Hearn, 2005).

val default_prover : Assertions.prover

val verbose : int Pervasives.ref

val args : (Arg.key * Arg.spec * Arg.doc) list