We will now consider a more realistic programming language, one where we can assign values to variables and execute control constructs such as if and while. The syntax for this imperative language, called IMP, is as follows:
Small-step Operational Semantics
We’ll first give a small-step operational semantics for IMP. The configurations in this language are of the form , , and , where is a store. The final configurations are of the form for commands, and for Boolean expressions, and ⟨𝜎, 𝑛⟩ for arithmetic expressions. There are three different small-step operational semantics relations: one each of the syntactic categories. For brevity, we will overload the symbol and use it to refer to all of these relations. Which relation is being used will be clear from context. The evaluation rules for arithmetic and Boolean expressions are similar to the ones we’ve seen before. However, note that since the arithmetic expressions no longer contain assignment, Arithmetic and Boolean Expressions can not update the store.
Arithmetic ExpressionsBoolean ExpressionsCommands For if commands, we reduce the test until we get true or false and then we execute the appropriate branch: For while loops, the above strategy doesn’t work (why?). Instead, we use the following rule, which can be thought of as “unrolling” the loop, one iteration at a time. We can now take a concrete program and see how it executes under the above rules. Consider we execute the program The execution works as follows: where is an abbreviation for the while loop .
Large-step Operational Semantics for IMP
We define large-step evaluation relations for arithmetic expressions, Boolean expressions, and commands. The relation for arithmetic expressions relates an arithmetic expression and store to the integer value that the expression evaluates to. For Boolean expressions, the final value is in . For commands, the final value is a store. Again, we overload the symbol and use it for any of these three relations; which relation is intended will be clear from context. We also use nfix notation, for example writing if .
The small-step operational semantics suggests that the loop should be equivalent to the command . Can we show that this indeed the case that the language is defined using the above large-step evaluation? First, we need to to be more precise about what "equivalent commands" mean. Our formal model allows us to define this concept using large- step evaluations as follows. ( One can write a similar definition using in small-step semantics.)
Definition (Equivalence of commands). Two commands and are equivalent (written ) if, for any stores and , we have We can now state and prove the claim that and are equivalent.
Theorem. Proof. Let be an abbreviation for . We want to show that for all stores and , we have: For this, we must show that both directions ( and ) hold. We’ll show only direction , the other is similar.
Assume that and are stores such that . It means that there is some derivation that proves for this fact. Inspecting the evaluation rules, we see that there are two possible rules whose conclusions match this fact: and . We analyze each of them in turn.
. The derivation must look like the following. Here, we use to refer to the derivation of . Note that in this case, We can use to derive a proof tree showing that the evaluation of yields the same final state : . In this case, the derivation has the following form. We can use , , and to show that the evaluation of yields the same final state Hence, we showed that in each of the two possible cases, the command evaluates to the same final state as the command .
