CS代考 COMP9164 Supplementary Lecture Notes – cscodehelp代写
COMP3161/COMP9164 Supplementary Lecture Notes
Imperative Programming
Liam O’ ̊ October 3, 2021
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.
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 ::= |
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
factorial of a fixed constant N:
Static Semantics
m := 1; whilei
NameError: name ’x’ is not defined
4.2 Default value semantics
In many programming languages, variables that are declared are automatically initialised to a default value. For example, the following Java program will always print 1 because Java initialises all fields to a default value—in the case of int, that’s 0.
public class test { static int x;
public static void main(String[] args) { System.out.println(x+1);
To adapt our operational semantics above to default-value semantics, we could replace the declaration rule with the following:
declared. Now, our crash-and-burn example can be evaluated as follows:
(σ·x):x→0 ⊢ x+1⇓1 ((σ·x):x→0,y:=x+1) ⇓ (σ·x):x→0:y→1 (σ,varx·y:=x+1) ⇓ σ:y→1
2Not a precise analogy, since Python doesn’t do explicit variable declarations. 5
((σ1 ·x):x→0,s)⇓σ2 (σ ,varx·s)⇓(σ |σ1)
Here, initialisation is modelled by immediately updating all variables to 0 as soon as they are
Note that the last step in the derivation relies on the fact that the expression ((σ · x) : x → 0 : y → 1)|σx
simplifies to σ : y → 1. You may want to convince yourself that this makes sense. 4.3 Junk data semantics
Most implementations of C will “initialise” variables by letting them inherit whatever junk data happened to live in the variable’s memory location beforehand.3 This can lead to unpredictable runtime behaviour. One way of capturing this unpredictability is with the following rule:
n. By choosing to instantiate n to 0, we can derive the judgement (σ,varx·y:=x+1) ⇓ σ:y→1
using the exact same proof tree as for the default-value example. But we can also prove the following:
(σ·x):x→5 ⊢ x+1⇓6 ((σ·x):x→5,y:=x+1) ⇓ (σ·x):x→5:y→6 (σ,varx·y:=x+1) ⇓ σ:y→6
The resulting semantics is non-deterministic: the final state (if one exists) is not unique. In real- world terms, this means the program may be observed to behave differently depending on lowerer- level details, e.g., in the compiler implementation, the hardware, or the runtime environment.
5 Hoare Logic
Because our language has been defined with compositional control structures inspired by struc- tured programming, we can write a compositional proof calculus for proving properties about our programs. This is a common type of axiomatic semantics, an alternative to the operational semantics we have defined earlier.
While scopes were important in previous sections, Hoare logic is usually presented in a setting where all variables are global. To avoid bogging down the presentation, we’d like to do the same. Therefore, from now on, we will start pretending that the var construct does not exist, and that all variables are declared.
Hoare Logic involves proving judgements of the following format:
Here φ and ψ are logical assertions, propositions that may mention variables from the state. The above judgement, called a Hoare Triple, states that if the program s starts in any state σ that satisfies the precondition φ and (σ, s) ⇓ σ′, then σ′ will satisfy the postcondition ψ.
3The situation in C is actually a bit more nuanced than this. Initialisation behaviour depends on the storage class, and uninitialised variables may contain bit patterns that do not represent values of the intended type. This may lead to crashing and burning.
((σ1 ·x):x→n,s)⇓σ2 (σ ,varx·s)⇓(σ |σ1)
This is almost identical to the default-value rule, except we’ve replaced the 0 with a free variable
Here’s an example of a Hoare triple:
To prove a Hoare triple, it is undesirable to use the operational semantics directly. We could, but it gets messy, and requires setting up an induction every time you encounder a while loop. Instead we shall define a set of rules to prove Hoare triples directly, without appealing to the operational semantics.
The rule for skip simply states that any condition about the state that was true before skip was executed is still true afterwards, as this statement does not change the state:
{φ} skip {φ}
The rule for sequential composition states that in order for s1;s2 to move from a precondition of φ to a postcondition of ψ, then s1 must, if starting from a state satisfying φ, evaluate to a state satisfying some intermediate assertion α, and s2, starting from α, must evaluate to a state satisfying ψ.
{φ} s1 {α} {α} s2 {ψ}
{φ}s1;s2 {ψ}
For a conditional to satisfy the postcondition ψ under precondition φ, both branches must satisfy ψ under the precondition that φ holds and that the condition either holds or does not hold, respectively:
{φ∧e} s1 {ψ} {φ∧¬e} s2 {ψ}
{φ}ifethens1 elses2 fi{ψ}
Seeing as while loops may execute zero times, the precondition φ must remain true after the while loop has finished. In addition, after the loop has finished, we know that the guard must be false. Furthermore, because the loop body may execute any number of times, the loop body must maintain the assertion φ to be true after each iteration. This is called a loop invariant.
{φ∧e} s {φ}
{φ} while e do s od {φ∧¬e}
For an assignment statement x := e to satisfy a postcondition φ, the precondition must effectively state that φ holds if x is replaced with e. Therefore, once the assignment has completed, x will indeed be replaced with e and therefore φ will hold. Try this on a few simple examples if you are not convinced:
{φ[x := e]} x := e {φ}
There is one more rule, called the rule of consequence, that we need to insert ordinary logical reasoning into our Hoare logic proofs, allowing us to change the pre- and post-conditions we have to prove by way of logical implications:
φ ⇒ α {α} s {β} β ⇒ ψ {φ} s {ψ}
This is the only rule that is not directed entirely by syntax. This means a Hoare logic proof need not look like a derivation tree. Instead we can sprinkle assertions through our program, and specially note uses of the consequence rule.
Note: An example verification of factorial using Hoare logic is provided in the Week 5 slides. 7
m := 1; whilei
