Module Rac

module Rac: sig .. end

Runtime Assertion Checkers for WhyML programs

type oracle_quant_var = Pinterp_core.env -> Term.vsymbol -> Pinterp_core.Value.value option

An oracle to get all-quantified variables during RAC. Used to progress when the transformation "compute_in_goal" blocks on a quantifier.

val oracle_quant_var_dummy : oracle_quant_var

Always returns in None.

val oracle_quant_var : ?bind_univ_quant_vars:bool ->
       ?bind_univ_quant_vars_default:bool ->
       Pinterp_core.oracle -> oracle_quant_var

Derive an oracle for quantified variables from a normal oracle.

module Why: sig .. end

RAC implementation using a Why3 transformation and prover