Revision 2d37a1e1
Added by Pierre-Loïc Garoche over 6 years ago
| regression_tests/lustre_files/success/kind_fmcad08/misc/durationThm_2_e2_63.lus | ||
|---|---|---|
| 7 | 7 |
let |
| 8 | 8 |
age_of_p = 0 -> if pre(p) then pre(age_of_p) -1+ 1 else 0; |
| 9 | 9 |
tel |
| 10 |
--@ ensures OK; |
|
| 11 | 10 |
node top (k0: int; p, q, r, t : bool) returns (OK: bool); |
| 11 |
--@ contract guarantees OK; |
|
| 12 | 12 |
var k: int; |
| 13 | 13 |
env : bool; |
| 14 | 14 |
let |
Also available in: Unified diff
Renaminig lustre contracts from ensures to guarantees
Will require the latest cocospec branch to compile (before it is integrated in the unstable/master branches)