Project

General

Profile

Download (414 Bytes) Statistics
| Branch: | Tag: | Revision:
1
node sub (in: int) returns (out: int);
2
--@mode contract_sub ;
3
--@require in > 0 ;
4
--@ensure out >= 0 ;
5
let
6
  out = 0 -> in + pre out ;
7
  -- Does not hold
8
  --%PROPERTY out >= 0 ;
9
tel
10

    
11
node top (in: int; clk: bool) returns (out: int);
12
--@mode contract_top ;
13
--@require in >= 0 ;
14
--@ensure true -> out >= 0 ;
15
var mem: int ;
16
let
17
  mem = 1 -> in + pre mem ;
18
  out = sub(mem) ;
19
  --%PROPERTY true -> out > pre out ;
20
tel
(6-6/6)