
## 4. Syntax Of Ursa Language

In this section we describe the language ursa **that serves as a specification language in the** spirit of the approach presented above. A description of the **syntax of the** ursa **language**
is given, in ebnf representation, in Table 1 (hnum vari **denotes the syntactical class of** numerical variables, hnum expri denotes the syntactical class of numerical expressions, h**bool**
expri **denotes the syntactical class of Boolean expressions, etc). An** ursa **program is a** sequence of statements (and procedure definitions). There are two types of variables —
numerical, with identifiers starting with n and Boolean, with identifiers starting with b**. The**
same convention holds for identifiers of arrays. Variables are not declared, but introduced dynamically. There are functions (bool2num and num2bool**) for converting Boolean values**
to numerical values and vice versa, and the sgn **function corresponding to signum function.** Arithmetic, bitwise, relational and compound assignment operators, applied over arithmetic variables/expressions, are written in the C-style. For example, bitwise conjunction over numerical variables n1 and n2 **is written** n1 & n2, bitwise left shift of n1 for n2 **is written** n1 << n2**, and** n1 += n2 **is equivalent to** n1 = n1+n2**. Logical operators, applied over** Boolean variables/expressions, are written in the C-style, with additional operator ^^ for logical exclusive disjunction, in the spirit of other C logical operators. There are also compound assignment operators for logical operators, such as &&= **(added for symmetry** and convenience, although they do not exist in C). The operator ite **is the conditional**
operator: ite(b,n1,n2) equals n1 if b is true, and equals n2 **otherwise. There are no**
user-defined functions, but only user-defined procedures.

The role of the command assert **is to assert that some constraint (given as the argument) is met (as in C). During the interpretation of the** ursa **program, this command**
invokes the solving mechanism and seeks for an assignment to **the introduced unknowns**
that make this constraint true. The command assert all **is analogous, but it seeks for all**
satisfying models. One program can have several commands of **this sort, but each of them** works locally (as in C), i.e., it invokes the solving mechanism just for its own argument.

The instructions minimize **(and** maximize**) state that a minimal (or maximal) value within** the given range for the given numerical variable should be found. The commands assert and assert all **take into account only the last** minimize/maximize **instruction.**
There are miscellaneous commands, mostly intended to be used in interactive mode (for listing values and status of variables - listvars**, for deleting values of all current variables**
- clear**, and stopping the interpreter —** halt).

The following two examples illustrate some constructs of the specification language —
the use of procedures and the use of the operator maximize.

Example 4.1. For a given value k, the task is to find all values x, y, and z **such that**
x k + y k ≡ z k(mod 2n**). The following** ursa **code (with a procedure that computes the**
power function) specifies the problem for k **= 2:**
procedure power(na,nk) {
np=na; for(ni=1;ni<nk;ni=ni+1)
na = na*np;
}