COMP3161/COMP9164 Supplementary Lecture Notes
Imperative Programming
Liam O’Connor September 22, 2020
The term imperative refers to programming languages that are defined as a series of commands that manipulate both the external world and internal state. The order in which commands are executed is significant in an imperative language, as the state changes over time.
Typically, states can be defined as a mapping from variable names to their values, however some lower-level languages may require more complex models. For example, to specify an assem- bly language, a detailed model containing a processor’s registers and accessible memory may be required.
Early imperative languages allowed not just global state but also global control flow – a go to statement could be used to transfer control to anywhere else in the entire program. Edsger Dijkstra was one of the first computer scientists to advocate the notion of structured programming, as it allowed imperative control flow to be made amenable to local reasoning. This movement was responsible for the introduction of things like loops, conditionals, and subroutines or functions to imperative language.
We will define an imperative language based on structured programming, describe its static and dynamic semantics, and specify a Hoare logic to demonstrate the benefits of structured pro- gramming for program verification.
1 Syntax
We’re going to specify a language TinyImp. This language consists of state-changing statements and pure, evaluable arithmetic expressions, as we have defined before.
Stmt ::= |
| | | |
Expr ::=
skip
x := Expr
var y · Stmt
if Expr then Stmt else Stmt fi while Expr do Stmt od
Stmt ; Stmt
⟨Arithmetic expressions⟩
Do nothing Assignment Declaration Conditional
Loop Sequencing
The statement skip does nothing, x := e updates the (previously-declared) variable x to have a new value resulting from the evaluation of e, var y · s declares a local variable that is only in scope within the statement s, if statements and while loops behave much like what you expect, and s1;s2 is a compound statement consisting of s1 followed sequentially by s2.
For the purposes of this language, we will assume that all variables are of integer types. This means for boolean conditions, we will adopt the C convention that zero means false, and non-zero means true.
Here are some example programs written in TinyImp. Firstly, a program that computes the
1
factorial of a fixed constant N:
2
Static Semantics
var i ·
var m ·
i := 0;
m := 1; whilei