This repository provides implementations for various semantics for the IMP language of ETHZ's Formal Methods course.

Currently only core IMP is supported.

The following semantics are supported:

• big-step semantics (aka. natural semantics)
• small-step semantics (aka. structural operational semantics)
• axiomatic semantics

To install the interpreters, clone the git repo, grab the Z3 Prover's library files corresponding to your OS (e.g. for Windows libz3.dll and libz3.lib from the *-win.zip archive) and build the project.

$ git clone git@github.com:skius/imp
$ cd imp/
$ # put the z3 files here
$ cargo build

./imp <filename> <true/false: run big-step> <true/false: run small-step> <total/partial/false: run axiomatic>

For example, ./imp examples/square.imp true true partial evaluates examples/square.imp with both big-step and small-step semantics and verifies the given derivations for partial correctness, and ./imp examples/divide.imp false false total just verifies examples/divide.imp for total correctness.

The core IMP syntax is precisely the same as introduced in the lecture (incl. shorthands). The syntax to verify axiomatic derivations is the same as the introduced "Proof Outline", except that there are no semi-colons and in the case of total correctness proofs no ⇓.

The syntactic sugar for ->, true and false boolean expressions is also implemented as usual.

Files that use the proof outline syntax (e.g. examples/swap.imp) may be used by all semantics, but files that only use the core IMP syntax (e.g. examples/abs.imp) may only be used by the big-step and small-step semantics.

Note for proof outline syntax: You may use ⊨ or |= for rules of consequence.
Additionally, one must be very careful writing the conditions for if and while - their conditions must be ANDed at the highest level:

# this is okay (note the parentheses that force precedence)
{i <= a and b = a * i}
while (i # a) do
    {i # a and (i <= a and b = a * i)}
    
# this is not
{i <= a and b = a * i}
while (i # a) do
    {i # a and i <= a and b = a * i}
    
# because it is equivalent to
{i <= a and b = a * i}
while (i # a) do
    {(((i # a) and i <= a) and b = a * i)}
# where the condition (i # a) is at the innermost/lowest level instead of the highest.

To make sure no errors happen because of to this, always write these assertions with explicit parentheses like b and (P) resp. b and (P) and e = Z for while loops in total correctness proofs (see examples/divide.imp for an example of a total correctness proof).

You might not be happy with just IMP operators in your pre-/post-conditions, so just like in the course, this tool allows you to define your own functions (and offers the built-in ! factorial function). The syntax for function calls should be familiar, but function definitions are a bit odd; at the moment their body must consist of a single expression, which may contain a recursive call. Also, the body's expression supports the ternary ? : operator to provide if-then-else control flow.

See examples/gcd_partial.imp for a proof making use of a user-provided function definition, and examples/factorial_partial for a proof making use of the built-in factorial !. Note that the tool is currently unable to verify either of those proofs, it reports UNKNOWN.