test-synthesis-1.ucl

/** This is an example to test UCLID5's invariant synthesis.
  */

module main
{
  synthesis function h(x : integer, y : integer) : boolean;
  var x, y : integer;
  
  init {
    x = 0;
    y = 1;
  }
  
  next {
    x' = x + 1;
    y' = x + y;
  }
  
  invariant always_positive: (y >= 0) && h(x, y);
  
  control {
    induction;
    check;
    print_results;
  }
}