mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-16 14:57:13 +03:00
41 lines
1.6 KiB
Plaintext
41 lines
1.6 KiB
Plaintext
{0 Verification}
|
|
|
|
{1 Generating verification conditions }
|
|
|
|
From the {{: dcalc.html} Dcalc} intermediate representation, the module
|
|
{!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:
|
|
|
|
{!modules: Verification.Conditions}
|
|
|
|
{1 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 {!module-type: Verification.Io.Backend}
|
|
to enjoy the normalized input/output (I/O) of {!module-type: Verification.Io.BackendIO}
|
|
through the functor {!module: Verification.Io.MakeBackendIO}.
|
|
|
|
Finally, the {!module: Verification.Solver} calls the I/O functions of the different
|
|
backends to perform the solving of the various verification conditions.
|
|
|
|
Related modules
|
|
|
|
{!modules: Verification.Io Verification.Solver}
|
|
|
|
{1 Z3 proof backend}
|
|
|
|
One of the way to prove the {!type: Verification.Conditions.verification_condition}s
|
|
true is to encode them into a Z3 query. The Catala compiler features a
|
|
complete encoding of the {{: dcalc.html} Dcalc} intermediate representation
|
|
into Z3, which can be used to launch Z3 queries and collect results to
|
|
inform potential Dcalc program optimizations.
|
|
|
|
Related modules:
|
|
|
|
{!modules: Verification.Z3backend} |