Syntax and informal semantics Contents

## Syntax and informal semantics

### Program.

 ::= * definition of procedures [var ;] local variables of the main procedure begin + end body of the main procedure
 ::= proc id ( ) returns ( ) signature, with names of input and output formal parameters [var ;] (other) local variables begin + end body

A procedure definition first declares a list of formal input parameters, then a list of formal output parameters (which are local variables that defines the tuple of returned values), then a list of local variables, and then a body. A procedure ends with its last statement.

 ::= eps  | id : (, id : )* ::= int  | real

Variables are either of integer type, or of real type. Real variables can behave as floating-point variables by modifying the exact semantics of arithmetic operations (see below).

### Instructions.

 ::= skip ; | halt ; | fail ; | assume ; | id = random ; | id = ; | id = id ( ) ; | ( ) = id ( ) ; | if then + [else + ] endif ; | while do + done ; ::= eps  | id (, id)*

The skip operation does nothing. The halt operation halts the program execution. The fail has exactly the same operational semantics, but, in addition, indicates a final control point for backward analysis (see below). The assume expr instruction is equivalent to if expr then skip; else halt; . It may be used to abstract non-deterministic assignements. For instance, the non-deterministic assignement of a value between 0 and 2 to a variable x can be written as

```
x = random;
assume x>=0 and x<=2;
```

A call to a procedure with a single return value can be written either as x = P(...) or (x)=P(...). A call to a procedure with multiple return values is written as (x,y) = P(a,b). Input parameters are passed by value. Formal input parameters in a procedure are assumed immutable. Conditional and iteration constructions have the usual semantics.

### Expressions.

#### Boolean expressions.

 ::= true  | false  | brandom | | not  |  or  |  and | ( ) ::= (== | >= | > | <= | <)

Atoms of Boolean expressions are Boolean constants, the unknown value denoted by brandom, and constraints over numerical variables.

#### Numerical expressions.

 ::=  | random | id |  |  | ( ) ::= (+|-|*|/|%)[_(i|f|d|l|q)[,(n|0|+oo|-oo|?)]] ::= - | (cast|sqrt)[_(i|f|d|l|q)[,(n|0|+oo|-oo|?)]] ::=  |  ::= C/OCaml floating-point number syntax ::=  | /

The syntax of numerical expressions is the same as the one used in the APRON interactive toplevel (in OCaml language). The priorities between (Boolean and arithmetic) operators is { *,/ } > { +,- } > { <, <=, =, >=,> } > { not } > { and } > { or } By default, numerical expressions are evaluated using exact arithmetic on real numbers (even if some involved variables are integer), and when assigned to a variable, filtered by the variable domain (when it is integers). For instance, the assignement

```
x = 3/4;
```

is equivalent to the halt instruction if x is declared as integer, because the rational 3/4 is not an integer value. The problem here is that the instruction is not well-typed (even if this is not checked). If one want to emulate the semantics of the integer division operation, with rounding to zero, one should write

```
x = 3 /_i,0 4;
```

Indeed, most arithmetic operators have optional qualifiers that allows to modify their semantics. The first qualifier indicates a numerical type, the second one the rounding mode.

• By default, operations have an exact arithmetic semantics in the real numbers (even if involved variables are of integer). The type qualifiers modify this default semantics. Their meaning is as follows:

 i integer semantics f IEEE754 32 bits floating-point semantics d IEEE754 64 bits floating-point semantics l IEEE754 80 bits extended floating-point semantics q IEEE754 128 bits floating-point semantics

• By default, the rounding mode is "any" (this applies only in non-real semantics), which allows to emulate all the following rounding modes:

 n nearest 0 towards zero +oo towards infinity -oo towards minus infinity ? emulates any rounding mode

#### Examples of numerical expressions.

We illustrate the syntax and (approximated) semantics of numerival expressions with the following program, annotated by Interproc using the command

```  interproc.opt -domain polka -colorize false examples/numerical.spl
```
```
proc integer () returns () var a : int, b : int, c : int;
begin
/* (L5 C5) top */
a = 5; /* (L6 C8) [|a-5=0|] */
b = 2; /* (L7 C8) [|b-2=0; a-5=0|] */
if brandom then
/* (L8 C17) [|b-2=0; a-5=0|] */
c = a / b; /* (L9 C14) bottom */
else
/* (L10 C6) [|b-2=0; a-5=0|] */
c = a /_i,? b; /* (L11 C16) [|b-2=0; a-5=0; -c+3>=0; c-2>=0|] */
c = a /_i,0 b; /* (L12 C18) [|c-2=0; b-2=0; a-5=0|] */
c = a /_i,-oo b; /* (L13 C20) [|c-2=0; b-2=0; a-5=0|] */
c = a /_i,+oo b; /* (L14 C20) [|c-3=0; b-2=0; a-5=0|] */
c = a /_i,n b; /* (L15 C18) [|b-2=0; a-5=0; -c+3>=0; c-2>=0|] */
c = a %_i,? b; /* (L16 C16) [|c-1=0; b-2=0; a-5=0|] */
endif; /* (L17 C8) [|c-1=0; b-2=0; a-5=0|] */
end

proc exact () returns (z : real) var x : real, y : real;
begin
/* (L22 C5) top */
x = 5; /* (L23 C8) [|x-5=0|] */
y = 2; /* (L24 C8) [|y-2=0; x-5=0|] */
z = x / y; /* (L25 C10) [|2z-5=0; y-2=0; x-5=0|] */
y = 0.1; /* (L26 C10)
[|2z-5=0; 36028797018963968y-3602879701896397=0; x-5=0|] */
z = x + y; /* (L27 C10)
[|36028797018963968z-183746864796716237=0;
36028797018963968y-3602879701896397=0; x-5=0|] */
z = z - y; /* (L28 C10)
[|z-5=0; 36028797018963968y-3602879701896397=0; x-5=0|] */
end

proc floating () returns (z : real) var x : real, y : real;
begin
/* (L33 C5) top */
x = 5; /* (L34 C8) [|x-5=0|] */
y = 2; /* (L35 C8) [|y-2=0; x-5=0|] */
z = x /_f,? y; /* (L36 C13)
[|y-2=0; x-5=0;
-713623846352979940529142984724747568191373312z
+1784059828558929176909397126420998565333565441>=0;
713623846352979940529142984724747568191373312z
-1784059403205970525736317797202739275623301119>=0|] */
y = 0.1; /* (L37 C10)
[|36028797018963968y-3602879701896397=0; x-5=0;
-713623846352979940529142984724747568191373312z
+1784059828558929176909397126420998565333565441>=0;
713623846352979940529142984724747568191373312z
-1784059403205970525736317797202739275623301119>=0|] */
z = x +_f,? y; /* (L38 C14)
[|36028797018963968y-3602879701896397=0; x-5=0;
-713623846352979940529142984724747568191373312z
+3639482050260215524856578735848702239922192385>=0;
713623846352979940529142984724747568191373312z
-3639481182540179876463495959770156714984210431>=0|] */
z = z -_f,? y; /* (L39 C14)
[|36028797018963968y-3602879701896397=0; x-5=0;
-5986310706507378352962293074805895248510699696029696z
+29931560882862943060522688904967984086376852368654337>=0;
5986310706507378352962293074805895248510699696029696z
-29931546182211708189135890236173744477275669529624577>=0|] */
end

var z : real
begin
/* (L43 C5) top */
() = integer(); /* (L44 C17) top */
z = exact(); /* (L45 C14) [z-5=0|] */
z = floating(); /* (L46 C17)
[|-5986310706507378352962293074805895248510699696029696z
+29931560882862943060522688904967984086376852368654337>=0;
5986310706507378352962293074805895248510699696029696z
-29931546182211708189135890236173744477275669529624577>=0|] */
end
```

 Syntax and informal semantics Contents