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
28
29

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

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

  prop = (f >= 0 and f <= 1.);

  guarantee g1: (true -> pre prop) and prop;
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