Program verification extension

[Zelatrix]

Extend the parser so that it can handle verification conditions in Hoare logic. A specification can either contain a precondition and postcondition specified by the user, or it can be empty. If the user does not specify a precondition, then it is assumed that the precondition is always true.

These pre- and post-conditions are then fed into the Z3 theorem prover in order to verify whether the axioms contained in the program are provable in Hoare logic.