### Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (1.01 KB)

1 2 3 6a93d814 xthirioux ```//@ type point = real; ``` ```//@ type triangle = point[3]; ``` ```/* axiomatic Stream { ``` ``` ``` ``` @ type prout = boolean[3]; ``` ``` ``` ``` @ type bstream = S(prout, integer); ``` ``` ``` ``` @ logic bstream bnot (bstream s) ``` ``` ``` ``` @ logic boolean head (bstream s) = s[0]; ``` ``` ``` ``` @ logic boolean * tail (boolean * s) = s + 1; ``` ``` ``` ``` @ axiom head_obs: \forall boolean b; \forall bstream s; head (tick (b, s)) == b; ``` ``` ``` ``` @ axiom tail_obs: \forall boolean b; \forall bstream s; tail (tick (b, s)) == s; ``` ``` ``` ``` @ axiom tick_obs: \forall bstream s; s == tick (head (s), tail(s)); ``` ``` ``` ``` @ logic bstream bnot (bstream b); ``` ``` ``` ``` @ axiom bnot_def: \forall boolean b; \forall bstream s; ``` ``` bnot (tick (b, s)) == tick ((b)?(\false):(\true), bnot (s)); ``` ``` ``` ``` @ logic boolean nth (integer i, bstream s) = ``` ``` (i==0)?(head(s)):(nth(i-1, tail(s))); ``` ``` ``` ``` @ predicate eq (bstream s1, bstream s2) = \forall integer i; i >= 0 ==> nth (i, s1) == nth (i, s2); ``` ``` ``` ``` @ axiom eq_obs: \forall bstream s1; \forall bstream s2; eq (s1, s2) ==> (s1 == s2); ``` ``` ``` ```@ lemma prout: \forall bstream s; bnot (bnot (s)) == s; ``` ```} ``` ``` ``` ```*/ ```