Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / oversampling / oversampling0_denot.h @ 6a93d814

History | View | Annotate | Download (295 Bytes)

1
#include "streams_acsl.h"
2

    
3
/*
4
node f(x:int) returns (cpt, y:int )
5
let
6
  y = x + 1;
7
  cpt = (0 fby cpt) + 1;
8
tel
9
*/
10

    
11
/*@ predicate denot_f (stream<integer> x, stream<integer> cpt, stream<integer> y) =
12
         (cpt = ite (_arrow, lift0 (0), pre(cpt)))
13
     &&  (y   = iplus (x, lift0 (1)));
14
 */
15