Theory PHoare
theory PHoare imports PLang begin
subsection‹Hoare logic for partial correctness›
text‹Taking auxiliary variables seriously means that assertions must
now depend on them as well as on the state. Initially we do not fix
the type of auxiliary variables but parameterize the type of
assertions with a type variable @{typ 'a}:›
type_synonym 'a assn = "'a ⇒ state ⇒ bool"
text‹
The second major change is the need to reason about Hoare
triples in a context: proofs about recursive procedures are conducted
by induction where we assume that all @{term CALL}s satisfy the given
pre/postconditions and have to show that the body does as well. The
assumption is stored in a context, which is a set of Hoare triples:›
type_synonym 'a cntxt = "('a assn × com × 'a assn)set"
text‹\noindent In the presence of only a single procedure the context will
always be empty or a singleton set. With multiple procedures, larger
sets can arise.
Now that we have contexts, validity becomes more complicated. Ordinary
validity (w.r.t.\ partial correctness) is still what it used to be,
except that we have to take auxiliary variables into account as well:
›
definition
valid :: "'a assn ⇒ com ⇒ 'a assn ⇒ bool" (‹⊨ {(1_)}/ (_)/ {(1_)}› 50) where
"⊨ {P}c{Q} ⟷ (∀s t. s -c→ t ⟶ (∀z. P z s ⟶ Q z t))"
text‹\noindent Auxiliary variables are always denoted by @{term z}.
Validity of a context and validity of a Hoare triple in a context are defined
as follows:›
definition
valids :: "'a cntxt ⇒ bool" (‹|⊨ _› 50) where
[simp]: "|⊨ C ≡ (∀(P,c,Q) ∈ C. ⊨ {P}c{Q})"
definition
cvalid :: "'a cntxt ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" (‹_ ⊨/ {(1_)}/ (_)/ {(1_)}› 50) where
"C ⊨ {P}c{Q} ⟷ |⊨ C ⟶ ⊨ {P}c{Q}"
text‹\noindent Note that @{prop"{} ⊨ {P}c{Q}"} is equivalent to
@{prop"⊨ {P}c{Q}"}.
Unfortunately, this is not the end of it. As we have two
semantics, ‹-c→› and ‹-c-n→›, we also need a second notion
of validity parameterized with the recursion depth @{term n}:›
definition
nvalid :: "nat ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" (‹⊨_ {(1_)}/ (_)/ {(1_)}› 50) where
"⊨n {P}c{Q} ≡ (∀s t. s -c-n→ t ⟶ (∀z. P z s ⟶ Q z t))"
definition
nvalids :: "nat ⇒ 'a cntxt ⇒ bool" (‹|⊨'__/ _› 50) where
"|⊨_n C ≡ (∀(P,c,Q) ∈ C. ⊨n {P}c{Q})"
definition
cnvalid :: "'a cntxt ⇒ nat ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" (‹_ ⊨_/ {(1_)}/ (_)/ {(1_)}› 50) where
"C ⊨n {P}c{Q} ⟷ |⊨_n C ⟶ ⊨n {P}c{Q}"
text‹Finally we come to the proof system for deriving triples in a context:›
inductive
hoare :: "'a cntxt ⇒ 'a assn ⇒ com ⇒ 'a assn ⇒ bool" (‹_ ⊢/ ({(1_)}/ (_)/ {(1_)})› 50)
where
Do:"C ⊢ {λz s. ∀t ∈ f s . P z t} Do f {P}"
| Semi:"⟦ C ⊢ {P}c1{Q}; C ⊢ {Q}c2{R} ⟧ ⟹ C ⊢ {P} c1;c2 {R}"
| If:"⟦ C ⊢ {λz s. P z s ∧ b s}c1{Q}; C ⊢ {λz s. P z s ∧ ¬b s}c2{Q} ⟧
⟹ C ⊢ {P} IF b THEN c1 ELSE c2 {Q}"
| While:"C ⊢ {λz s. P z s ∧ b s} c {P}
⟹ C ⊢ {P} WHILE b DO c {λz s. P z s ∧ ¬b s}"
| Conseq:"⟦ C ⊢ {P'}c{Q'}; ∀s t. (∀z. P' z s ⟶ Q' z t) ⟶ (∀z. P z s ⟶ Q z t) ⟧
⟹ C ⊢ {P}c{Q}"
| Call:"{(P,CALL,Q)} ⊢ {P}body{Q} ⟹ {} ⊢ {P} CALL {Q}"
| Asm:"{(P,CALL,Q)} ⊢ {P} CALL {Q}"
| Local: "⟦ ∀s'. C ⊢ {λz s. P z s' ∧ s = f s'} c {λz t. Q z (g s' t)} ⟧ ⟹
C ⊢ {P} LOCAL f;c;g {Q}"
abbreviation hoare1 :: "'a cntxt ⇒ 'a assn × com × 'a assn ⇒ bool" (‹_ ⊢ _›) where
"C ⊢ x ≡ C ⊢ {fst x}fst (snd x){snd (snd x)}"
text‹\noindent The first four rules are familiar, except for their adaptation
to auxiliary variables. The @{term CALL} rule embodies induction and
has already been motivated above. Note that it is only applicable if
the context is empty. This shows that we never need nested induction.
For the same reason the assumption rule (the last rule) is stated with
just a singleton context.
The rule of consequence is explained in the accompanying paper.
›
lemma strengthen_pre:
"⟦ ∀z s. P' z s ⟶ P z s; C⊢ {P}c{Q} ⟧ ⟹ C⊢ {P'}c{Q}"
by(rule hoare.Conseq, assumption, blast)
lemmas valid_defs = valid_def valids_def cvalid_def
nvalid_def nvalids_def cnvalid_def
theorem hoare_sound: "C ⊢ {P}c{Q} ⟹ C ⊨ {P}c{Q}"
txt‹\noindent requires a generalization: @{prop"∀n. C ⊨n
{P}c{Q}"} is proved instead, from which the actual theorem follows
directly via lemma @{thm[source]exec_iff_execn} in \S\ref{sec:proc1-lang}.
The generalization
is proved by induction on @{term c}. The reason for the generalization
is that soundness of the @{term CALL} rule is proved by induction on the
maximal call depth, i.e.\ @{term n}.›
apply(subgoal_tac "∀n. C ⊨n {P}c{Q}")
apply(unfold valid_defs exec_iff_execn)
apply fast
apply(erule hoare.induct)
apply simp
apply fast
apply simp
apply clarify
apply(drule while_rule)
prefer 3
apply (assumption, assumption)
apply fast
apply fast
prefer 2
apply simp
apply(rule allI, rule impI)
apply(induct_tac n)
apply blast
apply clarify
apply (simp(no_asm_use))
apply blast
apply auto
done
text‹
The completeness proof employs the notion of a \emph{most general triple} (or
\emph{most general formula}):›
definition
MGT :: "com ⇒ state assn × com × state assn" where
"MGT c = (λz s. z = s, c, λz t. z -c→ t)"
declare MGT_def[simp]
text‹\noindent Note that the type of @{term z} has been identified with
@{typ state}. This means that for every state variable there is an auxiliary
variable, which is simply there to record the value of the program variables
before execution of a command. This is exactly what, for example, VDM offers
by allowing you to refer to the pre-value of a variable in a
postcondition. The intuition behind @{term"MGT c"} is
that it completely describes the operational behaviour of @{term c}. It is
easy to see that, in the presence of the new consequence rule,
\mbox{@{prop"{} ⊢ MGT c"}} implies completeness:›
lemma MGT_implies_complete:
"{} ⊢ MGT c ⟹ {} ⊨ {P}c{Q} ⟹ {} ⊢ {P}c{Q::state assn}"
apply(simp add: MGT_def)
apply (erule hoare.Conseq)
apply(simp add: valid_defs)
done
text‹In order to discharge @{prop"{} ⊢ MGT c"} one proves›
lemma MGT_lemma: "C ⊢ MGT CALL ⟹ C ⊢ MGT c"
apply (simp)
apply(induct_tac c)
apply (rule strengthen_pre[OF _ hoare.Do])
apply blast
apply(blast intro:hoare.Semi hoare.Conseq)
apply(rule hoare.If)
apply(erule hoare.Conseq)
apply simp
apply(erule hoare.Conseq)
apply simp
prefer 2
apply simp
apply(rename_tac b c)
apply(rule hoare.Conseq)
apply(rule_tac P = "λz s. (z,s) ∈ ({(s,t). b s ∧ s -c→ t})^*"
in hoare.While)
apply(erule hoare.Conseq)
apply(blast intro:rtrancl_into_rtrancl)
apply clarsimp
apply(rename_tac s t)
apply(erule_tac x = s in allE)
apply clarsimp
apply(erule converse_rtrancl_induct)
apply simp
apply(fast elim:exec.WhileTrue)
apply(fastforce intro: hoare.Local elim!: hoare.Conseq)
done
text‹\noindent The proof is by induction on @{term c}. In the @{term
While}-case it is easy to show that @{term"λz t. (z,t) ∈ ({(s,t). b
s ∧ s -c→ t})^*"} is invariant. The precondition \mbox{@{term[source]"λz s. z=s"}}
establishes the invariant and a reflexive transitive closure
induction shows that the invariant conjoined with @{prop"¬b t"}
implies the postcondition \mbox{@{term"λz t. z -WHILE b DO c→ t"}}. The
remaining cases are trivial.
Using the @{thm[source]MGT_lemma} (together with the ‹CALL› and the
assumption rule) one can easily derive›
lemma MGT_CALL: "{} ⊢ MGT CALL"
apply(simp add: MGT_def)
apply (rule hoare.Call)
apply (rule hoare.Conseq[OF MGT_lemma[simplified], OF hoare.Asm])
apply (fast intro:exec.intros)
done
text‹\noindent Using the @{thm[source]MGT_lemma} once more we obtain
@{prop"{} ⊢ MGT c"} and thus by @{thm[source]MGT_implies_complete}
completeness.›
theorem "{} ⊨ {P}c{Q} ⟹ {} ⊢ {P}c{Q::state assn}"
apply(erule MGT_implies_complete[OF MGT_lemma[OF MGT_CALL]])
done
end