ProgProving is a LaTeX package that aims to help people prove their codes.

ProgProving requires:

• amsmath

You can find the downloads for each version with their release notes in the releases page.

You can install ProgProving by downloading the package to your folder and importing it into your LaTeX files using :

\usepackage{progproving}

This command allows you to easily display the state of a program.

Requires Math mode

Usage :

\state{<state>}

Example :

\state{x = 1}

Example output :

{x = 1}

This command allows you to easily display a sp.

Requires Math mode

Usage :

\ppsp{<instructions>, <state>}

Example :

\ppsp{x := 2, \state{x = 1}}

Example output :

sp(x := 2,{x = 1})

This command allows you to easily display a wp.

Requires Math mode

Usage :

\ppwp{<instructions>, <state>}

Example :

\ppwp{x := 2, \state{x = 1}}

Example output :

wp(x := 2,{x = 1})

This command allows you to easily display the precondition letter.

Usage :

\pre

This command allows you to easily display the postcondition letter.

Usage :

\post

This command allows you to easily display the invariant letter.

Usage :

\inv

This command allows you to easily display the loop condition letter.

Usage :

\cond

This command allows you to easily display the loop precondition letter.

Usage :

\lpre

This command allows you to easily display the loop postcondition letter.

Usage :

\lpost

This command allows you to easily display the loop initialisation letters.

Usage :

\init

This command allows you to easily display the loop iteration letters.

Usage :

\iter

This command allows you to easily display the loop termination letters.

Usage :

\term

You can find all contributors here.

All code is licensed for others under MIT (see LICENSE).