Project

General

Profile

« Previous | Next » 

Revision 2d37a1e1

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

Renaminig lustre contracts from ensures to guarantees
Will require the latest cocospec branch to compile (before it is integrated in the unstable/master branches)

View differences:

regression_tests/lustre_files/success/kind_fmcad08/misc/_6counter2.lus
1 1
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
2 2
-- invalid property is that it should never reach 5 or 7
3 3

  
4
--@ ensures OK;
5 4
node top (x:bool) returns (OK:bool);
5
--@ contract guarantees OK;
6 6
var a,b,c:bool;
7 7
let
8 8
  a = false -> not pre(a);

Also available in: Unified diff