Hi. I was going through the small step semantics illustrated with Coq at https://github.com/coq-community/semantics/blob/master/little.v
There I am having trouble understanding one of the constructors.
It's a type representing a small step evaluation for a loop:
| SOS4 :
forall r b i, beval r b true ->
sos_step r (while b i) (sequence i (while b i)) r
With type annotations:
| SOS4 :
forall (r:env) (b:bexpr) (i:instr), beval r b true ->
sos_step r (while b i) (sequence i (while b i)) r
(where bexpr
denotes a boolean expression.
So this constructor represents the case where the condition for the loop is still true.
How can we be sure that the environment remains same after the execution of the instruction i
?
That's what this constructor indicates, right?
Given an environment r
, loop condition b
and instruction i
as the loop body, result would be the _same_ environment.
What am I missing here?
The instruction i
has not been executed yet.
Maybe a dumb question, but when will i
be evaluated?
At the next step.
while b i -> sequence i (while b i) -> sequence i' (while b i) -> ... -> sequence skip (while b i) -> while b i
Ah.. I think I get it now. Thanks!
Julin S has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC