package catala

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Verification

Generating verification conditions

From the Dcalc intermediate representation, the module Verification.Conditions provides functions to generate verification conditions for each scope definition present in the program. These verification conditions, if proven true, can assert the well-behaved execution of the scope definition: absence of empty or conflict errors.

Related modules:

Generic solver

As Catala ambitions to mix and match different proof backends to solve the verification conditions, the compiler features a functorial interface common to all backends to rationalize the inputs and outputs. More precisely, it is sufficient for a proof backend to implement Verification.Io.Backend to enjoy the normalized input/output (I/O) of Verification.Io.BackendIO through the functor Verification.Io.MakeBackendIO.

Finally, the Verification.Solver calls the I/O functions of the different backends to perform the solving of the various verification conditions.

Related modules

Z3 proof backend

One of the way to prove the Verification.Conditions.verification_conditions true is to encode them into a Z3 query. The Catala compiler features a complete encoding of the Dcalc intermediate representation into Z3, which can be used to launch Z3 queries and collect results to inform potential Dcalc program optimizations.

Related modules:

OCaml

Innovation. Community. Security.