%%% %%% Author: Paul Y Gloess %%% http://dept-info.labri.u-bordeaux.fr/~gloess/ %%% %%% LaBRI, ENSERB & Universite Bordeaux I %%% 351, Cours de la Liberation %%% 33405 Talence Cedex %%% France %%% %%% In B, the while statement must come with two reasons: %%% - a termination reason, specified as a term ranging into nat; %%% - an invariant, some assertion remaining true at each loop step. %%% Here, we base the variant "v" on the same "domain", instead of "nat": %%% - "<" is a "domain" binary well founded relation; %%% - "v", the variant, is a term, that is a function from %%% [environment -> domain]. %%% A well founded relation "R" on "environment" is built from "<" and "v". %%% rivwhile_statement[ environment: TYPE+ ,domain: TYPE+ ]: THEORY BEGIN folfhl: LIBRARY = "../fol" ; IMPORTING riwhile_statement[environment] IMPORTING folfhl@terms[environment, domain] IMPORTING folfhl@lifting[environment, domain, domain] corrdecr?(<: pred[[domain, domain]], variant: term) (a, b: assertion[environment]) (S: program[environment]): bool = correct?(a, S, b) AND (FORALL (d: domain): correct?(a AND equals(variant, lift_(d)) ,S ,lift_(<)(variant, lift_(d)))) ; %% %% Construction of a relation from a term: %% trel(r: pred[[domain, domain]])(t: term)(sigma1, sigma2: environment): bool = r(t(sigma1), t(sigma2)) ; IMPORTING wellfoundedness[domain, environment] trel_wf: LEMMA (FORALL (<: (well_founded?[domain]), t: term): well_founded?[environment](trel(<)(t))) ; correctness_implies_termination: LEMMA (FORALL (<: pred[[domain, domain]], t: term, a: assertion[environment], S: program[environment]): (FORALL (d: domain): correct?(a AND equals(t, lift_(d)), S, lift_(<)(t, lift_(d)))) IMPLIES decreases?(trel(<)(t))(a)(S)) ; variant_corrdecr_implies_corrdecr: LEMMA (FORALL (<: pred[[domain, domain]], variant: term, a, b: assertion[environment], S: (corrdecr?(<, variant)(a, b))): corrdecr?(trel(<)(variant))(a, b)(S)) %% %% Since in practical applications, each while loop will raise a %% TCC for the loop, we want this TCC to look as simple as possible. %% We were previously using: %% "loop: (corrdecr?(<, variant)(invariant AND test, invariant))" %% but then the "invariant" appears twice. Hence the reason for %% introducing "terminates?" and use the type restriction: %% "loop: (terminates?(<, variant, invariant)(test)": %% terminates?(<: (well_founded?[domain]), variant: term, invariant: assertion[environment]) (test: assertion[environment]) (S: program[environment]) % typically the "loop". : bool = corrdecr?(<, variant)(invariant AND test, invariant)(S) ; while(<: (well_founded?[domain]), variant: term, invariant: assertion[environment]) (test: assertion[environment], loop: (terminates?(<, variant, invariant)(test))) : program[environment] = while(trel(<)(variant), invariant) (test, loop) ; while_hoare_rule: LEMMA %% %% {i AND e AND k=v}S{i AND v