Project

General

Profile

« Previous | Next » 

Revision 5dfe059d

Added by Pierre-Loïc Garoche over 6 years ago

Cocospec

View differences:

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