Project

General

Profile

« Previous | Next » 

Revision c3af3032

Added by Bourbouh over 3 years ago

add more contracts examples

View differences:

tests/cocospec/StopwatchSpec2.lus
52 52
-- Stopwatch low-level spec --
53 53
------------------------------
54 54

  
55
node stopwatch ( toggle, reset : bool ) returns ( count : int );
56
(*@
55
node stopwatch ( toggle, reset : bool ) returns ( time : int );
56
(*@contract
57 57
  -- the watch is activated initially if the toggle button is pressed
58 58
  -- afterwards, it is activated iff 
59 59
  --   it was activated before and the toggle button is unpressed or
......
73 73
  
74 74
  -- if there is no reset now and there was an even number of counts since the last reset
75 75
  -- then the current elapsed time is the same as the previous one
76
  guarantee not reset and Since(reset, Even(Count(toggle))) 
76
  var even_count:bool = Even(Count(toggle));
77
  guarantee not reset and Since(reset, even_count) 
77 78
            => Stable(time) ;
78 79
  -- if there is no reset now and there was an odd number of counts since the last reset
79 80
  -- then the current elapsed time is greater than previous one
80
  guarantee not reset and Since(reset, not Even(Count(toggle))) 
81
            => Increased(time) ;
81
  guarantee (not reset) and Since(reset, not even_count)  => Increased(time) ;
82 82

  
83 83

  
84 84
--  guarantee true -> not Even(Count(toggle)) and Count(reset) = 0 => time > pre time ;
......
115 115
  var running : bool;
116 116
let
117 117
  running = (false -> pre running) <> toggle ;
118
  count =
118
  time =
119 119
    if reset then 0
120
    else if running then 1 -> pre count + 1
121
    else 0 -> pre count ;
120
    else if running then 1 -> pre time + 1
121
    else 0 -> pre time ;
122 122
tel
123 123

  
124 124

  

Also available in: Unified diff