Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / misc / durationThm_1.lus @ 2d37a1e1

1 2 3 b8dc00eb bourbouh ```-- ``` ```-- Source: Bertrand Jeannet ``` ```-- ``` ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```node Age (p: bool) returns (age_of_p: int); ``` ```-- how long has p been maintained true in the strict past ``` ```let ``` ``` age_of_p = 0 -> if pre(p) then pre(age_of_p) + 1 else 0; ``` ```tel ``` ```-- Theorem 1: ``` ```-- (p -k-> q and q -m-> r) => p -k+m-> r ``` ```-- Not provable in luke-* ``` ```node top (ik, im: int; p, q, r : bool) returns (OK: bool); ``` 2d37a1e1 ploc ```--@ contract guarantees OK; ``` b8dc00eb bourbouh ```var k,m : int; ``` ``` env : bool; ``` ```let ``` ``` k = ik -> pre k; ``` ``` m = im -> pre m; ``` ``` env = Sofar((k>=1 and m>=1) and (Age(p)>=k => q) and (Age(q)>=m => r)); ``` ``` OK = env => (true -> ( (Age(p)>=k+m) => r )); ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` `tel`