### Profile

1 2 3 b8dc00eb bourbouh ```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 ``` ```node top(B0, B1 : bool; S : bool) ``` ```returns (OK:bool); ``` 2d37a1e1 ploc ```--@ contract guarantees OK; ``` b8dc00eb bourbouh ```var nB0, nB1 : int; ``` ``` nS : int; ``` ``` diff0, diff1 :int; ``` ``` avance0, avance1, retard0, retard1 : bool; ``` ``` pOK:bool; ``` ``` ast:bool; ``` ```let ``` ``` (ast,nB0,nB1,nS,diff0,diff1,avance0,avance1,retard0,retard1) = main(B0,B1,S); ``` ``` pOK = true -> not (pre avance0 and retard0 or pre retard0 and avance0); ``` ``` OK = Sofar( ast and nB0 < 1 and nB1 < 1 and nS < 1 and diff0 < 32767 ) => (true -> pre pOK); ``` ``` --%PROPERTY OK=true; ``` ``` --%MAIN; ``` ```tel ```