Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (5.61 KB)

1 6a93d814 xthirioux
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);