Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (927 Bytes)

1

    
2
/*@ axiomatic Stream {
3

4
  @ type bstream;
5

6
  @ logic bstream tick (boolean b, bstream s);
7

8
  @ logic boolean head (bstream s);
9

10
  @ logic bstream tail (bstream s);
11

12
  @ axiom head_obs: \forall boolean b; \forall bstream s; head (tick (b, s)) == b;
13

14
  @ axiom tail_obs: \forall boolean b; \forall bstream s; tail (tick (b, s)) == s;
15

16
  @ axiom tick_obs: \forall bstream s; s == tick (head (s), tail(s));
17

18
  @ logic bstream bnot (bstream b);
19

20
  @ axiom bnot_def: \forall boolean b; \forall bstream s;
21
                    bnot (tick (b, s)) == tick ((b)?(\false):(\true), bnot (s));
22

23
  @ logic boolean nth (integer i, bstream s) =
24
      (i==0)?(head(s)):(nth(i-1, tail(s)));
25

26
  @ predicate eq (bstream s1, bstream s2) = \forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2);
27

28
  @ axiom eq_obs: \forall bstream s1; \forall bstream s2; eq (s1, s2) ==> (s1 == s2);
29

30
@ lemma prout: \forall bstream s; bnot (bnot (s)) == s;
31

32
}
33
*/
34