Program Semantics

program-proofing

Definition

Program Semantics

The semantics of a program $[\Pi ]$ is the function computed by a program $\Pi$.

Formally, for every program configuration $(\Pi ,\sigma )$ and every final configuration ${\sigma }^{\prime }$:

$$[\Pi ]\sigma ={\sigma }^{\prime }\text{iff}(\Pi ,\sigma ){\Rightarrow }^{\ast }{\sigma }^{\prime }$$

If no such ${\sigma }^{\prime }$ exists, then $[\Pi ]\sigma$ is undefined.

Here, ${\Rightarrow }^{\ast }$ denotes the reflexive and transitive closure of the program transition relation.

Semantic Equivalence

Two programs $\Pi$ and $\Omega$ are semantically equivalent if they compute the same program semantics.

$$\Pi \equiv \Omega \text{iff}[\Pi ]=[\Omega ].$$

This means that for every input state $\sigma$, both programs produce the same output state whenever either of them terminates.

Important

Semantic equivalence does not distinguish between different causes of non-termination or failure. If one program loops forever and another aborts, they are still semantically equivalent as long as they compute the same partial function on all terminating inputs.

Sequencing

Associative Sequencing

Sequencing is associative at the level of program semantics:

$$[({\Pi }_1;{\Pi }_2);{\Pi }_3]=[{\Pi }_1;({\Pi }_2;{\Pi }_3)]$$

So the order of bracketing does not change the computed function.

function composition.

$([({\Pi }_1;{\Pi }_2);{\Pi }_3]=[{\Pi }_3][{\Pi }_1;{\Pi }_2])$
$(=[{\Pi }_3]([{\Pi }_2][{\Pi }_1]))$
$(=([{\Pi }_3][{\Pi }_2])[{\Pi }_1])$
$(=[{\Pi }_2;{\Pi }_3][{\Pi }_1])$
$(=[{\Pi }_1;({\Pi }_2;{\Pi }_3)])$

Here we use that sequencing corresponds to composition:

$$[\Pi ;\Omega ]=[\Omega ][\Pi ]$$

Therefore, sequential programs can be grouped arbitrarily.