Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.01 KB)

1 6a93d814 xthirioux
2
//@ type point = real;
3
//@ type triangle = point[3];
4
5
/* axiomatic Stream {
6

7
  @ type prout = boolean[3];
8

9
  @ type bstream = S(prout, integer);
10

11
  @ logic bstream bnot (bstream s) 
12

13
  @ logic boolean head (bstream s) = s[0];
14

15
  @ logic boolean * tail (boolean * s) = s + 1;
16

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

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

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

23
  @ logic bstream bnot (bstream b);
24

25
  @ axiom bnot_def: \forall boolean b; \forall bstream s;
26
                    bnot (tick (b, s)) == tick ((b)?(\false):(\true), bnot (s));
27

28
  @ logic boolean nth (integer i, bstream s) =
29
      (i==0)?(head(s)):(nth(i-1, tail(s)));
30

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

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

35
@ lemma prout: \forall bstream s; bnot (bnot (s)) == s;
36
}
37

38
*/