### Profile

 1 ```node Sofar( X : bool ) returns ( Sofar : bool ); ``` ```let ``` ``` Sofar = X -> X and pre Sofar; ``` ```tel ``` ```--const N=3; ``` ```node controleur(nB,nS:int) returns (diff:int; avance,retard:bool); ``` ```let ``` ``` diff = nB-nS; ``` ``` avance = false -> ``` ``` if not (pre avance) then diff >= 10 else diff > 0; ``` ``` retard = false -> ``` ``` if not (pre retard) then (diff <= -10) else (diff < 0); ``` ```tel ``` ```node hypothese(B,S,avance,retard:bool) returns (ok:bool); ``` ```var c:int; ``` ```let ``` ``` ok = true -> ``` ``` (if pre retard then not S else true) and ``` ``` (if pre c >= 9 then not B else true); ``` ``` c = 0 -> ``` ``` if pre avance and avance then ``` ``` if B then pre c + 1 else pre c ``` ``` else ``` ``` 0; ``` ```tel ``` ```node main(B0, B1 : bool; S : bool) ``` ```returns ( ast: bool; nB0, nB1 : int; nS : int; ``` ``` diff0, diff1:int; ``` ``` avance0, avance1, retard0, retard1 : bool ); ``` ```var H0, H1:bool; ``` ```let ``` ``` nB0 = 0 -> if B0 then pre nB0 + 1 else pre nB0; ``` ``` nB1 = 0 -> if B1 then pre nB1 + 1 else pre nB1; ``` ``` nS = 0 -> if S then pre nS + 1 else pre nS; ``` ``` H0 = hypothese(B0,S,avance0,retard0); ``` ``` H1 = hypothese(B1,S,avance1,retard1); ``` ``` (diff0,avance0,retard0) = controleur(nB0,nS); ``` ``` (diff1,avance1,retard1) = controleur(nB1,nS); ``` ``` ast = H0 and H1; ``` ```tel ``` ```-- Not provable? ``` ```node top(B0, B1 : bool; S : bool) ``` ```returns (OK:bool); ``` ```--@ contract guarantees OK; ``` ```var nB0, nB1 : int; ``` ``` nS : int; ``` ``` diff0,diff1:int; ``` ``` avance0,avance1,retard0,retard1 : bool; ``` ``` ast:bool; ``` ```let ``` ``` (ast,nB0,nB1,nS,diff0,diff1,avance0,avance1,retard0,retard1) = main(B0,B1,S); ``` ``` OK = true -> Sofar( ast ) => -10 <= pre diff0 and pre(diff0) <= 20; ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` ```tel ```