Project

General

Profile

« Previous | Next » 

Revision 2a5c9911

Added by Pierre-Loïc Garoche about 2 years ago

array example with spec

View differences:

tests/cocospec/arrays.lus
1
(*@ contract NLGuidanceSpec (Vt, Vv, Xtarg,   Xv:real^3; r:real; ) returns (r1: real; );
2
let
3
var P1 : bool = 0.0 = Vt[0];
4
guarantee "NLG-007" P1;
5
tel
6
*)
7

  
8
node mynode (Vt, Vv, Xtarg,   Xv:real^3; r:real; ) returns (r1: real; );
9
var P0, P1: bool;
10
let
11
 P0 = [0.1, 0.2] = [0.1, 0.3]; -- Bug: it looks like the output C doesn't check the equality btw values but pointers!
12
 P1 = 0.0 = Vt[0];
13
 r1 = if P1 && P0 then 1.0 else 0.0;
14
tel

Also available in: Unified diff