# Documentation

## How Polyspace Evaluates Function and Procedure Parameters

Polyspace® applies by-copy semantics and a left-to-right evaluation order for parameter passing. You can use Polyspace to verify your Ada code provided your compiler implements:

• Left-to-right evaluation for subprogram parameters. Consider the following code.

```1 with ada.integer_text_io; 2 use ada.integer_text_io; 3 procedure test1 is 4 x,y,z,r : integer; 5 6 function f (x : integer) return integer 7 is 8 begin 9 z := 0; 10 return x + 1; 11 end f; 12 begin 13 x := 10; 14 y := 20; 15 z := 10; 16 R := y / Z + F(x); 17 pragma assert(R = 13); -- green ASRT 18 put(R); 19 end;```
In this example, Polyspace verification implements left-to-right evaluation and generates a green ASRT check.

• By-copy semantics for subprogram parameters. Consider the following code.

```1 procedure Test2 2 is 3 4 type Rec is 5 record 6 F,G: Integer; 7 end record; 8 9 R: Rec; 10 Result : Integer; 11 12 procedure Multiply (X, Y : in Rec; Z : out Rec) 13 14 is 15 begin 16 z := (0,0); 17 Z.F := X.F * Y.F; 18 Z.G := X.G * Y.G; 19 end Multiply; 20 21 begin 22 R := (10,10); 23 Result := 100; 24 Multiply (R,R,R); 25 Result := Result/R.F; 26 pragma assert (Result = 1); -- green ASRT 27 end Test2; ```
In this example, Polyspace verification implements by-copy semantics and generates a green ASRT check.

The green checks generated indicate that the code conforms to the Ada standard, which states that The execution of a program is erroneous if its effect depends on which mechanism is selected by the implementation. See Formal Parameter Modes.