Imp-language
An ACL2 library for the simple programming language Imp.
Imp is a simple programming language,
used mainly for didactic purposes.
It is found (with small variations) in textbooks and course materials,
such as:
This library contains a formalization of Imp in ACL2,
and is expected to be extended with additional material
related to formal verification and synthesis of Imp programs.
The package name of this library, "SIMPL-IMP",
consists of `SIMPL' for `Simple Programming Language'
(where the `P' can be in either word)
and `IMP' for `Imp'.
ACL2 libraries for other simple programming languages could use
a similar package "SIMPL-..." package naming scheme.
Imp is informally defined by the following elements:
- Arithmetic expressions,
consisting of
integer constants (of any size),
variables (i.e. symbolic names),
and a few arithmetic operators like addition and multiplication.
These expressions are always integer-valued,
without any size limitations;
the arithmetic operators are exact, i.e. not modular.
- Boolean expressions,
consisting of
boolean constants (one for truth and one for falsehood),
equalities and inequalities of arithmetic expressions,
boolean negation,
and boolean conjunction.
These expressions are always boolean-valued.
- Commands (i.e. statements),
consisting of
assignments of arithmetic expressions to variables,
sequencing (i.e. following a command with another command),
conditionals (`if-then-else'),
and loops.
These commands operate on a state consisting of
values stored in variables.
Imp does not have user-defined functions or procedures.
An Imp program is a command, which operates on a variable store.
Variables always contain integers (of any size);
they do not contain booleans.
Subtopics
- Semantics
- Semantics of Imp.
- Abstract-syntax
- Abstract syntax of Imp.
- Interpreter
- An interpreter for Imp.
