Project

General

Profile

« Previous | Next » 

Revision 2d37a1e1

Added by Pierre-Loïc Garoche over 6 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/simulation/metros_1.lus
44 44 
  ast = H0 and H1;
45 45 
tel
46 46 

  		




  47
  
  
    
--@ ensures OK;


  		




  48
  47
  
    
node top(B0, B1 : bool; S : bool) 


  		




  49
  48
  
    
returns (OK:bool);


  		




  
  49
  
    
--@ contract guarantees OK;


  		




  50
  50
  
    
var nB0, nB1 : int;


  		




  51
  51
  
    
    nS : int;


  		




  52
  52
  
    
    diff0, diff1 :int;


  		












Also available in:  Unified diff