Project

General

Profile

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

    
(13-13/25)