tests/source/rfollow.scade


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

node follow(a: real) returns (probe f: real)
var
  probe pf: real;
let
  assume h1: a >= 0. and a <= 1.;
  guarantee g1: f >= 0. and f <= 1.;
  guarantee g2: pf >= 0. and pf <= 1.;

  pf = 0. -> pre f;
  f = (pf + a) / 2.0;

tel


node test(i: int) returns (a, b, c: int; exit: bool)
var
  probe u, v: real;
let
  u = real(i mod 10) / 10.;
  v = follow(u);
  a = int(u * 1000.);
  b = int(v * 1000.);
  c = 0;
  exit = (i > 100);
tel