%%% %%% 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 %%% %%% Note November 17, 1999: we adapt type coercion to PVS 2.3 %%% new syntax, replacing ":" with "::". %%% Note November 27, 1999: For the proof of "wc", with PVS 2.3, %%% we had to replace REWRITE with LEMMA %%% and INST? with same :SUBST, as REWRITE %%% no longer worked! Similar problem with %%% "ws" proof. %%% standard_verification[domain: TYPE]: THEORY BEGIN ASSUMING two_elements_in_domain: ASSUMPTION (EXISTS (d1, d2: domain): d1 /= d2) ; ENDASSUMING IMPORTING standard_programming[domain] %% %% We implement an auto-rewrite Hoare calculus which combines %% the basic statement rules (assignment, if then else, while) %% with sequential composition and or comment. %% %% %% "cc" is provided for the case where the user has provided %% a comment with a unique statement (or the leftmost statement %% in a sequence). This is normally nouse, but it triggers a %% "left_consequence" application, and is auto-rewrite! %% cc: LEMMA % auto-rewrite! %% %% p => pp, {pp} S {q} %% --------------------- %% {p}[|pp, S|]{q} %% (FORALL (p, pp, q: assertion, S: program): ((p IMPLIES pp) AND correct?(pp, S, q)) IMPLIES correct?(p, [|pp, S|], q)) ; %% %% "ac" is a combination of "assignment_hoare_rule" %% and "left_consequence" %% ac: LEMMA % Auto-rewrite! %% %% p=>q[x/t] %% ---------- %% {p}x:=t{q} %% (FORALL (p, q: assertion, x: variable, t: term): (p IMPLIES alt(x,t)(q)) IMPLIES correct?(p, set(x, t), q)) ; %% %% "as" is a combination of "assignment_hoare_rule" and %% "compose_hoare_rule": %% as: LEMMA % Auto-rewrite! %% %% {p} S {q[x/t]} %% ----------------- %% {p} S; x:=t {q} %% (FORALL (p, q: assertion, S: program, x: variable, t: term): correct?(p, S, alt(x, t)(q)) IMPLIES correct?(p, S @@ set(x, t), q)) ; %% %% "asc" is a combination of "as" and "right_consequence_hoare_rule" %% provided for the sake of completeness, in case the user %% comments an assignment located at the end of a sequence: %% asc: LEMMA % Auto-rewrite! %% %% {p} S {pp}, pp=>q[x/t] %% --------------------------- %% {p} S; [| pp, x:=t |] {q} %% (FORALL (p, pp, q: assertion, S: program, x: variable, t: term): (correct?(p, S, pp) AND (pp IMPLIES alt(x, t)(q))) IMPLIES correct?(p, S @@ [| pp, set(x, t) |], q)) ; %% %% "ifh" is a short name for "if_hoare_rule": %% ifh: LEMMA %% %% {p AND e}S1{q}, {p AND NOT(e)}S2{q} %% ----------------------------------- %% {p}if e then S1 else S2 endif{q} %% (FORALL (p, q, e: assertion, S1, S2: program): (correct?(p AND e, S1, q) AND correct?(p AND NOT(e), S2, q)) IMPLIES correct?(p, IF e THEN S1 ELSE S2 ENDIF, q)) %% %% "is" is a combination of commented "if_then_else_hoare_rule" and %% "compose_hoare_rule" (note the use of a comment "[||]" to make %% the rule auto-rewrite by suggesting "pp"): %% is: LEMMA % auto-rewrite! %% %% %% {p}S{pp}, {pp/\e}S1{q}, {pp/\~e}S2{q} %% ------------------------------------------------ %% {p} S; [|pp, if e then S1 else S2 endif|] {q} %% (FORALL (p, pp, q, e: assertion, S1, S2, S: program): ( correct?(p, S, pp) AND correct?(pp AND e, S1, q) AND correct?(pp AND NOT e, S2, q)) IMPLIES correct?(p, S @@ [| pp, IF e THEN S1 ELSE S2 ENDIF |], q)) ; %% %% "wc" is a combination of "while_hoare_rule" and %% "consequence_hoare_rule": %% wc: LEMMA % auto-rewrite! %% %% p IMPLIES i, {i/\e}L{i}, i/\~e IMPLIES q %% ---------------------------------------- if v decreases! %% {p}while(r, v, i) e do L od{q} %% (FORALL (r: (well_founded?[domain]), v: term, i, e, p, q: assertion, L: (terminates?(r, v, i)(e))): ( (p IMPLIES i):: bool AND ((i AND NOT e) IMPLIES q)) IMPLIES correct?(p, while(r, v, i)(e, L), q)) ; %% %% "ws" is a combination of "while_hoare_rule", %% "compose_hoare_rule" and "right_consequence_hoare_rule": %% ws: LEMMA % auto-rewrite! %% %% {p}S{i}, {i/\e}L{i}, i/\~e IMPLIES q %% -------------------------------------- if v decreases! %% {p} S; while(r, v, i) e do L od {q} %% (FORALL (r: (well_founded?[domain]), v: term, i, e, p, q: assertion, S: program, L: (terminates?(r, v, i)(e))): ( correct?(p, S, i) AND ((i AND NOT e) IMPLIES q)) IMPLIES correct?(p, S @@ while(r, v, i)(e, L), q)) ; %% %% "wsc" is a combination of "ws" and "consequence_hoare_rule": %% It is provided for the sake of completeness, since the %% user might comment a "while" statement at the end of %% a sequence, which is not really useful since the %% invariant "i" is already a comment. %% wsc: LEMMA % auto-rewrite! %% %% {p}S{pp}, pp=>i, {i/\e}L{i}, i/\~e => q %% ----------------------------------------------- if v decreases! %% {p} S; [| pp, while(r, v, i) e do L od |] {q} %% (FORALL (r: (well_founded?[domain]), v: term, i, e, p, pp, q: assertion, S: program, L: (terminates?(r, v, i)(e))): ( correct?(p, S, pp) AND ((pp IMPLIES i):: bool) AND ((i AND NOT e) IMPLIES q)) IMPLIES correct?(p, S @@ [| pp, while(r, v, i)(e, L) |], q)) ; %% %% Since "terminates?" is defined in terms of "corrdecr?" %% and "corrdecr?" is defined in terms of "lift_" we need to %% rewrite "lift_" into "l", so that "alt_..." rules can apply: %% lift_l_d: LEMMA (FORALL (d: domain): lift_(d) = l(d)) ; lift_l_db2: LEMMA (FORALL (r: pred[[domain, domain]]): lift_(r) = l(r)) ; %% %% Substitution (alt) simplifications: %% alt_ld: LEMMA % l(d)[x/t] = l(d) . (FORALL (x: variable, t: term, d: domain): alt(x, t)(l(d)) = l(d)) ; alt_true: LEMMA % TRUE[x/t] = TRUE . (FORALL (x: variable, t: term): alt(x, t)(TRUE) = TRUE) ; alt_false: LEMMA % FALSE[x/t] = FALSE . (FORALL (x: variable, t: term): alt(x, t)(FALSE) = FALSE) ; alt_dd1: LEMMA % l(ddo)(t1)[x/t] = l(op)(t1[x/t]) . (FORALL (x: variable, t, t1: term, ddo: unary[domain]): alt(x, t)(l(ddo)(t1)) = l(ddo)(alt(x, t)(t1))) ; alt_db1: LEMMA % l(dbo)(t1)[x/t] = l(dbo)(t1[x/t]) . (FORALL (x: variable, t, t1: term, dbo: unary[domain, bool]): alt(x, t)(l(dbo)(t1)) = l(dbo)(alt(x, t)(t1))) ; alt_bb1: LEMMA % l(bbo)(a1)[x/t] = l(bbo)(a1[x/t]) . (FORALL (x: variable, t: term, a1: assertion, bbo: unary[bool, bool]): alt(x, t)(l(bbo)(a1)) = l(bbo)(alt(x, t)(a1))) ; alt_not: LEMMA % (NOT a)[x/t] = NOT a[x/t] . (FORALL (x: variable, t: term, a1: assertion): alt(x, t)(NOT a1) = NOT alt(x, t)(a1)) ; alt_dd2: LEMMA % l(ddo)(t1, t2)[x/t] % = l(ddo)(t1[x/t], t2[x/t]) . (FORALL (x: variable, t, t1, t2: term, ddo: binary[domain]): alt(x, t)(l(ddo)(t1, t2)) = l(ddo)(alt(x, t)(t1), alt(x, t)(t2))) ; alt_db2: LEMMA % l(dbo)(t1, t2)[x/t] % = l(dbo)(t1[x/t], t2[x/t])) . (FORALL (x: variable, t, t1, t2: term, dbo: binary[domain, bool]): alt(x, t)(l(dbo)(t1, t2)) = l(dbo)(alt(x, t)(t1), alt(x, t)(t2))) ; alt_equals: LEMMA % equals(t1, t2)[x/t] % = equals(t1[x/t], t2[x/t]) . (FORALL (x: variable, t, t1, t2: term): alt(x, t)(equals(t1, t2)) = equals(alt(x, t)(t1), alt(x, t)(t2))) ; alt_bb2: LEMMA % l(bbo)(a1, a2)[x/t] % = l(bbo)(a1[x/t], a2[x/t]) . (FORALL (x: variable, t: term, a1, a2: assertion, bbo: binary[bool, bool]): alt(x, t)(l(bbo)(a1, a2)) = l(bbo)(alt(x, t)(a1), alt(x, t)(a2))) ; alt_and: LEMMA % (a1 AND a2)[x/t] = a1[x/t] AND a2[x/t] . (FORALL (x: variable, t: term, a1, a2: assertion): alt(x, t)(a1 AND a2) = (alt(x, t)(a1) AND alt(x, t)(a2))) ; alt_or: LEMMA % (a1 OR a2)[x/t] = a1[x/t] OR a2[x/t] . (FORALL (x: variable, t: term, a1, a2: assertion): alt(x, t)(a1 OR a2) = (alt(x, t)(a1) OR alt(x, t)(a2))) ; alt_implies: LEMMA % (a1 => a2)[x/t] = a1[x/t] => a2[x/t] . (FORALL (x: variable, t: term, a1, a2: assertion): alt(x, t)(a1 IMPLIES a2) = (alt(x, t)(a1) IMPLIES alt(x, t)(a2))) ; alt_dd3: LEMMA % l(ddo)(t1, t2, t3)[x/t] % = l(ddo)(t1[x/t], t2[x/t], t3[x/t]) . (FORALL (x: variable, t, t1, t2, t3: term, ddo: ternary[domain]): alt(x, t)(l(ddo)(t1, t2, t3)) = l(ddo)(alt(x, t)(t1), alt(x, t)(t2), alt(x, t)(t3))) ; alt_db3: LEMMA % l(dbo)(t1, t2, t3)[x/t] % = l(dbo)(t1[x/t], t2[x/t], t3[x/t])) . (FORALL (x: variable, t, t1, t2, t3: term, dbo: ternary[domain, bool]): alt(x, t)(l(dbo)(t1, t2, t3)) = l(dbo)(alt(x, t)(t1), alt(x, t)(t2), alt(x, t)(t3))) ; alt_bb3: LEMMA % l(bbo)(a1, a2, a3)[x/t] % = l(bbo)(a1[x/t], a2[x/t], a3[x/t]) . (FORALL (x: variable, t: term, a1, a2, a3: assertion, bbo: ternary[bool, bool]): alt(x, t)(l(bbo)(a1, a2, a3)) = l(bbo)(alt(x, t)(a1), alt(x, t)(a2), alt(x, t)(a3))) ; alt_xtx: LEMMA % x[x/t] = t . (FORALL (x: variable, t: term): alt(x, t)(x) = t) ; %% %% This lemma should be applied only when "alt_xtx" has failed! %% Otherwise it will yield unprovable subgoals of the form %% X /= X, where X is a variable. %% alt_xty: LEMMA % y[x/t] = y, provided that x /= y. (FORALL (x, y: variable, t: term): x /= y IMPLIES alt(x, t)(y) = y) ; END standard_verification