Revision 2d37a1e1
Added by Pierre-Loïc Garoche over 6 years ago
| regression_tests/lustre_files/success/kind_fmcad08/simulation/car_5_e7_244_e2_693.lus | ||
|---|---|---|
| 26 | 26 |
stop = time >= 4; |
| 27 | 27 |
bump = dist = 10; |
| 28 | 28 |
tel |
| 29 |
--@ ensures OK; |
|
| 30 | 29 |
node top(m, s : bool) returns (OK : bool); |
| 30 |
--@ contract guarantees OK; |
|
| 31 | 31 |
var toofast, stop, bump: bool; |
| 32 | 32 |
dist, speed, time: int; |
| 33 | 33 |
move: bool; second, meter: bool; |
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)