What is the significance of ⟨B, s⟩ -> ⟨B', s'⟩ as the initial rule in this question about small-step semantics?

Question

Revising for an exam and I'm trying to get to grips with operational semantics. Here's the exam question that prompted me posting this:

Exam Question:

We add to the language $\mathsf{SIMP}$ two new commands, with abstract syntax defined by the grammar rule:

$$C ::= \mathsf{assert}\ B\ \mathsf{before}\ C \mid \mathsf{abort}$$

The small step semantics of $\mathsf{SIMP}$ is extended with the following rules:

$$\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}$$

$$\frac{}{\langle \mathsf{assert}\ \mathsf{True}\ \mathsf{before}\ C, s\rangle \to \!\, \langle C, s \rangle}$$

$$\frac{}{\langle \mathsf{assert}\ \mathsf{False}\ \mathsf{before}\ C, s\rangle \to \!\, \langle \mathsf{abort}, s \rangle}$$

The configuration $\langle \mathsf{abort}, s \rangle$ is stuck (no transitions are available from this configuration). Explain with your own words the behaviour of the new commands.

Given $\mathsf{SIMP}$ Language:

$$ \begin{align*} C &::= \mathsf{skip} \mid l\ \mathsf{:=}\ E \mid C;\, C \mid \mathsf{if}\ B\ \mathsf{then}\ C\ \mathsf{else}\ C \mid \mathsf{while}\ B\ \mathsf{do}\ C \\ E &::= \mathsf{!}l \mid n \mid E\ op\ E \\ op &::= \mathsf{+} \mid \mathsf{-} \mid \mathsf{*} \mid \mathsf{/} \\ B &::= \mathsf{True} \mid \mathsf{False} \mid E\ bop\ E \mid \neg B \mid B \wedge B \\ bop &::= \mathsf{>} \mid \mathsf{<} \mid \mathsf{=} \\ \end{align*} $$

My Question:

Firstly let me get my understanding of the question out of the way: We're adding a new command $(C)$ to the list of commands we have defined in our $\mathsf{SIMP}$ language. $C$ asserts $B$ before $C$ or aborts the program/process running. Using small step semantics the question has shown us each step of the process as it runs. Here's my issue:

Assuming my knowledge is correct, every rule written below the line holds if what is written above it holds. If this is the case, what is the importance of the first line

$$\langle B,\ s \rangle \ \to \!\ \ \langle B',\ s' \rangle$$

The rule we have implemented makes no reference of a $B$ in some state $s$ becoming/transitioning into $B'$ in some state $s'$. How can that suddenly be what decides the rule

$$\langle \mathsf{assert}\ B\ \mathsf{before}\ C,\ s \rangle\ \to \!\ \ \langle \mathsf{assert}\ B'\ \mathsf{before}\ C,\ s' \rangle$$

I feel like that rule should be what we start with, not what comes in second. The rule we decided to add to $\mathsf{SIMP}$'s grammar seemed to be more about checking with $B$ before we continue on to $C$, not checking with $B$ so we can go to $B$ (or something to that effect?).

I know that it's not directly related to the exam question at hand but I feel like understanding why might clear up some gaps in my knowledge regarding operational semantics on the whole. That said, here is my answer to the exam question itself:

'The behaviour of the command $C$ ($C ::= \mathsf{assert}\ B\ \mathsf{before}\ C \mid \mathsf{abort}$) is such that when $B$ is asserted it must return either $\mathsf{True}$ or $\mathsf{False}$, as it is a Boolean command. When it returns $\mathsf{False}$ the program/process is aborted, meaning to transitions from this state cannot be made. If it returns $\mathsf{True}$ then you are able to continue on to $C$ in some state $s$.'

Is this correct? If not, where did I go wrong? Like I said, I don't understand the top two rules and as such I feel it hurts my answer not being able to include them in my reasoning.

Answer 1

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 of the rule, the bottom part is called a conclusion.

We call rules of this type rules of congruence (and the next two are computation rules). One needs rules of congruence to reduce subparts of a bigger expression or command, i.e. reduce something in its context. Usually, one applies rules of congruence until one can use a computation rule to dispose of some parts of the context. Here, the premise serves you as a means of reducing a Boolean expression $B$ to its value $(\mathsf{True}$ or $\mathsf{False})$.

Let me illustrate this by example: if you have a command $\mathsf{assert}\ \mathsf{True}\ \mathsf{before}\ \mathsf{skip}$, and an initial state $s$, then you reduce it to $\mathsf{skip}$ (without changing $s$) using the second added rule: $$ \langle \mathsf{assert}\ \mathsf{True}\ \mathsf{before}\ \mathsf{skip}, s\rangle \to \!\, \langle \mathsf{skip}, s \rangle $$

But what should we do if the command we've got is $\mathsf{assert}\ \mathsf{True \wedge \mathsf{True}}\ \mathsf{before}\ \mathsf{skip}$? There is no computation rules for this, i.e. rules that are able to get rid of the $\mathsf{assert}$... part. Here comes the congruence rule: first you reduce $\mathsf{True \wedge \mathsf{True}}$ to $\mathsf{True}$, using some evaluation rule defined for Booleans (not shown here) -- that's why you need the premise ${\langle B, s \rangle \to \!\, \langle B', s' \rangle}$ -- then you use the 2nd added rule to finish off your computation:

$$ \langle \mathsf{assert}\ \mathsf{True} \wedge \mathsf{True}\ \mathsf{before}\ \mathsf{skip}, s\rangle \to \langle \mathsf{assert}\ \mathsf{True}\ \mathsf{before}\ \mathsf{skip}, s\rangle \to \!\, \langle \mathsf{skip}, s \rangle $$