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