ground value false, even if the variables bB and bY **were symbolic. This is described by the** modified version of the rule (4'd):

$(4^{n}\mathrm{d})\quad\langle[f_{1},\ldots,f_{n}]\circ[f_{1}^{\prime},\ldots,f_{n}^{\prime}],s\rangle\ \mapsto\ \left\{\begin{array}{ll}\langle i,s\rangle&\mbox{if all$f_{1}^{\prime}$,$\ldots$,$f_{n}^{\prime}$are Boolean}\\ &\mbox{contexts,where$i$is a number}\\ &\mbox{with the binary representation}\\ \langle[f_{1}^{\prime\prime},\ldots,f_{n}^{\prime\prime}],s\rangle&\mbox{otherwise}\end{array}\right.$  $\langle[f_{1}^{\prime\prime},\ldots,f_{n}^{\prime\prime}],s\rangle$  $\langle[f_{1}^{\prime\prime},\ldots,f_{n}^{\prime\prime}],s\rangle$  $\langle[f_{1}^{\prime\prime},\ldots,f_{n}^{\prime\prime}],s\rangle$  \(\langle[f_{1}^{\prime\prime},\ldots,f_{n}^{\prime\prime}],s\rangle\
While the rule (5) from above is kept unchanged for the ursa **language, the rule (6) is**
split into two rules, one for ground argument and one for symbolic argument:

* $\langle e_{1},s\rangle\ \mapsto\ \langle e_{1}^{\prime},s^{\prime}\rangle$ $\langle e_{1}\circ e_{2},s\rangle\ \mapsto\ \langle e_{1}^{\prime}\circ e_{2},s^{\prime}\rangle$ * $\langle e_{2},s\rangle\ \mapsto\ \langle e_{2}^{\prime},s^{\prime}\rangle$ $\langle i\circ e_{2},s\rangle\ \mapsto\ \langle i\circ e_{2}^{\prime},s^{\prime}\rangle$ * $\langle e_{2},s\rangle\ \mapsto\ \langle e_{2}^{\prime},s^{\prime}\rangle$ * $\langle[f_{1},\ldots,f_{n}]\circ e_{2},s\rangle\ \mapsto\ \langle[f_{1},\ldots,f_{n}]\circ e_{2}^{\prime},s^{\prime}\rangle$  The $\langle e_{1},s\rangle\ \mapsto\ \langle e_{1}^{\prime},s^{\prime}\rangle$ 
The semantics of **while** is defined by the following standard rules:  $$\begin{array}{ll}\langle b,s\rangle&\mapsto&\langle\top,s^{\prime}\rangle\\ \hline\mbox{\bf while$b$do$c,s$}&\mapsto&\langle c;\mbox{\bf while$b$do$c,s^{\prime}$}\rangle\\ \langle b,s\rangle&\mapsto&\langle\bot,s^{\prime}\rangle\\ \hline\mbox{\bf while$b$do$c,s$}&\mapsto&\langle skip,s^{\prime}\rangle\\ \end{array}$$
If, for the statement while b do c, neither of hb, si 7→ ⊤ and hb, si 7→ ⊥ **holds**
(i.e., if b **is evaluated to a propositional formulae), then a run-time error is raised. The**
semantics of for **is defined by analogy. This is a restriction of the specification language**
and it is difficult to overcome, as it would require indefinite loop unrolling. Recursion is also not supported and an index for accessing an array element has to be a ground number.

A condition for the if **statement has to evaluate to a ground Boolean value, too (otherwise** a run-time error is raised). However, as a substitute, there **is a conditional statement** ite (for if-then-else**) and its condition (the first argument) can be either ground or symbolic.**
Its semantics, if the last two arguments are of the Boolean type, is defined in the following way (if the arguments are of the numerical type, it is defined for each vector element by analogy):
hite(b, [b1], [b2], si 7→ h(b ⇒ b1) ∧ (¬b ⇒ b2), si Arguments to procedures are passed by name if they are variables, and otherwise, they are passed by value.

The semantics of other commands in the ursa **language and its relationship with the**
standard semantics is obvious or analogous to the semantics **of the commands given above.**
The above, clear and relatively simple semantics, enable a rather straightforward (although still tedious) verification (of correctness) of the proposed system: if the system returns a solution, then this solution indeed meets the given specification, and - if the system does not return a solution, then the specification has **no solutions. The correctness**
property is given by the following theorem (s∅ denotes a function not defined for any argument and 7→ **correspond both to the standard and the** ursa **semantics since there are no**
unknowns in the relevant specification).