Revision 5dfe059d
Added by Pierre-Loïc Garoche over 6 years ago
tests/cocospec/refinement.lus | ||
---|---|---|
4 | 4 |
tel |
5 | 5 |
|
6 | 6 |
node sub (in: bool) returns (cpt: int) ; |
7 |
(*@contract |
|
7 |
(*@ --contract
|
|
8 | 8 |
assume true -> in = not pre in ; |
9 | 9 |
mode begin ( |
10 | 10 |
require count(true) <= 10 ; |
... | ... | |
20 | 20 |
tel |
21 | 21 |
|
22 | 22 |
node top (in: bool) returns (cpt: int) ; |
23 |
(*@contract |
|
23 |
(*@ --contract
|
|
24 | 24 |
assume true -> in = not pre in ; |
25 |
guarantee "sub" cpt >= 0 ; |
|
26 |
guarantee "sub" (count(true) > 15) => false ; |
|
25 |
-- guarantees "sub" cpt >= 0 ; |
|
26 |
-- guarantees "sub" (count(true) > 15) => false ; |
|
27 |
guarantees cpt >= 0 ; |
|
28 |
guarantees (count(true) > 15) => false ; |
|
27 | 29 |
*) |
28 | 30 |
let |
29 | 31 |
cpt = sub(in) ; |
Also available in: Unified diff
Cocospec