C0p auxiliary calculations

What are auxiliary calculations of an C0p execution supposed to look like? They were part of the task in the exam if I’m not mistaken, but I can’t find anything about those in the book.

If you take a look at the Definition 6.3.4: Operational Semantics of C0 of C0(pbt), you see certain preconditions that need to be met to apply the rules.
Some of them are again operational semantics steps (for instance for exec and subst) that require inductive reasoning (quite simple for the operational semantics. Therefore, we often do not draw these trees explicitly).
Others like the ones for [Assign] require additional reasoning of another form.

For assign, we for instance have to prove that the R-evaluation of the expression e in the current state \sigma results in a value v.

R[\![e]\!] \sigma = v\in Val

The task asked you to explicitly show the evaluation as it is not trivial.
You can use the Definition 6.3.2: Expression Evaluation in C0 to derive the value (and show that it is a value).

For preconditions in these rules see:

1 Like