impli

This is an interpreter for the imperative toy language IMP from the course Formal Methods and Functional Programming at ETH Zürich. It is published under the MIT license.

Usage

To start the REPL, just run impli with no arguments. Pass the path of an IMP source file as argument to interpret it. Directly execute a statement with the --command option or print its AST with --ast. Select the structural small-step semantics with --structural and set the verbosity level of the REPL with --verbose LEVEL (or interactively with :set verbose LEVEL). In the initial state all variables are uninitialized with zero and no procedure is defined. Find some sample programs in docs/examples/.

Installation

Build artifacts for macOS, Linux, and Windows are available under GitHub Releases. You can download the latest version directly using curl. Replace BINARY with the OS appropriate binary name found on the releases page, for example impli-aarch64-darwin for Apple Silicon or impli-x86_64-windows.exe for x86 Windows.

curl -Lo impli https://github.com/bfeitknecht/impli/releases/latest/download/BINARY

You may need to modify execution privileges and remove the quarantine attribute on macOS.

chmod +x impli
xattr -d com.apple.quarantine impli

Specification

The most apparent deviations from the specifications are that parentheses are not required for arithmetic or boolean operations in expressions, and sequential composition in statements. Additionally, the write-only placeholder variable _ allows discarding of values. It can only be used on the lefthandside of variable definitions. For complete specification of the syntax refer to the EBNF.

The table below depicts the correspondence between semantics functions defined in the lectures and according functions in this project for $\sigma$ equivalent to state. For an overview of all natural semantics inference rules, check out the paper.

FMFP	impli
$\sigma_{\text{zero}}$	IMP.State.initial
$\sigma(x)$	IMP.State.getVar state x
$\sigma[x \mapsto n]$	IMP.State.setVar state x n
$\langle s, \sigma \rangle \to \cdot$	IMP.Semantics.Natural.run s state
$\langle s, \sigma \rangle \to_{1} \cdot$	IMP.Semantics.Structural.step (Source s, state)
$\langle s, \sigma \rangle \to_{1}^{*} \cdot$	IMP.Semantics.Structural.run s state
$\mathcal{N}[[n]]$	n
$\mathcal{A}[[a]]\sigma$	IMP.Expression.evaluate a state
$\mathcal{B}[[b]]\sigma$	IMP.Expression.evaluate b state

Both semantics run in any monad providing IMP.Effect.MonadIMP (input, output, choice, havoc). Some extensions behave as follows:

• break immediately exits the innermost enclosing loop. A break outside a loop is rejected before execution.
• time s evaluates to the number of small-step transitions of executing s (reads and havocs yield zero, choices go left), limited to one million steps.
• timeout s after a end executes at most a small-step transitions of s. It and alternate are delegated to the structural semantics when interpreting with natural semantics.
• par combines the states of both branches executed independently under natural semantics, and interleaves the branches at every step under structural semantics.

Star History