Revision 2d37a1e1
Added by Pierre-Loïc Garoche over 6 years ago
| regression_tests/lustre_files/success/kind_fmcad08/misc/ex3_e8_381.lus | ||
|---|---|---|
| 19 | 19 |
late = false -> if pre late then (diff < 0) |
| 20 | 20 |
else (diff <= -10); |
| 21 | 21 |
tel |
| 22 |
--@ ensures OK; |
|
| 23 | 22 |
node top(beacon,second:bool) returns (OK:bool); |
| 23 |
--@ contract guarantees OK; |
|
| 24 | 24 |
var late,early: bool; |
| 25 | 25 |
let |
| 26 | 26 |
(late,early) = speed(beacon,second); |
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)