Project

General

Profile

Download (5.61 KB) Statistics
| Branch: | Tag: | Revision:
1

    
2
/*@ axiomatic Stream {
3

    
4
  @ type stream<A> = Tick(A, stream<A>);
5

    
6
  @ logic A nth<A> (integer i, stream<A> s);
7

    
8
  @ axiom nth_0<A>: \forall A v; \forall stream<A> ss; nth(0, Tick(v, ss)) == v;
9

    
10
  @ axiom nth_S<A> : \forall integer i; i > 0 ==> \forall A v; \forall stream<A> ss; nth(i, Tick(v, ss)) == nth(i-1, ss);
11

    
12
  @ logic stream<A> lift0<A> (A c) = Tick (c, lift0 (c));
13

    
14
  @ logic stream<boolean> _arrow<A> = Tick (\true, lift0 (\false));
15

    
16
  @ logic stream<A> ite<A> (stream<boolean> s_if, stream<A> s_then, stream<A> s_else);
17

    
18
  @ axiom ite_def<A>: \forall boolean v_if; \forall stream<boolean> ss_if;
19
                      \forall A v_then; \forall stream<A> ss_then;
20
                      \forall A v_else; \forall stream<A> ss_else;
21
                      ite(Tick(v_if, ss_if), Tick(v_then, ss_then), Tick(v_else, ss_else)) ==
22
      Tick((v_if)?(v_then):(v_else), ite(ss_if, ss_then, ss_else));
23

    
24

    
25
  @ logic stream<A> pre<A> (stream<A> s);
26

    
27
  @ axiom pre_def<A>: \forall integer i; \forall stream<A> s;
28
                      i >= 0 ==> nth(1+i, pre (s)) == nth(i, s);
29

    
30
  @ logic stream<A> when<A> (stream<boolean> s_clock, stream<A> s_sample);
31

    
32
  @ axiom when_def<A>: \forall integer i; \forall stream<boolean> c; \forall stream<A> s;
33
                       i >= 0 ==> nth (i, c) == \true ==> nth (i, when (c, s)) == nth (i, s);
34

    
35
  //Boolean operators
36

    
37
  @ logic stream<boolean> bnot (stream<boolean> b);
38

    
39
  @ axiom bnot_def: \forall boolean b; \forall stream<boolean> s;
40
                    bnot (Tick (b, s)) == Tick (!b, bnot (s));
41

    
42
  @ logic stream<boolean> band (stream<boolean> b1, stream<boolean> b2);
43

    
44
  @ axiom band_def: \forall boolean b1; \forall stream<boolean> s1; \forall boolean b2; \forall stream<boolean> s2;
45
                    band (Tick (b1, s1), Tick (b2, s2)) == Tick (b1 && b2, band (s1, s2));
46

    
47
  @ logic stream<boolean> bor (stream<boolean> b1, stream<boolean> b2);
48

    
49
  @ axiom bor_def: \forall boolean b1; \forall stream<boolean> s1; \forall boolean b2; \forall stream<boolean> s2;
50
                    bor (Tick (b1, s1), Tick (b2, s2)) == Tick (b1 || b2, bor (s1, s2));
51

    
52
  //Relational operators
53

    
54
  @ logic stream<boolean> eq<A> (stream<A> s1, stream<A> s2);
55

    
56
  @ axiom eq_def<A>: \forall A v1; \forall stream<A> s1; \forall A v2; \forall stream<A> s2;
57
                    eq (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 == v2, eq (s1, s2));
58

    
59

    
60
  @ logic stream<boolean> inf (stream<real> s1, stream<real> s2);
61

    
62
  @ axiom inf_def<A>: \forall real v1; \forall stream<real> s1; \forall real v2; \forall stream<real> s2;
63
                    inf (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 < v2, inf (s1, s2));
64

    
65
  @ logic stream<boolean> infeq (stream<real> s1, stream<real> s2) = bor (eq (s1, s2), inf(s1, s2));
66

    
67

    
68
  //Real operators:
69

    
70
  @ logic stream<real> plus (stream<real> s1, stream<real> s2);
71

    
72
  @ axiom plus_def<A>: \forall real v1; \forall stream<real> s1; \forall real v2; \forall stream<real> s2;
73
                    plus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 + v2, plus (s1, s2));
74

    
75
  @ logic stream<real> minus (stream<real> s1, stream<real> s2);
76

    
77
  @ axiom minus_def<A>: \forall real v1; \forall stream<real> s1; \forall real v2; \forall stream<real> s2;
78
                    minus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 - v2, minus (s1, s2));
79

    
80
  @ logic stream<real> mult (stream<real> s1, stream<real> s2);
81

    
82
  @ axiom mult_def<A>: \forall real v1; \forall stream<real> s1; \forall real v2; \forall stream<real> s2;
83
                    mult (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 * v2, mult (s1, s2));
84

    
85
  @ logic stream<real> div (stream<real> s1, stream<real> s2);
86

    
87
  //Integer operators:
88

    
89
  @ logic stream<integer> iplus (stream<integer> s1, stream<integer> s2);
90

    
91
  @ axiom iplus_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;
92
                    iplus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 + v2, iplus (s1, s2));
93

    
94
  @ logic stream<integer> iminus (stream<integer> s1, stream<integer> s2);
95

    
96
  @ axiom iminus_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;
97
                    iminus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 - v2, iminus (s1, s2));
98

    
99
  @ logic stream<integer> imult (stream<integer> s1, stream<integer> s2);
100

    
101
  @ axiom imult_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;
102
                    imult (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 * v2, imult (s1, s2));
103

    
104
  @ logic stream<integer> idiv (stream<integer> s1, stream<integer> s2);
105

    
106
  @ axiom idiv_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;
107
                    idiv (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 / v2, idiv (s1, s2));
108

    
109
  @ logic stream<integer> imod (stream<integer> s1, stream<integer> s2);
110

    
111
  @ axiom imod_def<A>: \forall integer v1; \forall stream<integer> s1; \forall integer v2; \forall stream<integer> s2;
112
                    imod (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 % v2, imod (s1, s2));
113

    
114
@ lemma prout: \forall stream<boolean> s; bnot (bnot (s)) == s;
115

    
116
@ lemma eq_obs_int: \forall stream<integer> s1; \forall stream<integer> s2;
117
                     (\forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2)) <==> (s1 == s2);
118
}
119
*/
120

    
121
// logic stream<int> apply1_int (stream<int> arg, int func(int ));
122

    
123
// axiom apply1_int_def: \forall int v; \forall stream<int> ss; \forall int func(int);
124
//                        apply1_int (Tick (v, ss), func) == Tick (func(v), apply1_int (ss, func));
125

    
126

    
127
// lemma eq_obs<A>: \forall stream<A> s1; \forall stream<A> s2;
128
//                   (\forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2)) <==> (s1 == s2);
(12-12/25)