38

Small-step semantics defines a method to evaluate expressions one computation step at a time. Formally speaking, a small-step semantics for an expression language $E$ is a relation $\rightarrow : E \times E$ called the reduction relation. Small-step semantics describes what happens to an expression in detail. It's able to give a precise account of even non-...


5

Your attempt does not work. Note that $s_1$ is never executed. (And if you prepend the right-hand side with "$s_1;$", it will be executed multiple times.) What you can do is to translate the for loop into an equivalent while loop: $$\sigma,\text{for } s_1, e_1, e_2, s_2 \text{ endfor} \to \sigma, s_1; \text{while } e_1 \text{ do } s_2; e_2 \text{ endwhile}....


3

Don't proceed by induction on $P$, i.e. by structural induction on the syntax of programs. This is because structural induction is quite weak, and is likely to fail on while loops. Look at the inference rules for the big step semantics for while, in particular at the while-true rule which handles the case where the guard is true. In such case, you'll see ...


2

It seems you have some doubts about the first added evaluation rule $$ \frac {\langle B, s \rangle \to \!\, \langle B', s' \rangle} {\langle \mathsf{assert}\ B\ \mathsf{before}\ C, s \rangle \to \!\, \langle \mathsf{assert}\ B'\ \mathsf{before}\ C, s' \rangle} $$ It might be redundant, but I ought to point out it's one rule: the top part is called a premise ...


2

In general, the only persistent pieces information in a deduction rule (like the ones in the wikipedia article) are the variables which are shared between one of the premises and the conclusion of the rule. So in effect, a findOne function that operates on a given (fixed) string and returns the position of the first bit which is one would have to pass the ...


Only top voted, non community-wiki answers of a minimum length are eligible