Axiomatic Semantics

Notes from Chapt. 2, Multithreaded and Distributed Programming

by Greg Andrews, 2000.

Formal Logical Systems: a mathematical abstraction. We must apply it to a domain of discourse – proving programs correct.

· A set of symbols

· A set of formulas constructed from these symbols

· A set of distinguished formulas, called axioms that are a priori true

· A set of inference rules

Inference Rules have the form:

H₁, H₂, … H_n / C, where H_i are hypotheses and C is a conclusion.

If all H_i are true, we can infer C.

A proof in a formal logical system is a sequence of lines, each of which is an axiom or can be derived from previous lines by application of an inference rule. A theorem is any line in a proof.

An interpretation of a logic maps each formula to true or false.

An axiom is sound if it maps to true.

An inference rule is sound if its logic is sound.

Programming Logic – a formal logic system that allows us to prove properties of programs

· The formulas are called triples: {P} S {Q}, where P and Q are predicates and S is a statement in the statement list.

· Interpretation of triples establishes the relationship between predicates (assertions) and the S statement list.

· Interpretation of a Triple : The triple {P} S {Q} is true if, whenever execution of S is begun in a state satisfying P and execution of S terminates, the resulting state satisfies Q.

· P and Q are assertions about the program state.

· P is called the Precondition and Q is called the Post-condition

Example:

{x==0} x = x + 1; { x==1} is a theorem.

Assignment Axiom: {P_{x <-e}} x = e {P}

· If you want an assignment to result in a state satisfying predicate P, then the prior state must satisfy P with variable x textually replaced by e

· {x == 0} x = 1; { x==1}

Composition Rule: {P} S₁ {Q}, {Q} S₂ {R} / {P} S₁ ; S₂ {R}

If Statement Rule:

{P ^ B} S {Q}, {P ^ notB} => Q / {P} if (B) S; {Q}

Example: {true}

m = x;

{ m==x};

If (y > m)

m = y;

{(m == x ^ m >= y) or (m == y) ^ m > x)}

While Statement Rule:

{I ^ B} S {I} / {I} while(B) S; {I ^ ~B}

Example: need loop invariant I

i = 1;

{i = 1 ^ (forall j: j <= j < i: a[j] != x}

While (a[i] != x}

i = i+1;

{(forall j: 1 <= j < i: a[j] != x) ^ a[i] == x}

Rule of Consequence:

P’ -> P, {P} S {Q}, Q->Q’ / {P’} S {Q’}

Example:

{ x== 0} x = x+1; {x == 1} by Rule of Consequence the following is true

{x == 0} x = x+ 1; {x > 0} weakens postcondition

Semantics of Concurrent Execution

Await Statement Rule: {P ^ B} S {Q} / {P} <await (B) S;> {Q}

· “if execution of S begins in a state in which both P and B are true, and S terminates, then Q will be true”

Co Statement Rule: co S₁; // S₂, // … // S_n; oc;

{P_i} S_i {Q_i} are interference free /

{P₁ ^ … ^ P_n}

co S₁; //…// S_n; oc

{Q₁ ^ … ^ Q_n}

Interference free: A process interferes with another process if it executes an assignment that invalidates an assertion in the other process

{x == 0}

co < x = x+ 1;> // < x = x+2;> oc

{x == 3} interference thru non-deterministic execution

Proof outline:

{x == 0}

co {x ==0 or x==2}

<x = x+1;>

{x == 1 or x==3}

// {x ==0 or x==1}

<x = x+2;>

{x==2 or x==3}

oc

{x==3}

Definition: a critical assertion is a precondition or post-condition that is not within an await statement

Noninterference: Let a be an assignment action in one process and let pre(a) be its precondition. Let C be a critical assertion in another process. If necessary, rename local variables in C so their names are different from the names of local variables in a and pre(a). Then a does not interfere with C if the following is a theorem in programming logic.

{C ^ pre(a)} a {C}

In short, critical assertion C is invariant with respect to execution of assignment action a.

Global Invariants

Suppose I is a predicate that references global variables. The I is a global invariant with respect to a set of processes if

· I is true when the processes begin execution and

· I is preserved by every assignment action