Skip to main content

pgcl2heyvl Frontend

The now deprecated pgcl2heyvl tool is a frontend for pGCL programs written in the syntax of the probably library Given an annotated pGCL program, it automatically generates HeyVL code for Caesar.

caution

The pgcl2heyvl tool is deprecated and its functionality is now fully integrated into Caesar itself. Simply use HeyVL statements and use the built-in proof rules on while loops.

Using HeyVL directly enables the use of the proof rule encodings with features of Caesar that pgcl2heyvl does not support, such as domain declarations or a more powerful set of expressions. Furthermore, Caesar's proof rules have support for slicing, which enables detailed error messages such as "the invariant is not inductive".

Installing pgcl2heyvl​

To run pgcl2heyvl, first install dependencies using poetry. Poetry is a build system and dependency manager for Python. Here are installation instructions for Poetry.

In the pgcl/pgcl2heyvl directory, install dependencies:

cd pgcl/pgcl2heyvl
poetry install

Using pgcl2heyvl​

After installation, use poetry run to run pgcl2heyvl.

cd pgcl/pgcl2heyvl
poetry run pgcl2heyvl FILE > OUTFILE

where FILE is a file name with the pGCL program and OUTFILE is the name of the output file with the HeyVL code.

The first line in FILE must include // ARGS: --post POST --pre PRE --k K. POST is a post-expectation, and PRE is a pre-expectation (in pGCL syntax). The K argument is an integer that specifies which k-induction to use for the encoding.

If the pGCL program includes a single loop, then PRE will be used as the loop invariant. When the program includes multiple loops, additional invariants must be specified using --invariant.

The command-line interface documentation is available by invoking poetry run pgcl2heyvl --help.

pGCL Examples​

You can find pGCL examples in the pgcl/examples directory. They include all necessary parameters to generate verifying HeyVL files.

For these examples, the generated HeyVL files are located under pgcl/examples-heyvl. Verification with caesar requires the --raw command-line flag since these files are just sequences of HeyVL statements.

Instructions on how to (re-)generate these examples are located in pgcl/examples-heyvl/README.md.

To execute caesar with the generated HeyVL files, refer to the benchmarks section of Caesar's documentation.

pGCL Syntax​

pgcl2heyvl uses the probably Python library to parse and type-check pGCL programs. That means the pGCL syntax of probably is used for the pGCL programs and the --pre, --post, and --invariant command-line parameters.

There is no formal specification for the exact pGCL syntax that probably accepts, but here are some pointers: