Tute (Week 4)

Ideally, static semantics judgements such as the \(\mathbf{ok}\) judgements should allow us to make some predictions about the dynamic behaviour of the program. In this case, we'd hope that an \(\mathbf{ok}\) program would be guaranteed not to misbehave in some way.

1. Give an example of a program where all variables are initialised before use, but that is nonetheless not \(\mathbf{ok}\).

Suppose we have proven that

\[ \emptyset;\emptyset\vdash s\;\mathbf{ok} \leadsto \emptyset\]

1. The slides gave three different semantics for uninitialised variables: crash-and-burn, default values and junk data. These are also mentioned in the related longform notes Under each of these interpretations, state (informally, in English) some desirable property about the runtime behaviour of \(s\) that follows as a result of the \(\mathbf{ok}\) judgement above.
2. Can you think of a way to formalise these properties as logical statements involving judgements?

We never bothered specifying whether sequential composition in TinyImp is left-associative or right-associative. That is, whether \(s_1;s_2;s_3\) should be evaluated as \((s_1; s_2); s_3\), or as \(s_1; (s_2; s_3)\).

Prove that \((\sigma_1, (s_1;s_2);s_3) \Downarrow \sigma_2\) holds iff \((\sigma_1, s_1;(s_2;s_3)) \Downarrow \sigma_2\)

Suppose we wanted to extend TinyImp with a new type of loop:

\[ \mathbf{do}\ s\ \mathbf{until}\ e\]

Which, running the loop body \(s\) at least once, checks the guard of the loop after the loop body has executed, terminating if it is true (i.e. nonzero).

1. Give big-step semantics rules for this construct in the style of the lecture slides.
2. Propose a translation of this construct into existing TinyImp constructs.
3. Validate your translation by showing that the Hoare logic rule for this loop is derivable for your translation:

\[ \dfrac{ \{ \varphi \}\ s\ \{ \varphi \} }{\{ \varphi \}\ \mathbf{do}\ s\ \mathbf{until}\ e\ \{ \varphi \land e \} } \]