Project

General

Profile

Download (295 Bytes) Statistics
| Branch: | Tag: | Revision:
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

    
(9-9/25)