Project

General

Profile

« Previous | Next » 

Revision 3e36d4e0

Added by Pierre-Loïc Garoche almost 8 years ago

Added default ensures statements

View differences:

test/src/kind_fmcad08/misc/_6counter.lus
1 1
-- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
2 2
-- property is that it should never reach 6 or 7
3 3

  
4
--@ ensures OK;
4 5
node top (x:bool) returns (OK:bool);
5 6
var a,b,c:bool;
6 7
let

Also available in: Unified diff