### Profile

Statistics
| Branch: | Tag: | Revision:

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

1 2 3 6a93d814 xthirioux ```/*@ axiomatic Stream { ``` ``` ``` ``` @ type stream = Tick(A, stream); ``` ``` ``` ``` @ logic A nth (integer i, stream s); ``` ``` ``` ``` @ axiom nth_0: \forall A v; \forall stream ss; nth(0, Tick(v, ss)) == v; ``` ``` ``` ``` @ axiom nth_S : \forall integer i; i > 0 ==> \forall A v; \forall stream ss; nth(i, Tick(v, ss)) == nth(i-1, ss); ``` ``` ``` ``` @ logic stream lift0 (A c) = Tick (c, lift0 (c)); ``` ``` ``` ``` @ logic stream _arrow = Tick (\true, lift0 (\false)); ``` ``` ``` ``` @ logic stream ite (stream s_if, stream s_then, stream s_else); ``` ``` ``` ``` @ axiom ite_def: \forall boolean v_if; \forall stream ss_if; ``` ``` \forall A v_then; \forall stream ss_then; ``` ``` \forall A v_else; \forall stream ss_else; ``` ``` ite(Tick(v_if, ss_if), Tick(v_then, ss_then), Tick(v_else, ss_else)) == ``` ``` Tick((v_if)?(v_then):(v_else), ite(ss_if, ss_then, ss_else)); ``` ``` ``` ``` ``` ``` @ logic stream pre (stream s); ``` ``` ``` ``` @ axiom pre_def: \forall integer i; \forall stream s; ``` ``` i >= 0 ==> nth(1+i, pre (s)) == nth(i, s); ``` ``` ``` ``` @ logic stream when (stream s_clock, stream s_sample); ``` ``` ``` ``` @ axiom when_def: \forall integer i; \forall stream c; \forall stream s; ``` ``` i >= 0 ==> nth (i, c) == \true ==> nth (i, when (c, s)) == nth (i, s); ``` ``` ``` ``` //Boolean operators ``` ``` ``` ``` @ logic stream bnot (stream b); ``` ``` ``` ``` @ axiom bnot_def: \forall boolean b; \forall stream s; ``` ``` bnot (Tick (b, s)) == Tick (!b, bnot (s)); ``` ``` ``` ``` @ logic stream band (stream b1, stream b2); ``` ``` ``` ``` @ axiom band_def: \forall boolean b1; \forall stream s1; \forall boolean b2; \forall stream s2; ``` ``` band (Tick (b1, s1), Tick (b2, s2)) == Tick (b1 && b2, band (s1, s2)); ``` ``` ``` ``` @ logic stream bor (stream b1, stream b2); ``` ``` ``` ``` @ axiom bor_def: \forall boolean b1; \forall stream s1; \forall boolean b2; \forall stream s2; ``` ``` bor (Tick (b1, s1), Tick (b2, s2)) == Tick (b1 || b2, bor (s1, s2)); ``` ``` ``` ``` //Relational operators ``` ``` ``` ``` @ logic stream eq (stream s1, stream s2); ``` ``` ``` ``` @ axiom eq_def: \forall A v1; \forall stream s1; \forall A v2; \forall stream s2; ``` ``` eq (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 == v2, eq (s1, s2)); ``` ``` ``` ``` ``` ``` @ logic stream inf (stream s1, stream s2); ``` ``` ``` ``` @ axiom inf_def: \forall real v1; \forall stream s1; \forall real v2; \forall stream s2; ``` ``` inf (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 < v2, inf (s1, s2)); ``` ``` ``` ``` @ logic stream infeq (stream s1, stream s2) = bor (eq (s1, s2), inf(s1, s2)); ``` ``` ``` ``` ``` ``` //Real operators: ``` ``` ``` ``` @ logic stream plus (stream s1, stream s2); ``` ``` ``` ``` @ axiom plus_def: \forall real v1; \forall stream s1; \forall real v2; \forall stream s2; ``` ``` plus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 + v2, plus (s1, s2)); ``` ``` ``` ``` @ logic stream minus (stream s1, stream s2); ``` ``` ``` ``` @ axiom minus_def: \forall real v1; \forall stream s1; \forall real v2; \forall stream s2; ``` ``` minus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 - v2, minus (s1, s2)); ``` ``` ``` ``` @ logic stream mult (stream s1, stream s2); ``` ``` ``` ``` @ axiom mult_def: \forall real v1; \forall stream s1; \forall real v2; \forall stream s2; ``` ``` mult (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 * v2, mult (s1, s2)); ``` ``` ``` ``` @ logic stream div (stream s1, stream s2); ``` ``` ``` ``` //Integer operators: ``` ``` ``` ``` @ logic stream iplus (stream s1, stream s2); ``` ``` ``` ``` @ axiom iplus_def: \forall integer v1; \forall stream s1; \forall integer v2; \forall stream s2; ``` ``` iplus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 + v2, iplus (s1, s2)); ``` ``` ``` ``` @ logic stream iminus (stream s1, stream s2); ``` ``` ``` ``` @ axiom iminus_def: \forall integer v1; \forall stream s1; \forall integer v2; \forall stream s2; ``` ``` iminus (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 - v2, iminus (s1, s2)); ``` ``` ``` ``` @ logic stream imult (stream s1, stream s2); ``` ``` ``` ``` @ axiom imult_def: \forall integer v1; \forall stream s1; \forall integer v2; \forall stream s2; ``` ``` imult (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 * v2, imult (s1, s2)); ``` ``` ``` ``` @ logic stream idiv (stream s1, stream s2); ``` ``` ``` ``` @ axiom idiv_def: \forall integer v1; \forall stream s1; \forall integer v2; \forall stream s2; ``` ``` idiv (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 / v2, idiv (s1, s2)); ``` ``` ``` ``` @ logic stream imod (stream s1, stream s2); ``` ``` ``` ``` @ axiom imod_def: \forall integer v1; \forall stream s1; \forall integer v2; \forall stream s2; ``` ``` imod (Tick (v1, s1), Tick (v2, s2)) == Tick (v1 % v2, imod (s1, s2)); ``` ``` ``` ```@ lemma prout: \forall stream s; bnot (bnot (s)) == s; ``` ``` ``` ```@ lemma eq_obs_int: \forall stream s1; \forall stream s2; ``` ``` (\forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2)) <==> (s1 == s2); ``` ```} ``` ```*/ ``` ```// logic stream apply1_int (stream arg, int func(int )); ``` ```// axiom apply1_int_def: \forall int v; \forall stream ss; \forall int func(int); ``` ```// apply1_int (Tick (v, ss), func) == Tick (func(v), apply1_int (ss, func)); ``` ```// lemma eq_obs: \forall stream s1; \forall stream s2; ``` `// (\forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2)) <==> (s1 == s2);`