32 lines
648 B
Plaintext
32 lines
648 B
Plaintext
module main {
|
|
var a, b : integer;
|
|
init {
|
|
a = 0;
|
|
b = 1;
|
|
}
|
|
next {
|
|
a', b' = b, a+b;
|
|
}
|
|
|
|
// Part 2: System specification
|
|
invariant a_le_b: a <= b;
|
|
|
|
// Part 3: Proof script
|
|
control {
|
|
// original uclid was like SRI's sat tool
|
|
//bmc(3); // do bounded model checking for 3 steps
|
|
//induction;
|
|
vobj = induction(1); // do induction for one step
|
|
|
|
check; // call smt solver
|
|
print_results;
|
|
|
|
vobj.print_cex(a, b); // print counterexample on failure
|
|
}
|
|
}
|
|
|
|
// uclid name.ucl
|
|
// uclid name.ucl (failed ∵ invariant not powerful enough)
|
|
|
|
// uclid name.ucl -m Sys // check Sys module instead of main module
|