|
| | | Syntax and informal semantics | Contents |
| <program> | ::= | <procedure_def>* | definition of procedures |
| [var <vars_decl> ;] | local variables of the main procedure | ||
| begin <statement>+ end | body of the main procedure |
| <procedure_def> | ::= | proc id ( <vars_decl> ) returns ( <vars_decl> ) | signature, with names of |
| input and output formal parameters | |||
| [var <vars_decl> ;] | (other) local variables | ||
| begin <statement>+ 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.
| <vars_decl> | ::= | eps | id : <type> (, id : <type>)* |
| <type> | ::= | 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).
| <statement> | ::= | skip ; |
| | | halt ; | |
| | | fail ; | |
| | | assume <bexpr> ; | |
| | | id = random ; | |
| | | id = <nexpr> ; | |
| | | id = id ( <var_list> ) ; | |
| | | ( <var_list> ) = id ( <var_list> ) ; | |
| | | if <bexpr> then <statement>+ [else <statement>+ ] endif ; | |
| | | while <bexpr> do <statement>+ done ; | |
| <var_list> | ::= | 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.
| <bexpr> | ::= | true | false | brandom |
| | | <constraint> | |
| | | not <bexpr> | <bexpr> or <bexpr> | <bexpr> and <bexpr> | |
| | | ( <bexpr> ) | |
| <constraint> | ::= | <nexpr> (== | >= | > | <= | <) <nexpr> |
Atoms of Boolean expressions are Boolean constants, the unknown value denoted by brandom, and constraints over numerical variables.
| <nexpr> | ::= | <coeff> | random |
| | | id | |
| | | <unop> <nexpr> | <nexpr> <binop> <nexpr> | |
| | | ( <nexpr> ) | |
| <binop> | ::= | (+|-|*|/|%)[_(i|f|d|l|q)[,(n|0|+oo|-oo|?)]] |
| <unop> | ::= | - |
| | | (cast|sqrt)[_(i|f|d|l|q)[,(n|0|+oo|-oo|?)]] | |
| <coeff> | ::= | <float> | <rational> |
| <float> | ::= | C/OCaml floating-point number syntax |
| <rational> | ::= | <integer> | <integer>/<integer> |
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.
| 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 |
| n | nearest |
| 0 | towards zero |
| +oo | towards infinity |
| -oo | towards minus infinity |
| ? | emulates any rounding mode |
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 |