(*<*)
theory ex10
imports Hoare Hoare_Sound_Complete
begin
(*>*)
text {* \ExerciseSheet{10}{23.~12.~2011} *}
text {*
\Exercise{Forward Assignment Rule}
Think up and prove a forward assignment rule, i.e., a rule of the
form @{text "\ {P} x::=a {\}"}, where @{text "\"} is some suitable
postcondition. Hint: To prove this rule, use the completeness
property, and prove the rule semantically.
*}
(*<*)
lemma fwd_Assign: "\ {P} x::=a { \s'. \s. P s \ s'=s[a/x]}"
apply (rule hoare_relative_complete)
unfolding hoare_valid_def
by auto
(*>*)
text {* Redo the proofs for @{text "MAX"} and @{text "MUL"} from the previous
exercise sheet, this time using your forward assignment rule.
*}
(*<*)
definition MAX :: com where
"MAX \
IF (Less (V ''a'') (V ''b'')) THEN
''c''::=V ''b''
ELSE
''c''::=V ''a''"
lemma [simp]: "(a::int)** max a b = b"
by (metis order_less_imp_le sup_absorb2 sup_int_def)
lemma [simp]: "\(a::int)**** max a b = a"
by (metis leI min_max.sup_absorb1)
lemmas fwd_Assign' = weaken_post[OF fwd_Assign]
lemma "\ {\s. True} MAX {\s. s ''c'' = max (s ''a'') (s ''b'')}"
unfolding MAX_def
apply (rule If)
apply (rule fwd_Assign')
apply (auto) []
apply (rule fwd_Assign')
apply (auto)
done
definition MUL :: com where
"MUL \
''z''::=N 0;
''c''::=N 0;
WHILE (Less (V ''c'') (V ''y'')) DO (
''z''::=Plus (V ''z'') (V ''x'');
''c''::=Plus (V ''c'') (N 1))"
lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}"
unfolding MUL_def
apply (rule Semi fwd_Assign fwd_Assign' If
strengthen_pre[OF
_ While'[where P="\s. s ''z'' = s ''x'' * s ''c'' \ s ''c'' \ s ''y''"]
]
| auto simp add: algebra_simps)+
done
(*>*)
text {*
\Exercise{More Hoare-Rules}
Which of the following Hoare-rules are correct?
Proof or counterexample!
*}
(*<*)
lemma hoare_by_sem: "\ {P}c{Q} \ \ {P}c{Q}"
using hoare_sound hoare_relative_complete by blast
(*>*)
lemma
"\\ {P} c {Q}; \ {P'} c {Q'}\ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}"
(*<*)
apply (simp add: hoare_by_sem)
unfolding hoare_valid_def
by blast
(*>*)
lemma
"\\ {P} c {Q}; \ {P'} c {Q'}\ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}"
(*<*)
apply (simp add: hoare_by_sem)
unfolding hoare_valid_def
by blast
(*>*)
lemma
"\\ {P} c {Q}; \ {P'} c {Q'}\ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}"
(*<*) oops
lemma
defines "P\\x. False" and "Q\\x. True"
and "P'\\x. False" and "Q'\\x. False"
and "c\SKIP"
shows
"\ {P} c {Q} \ \ {P'} c {Q'} \ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}"
apply (simp add: hoare_by_sem)
unfolding hoare_valid_def P_def Q_def P'_def Q'_def c_def
by blast
(*>*)
text {*
\Homework{Be Original!}{18~January~2012}
Think up a nice formalization yourself!
Here are some ideas:
\begin{itemize}
\item Add some new language features to IMP, and redo some proofs
(e.g., compiler,typing,Hoare-Logic).
\item
A control flow graph (CFG) is a graph where edges are labeled by either an
assignment or a boolean expression. An assignment causes a state change
and a boolean expression restricts which states can traverse this edge.
Formalize an operational semantics of control flow graphs and prove
some nice results, e.g., compiler (IMP$\to$CFG or CFG$\to$STACK),
Floyd-style correctness proofs.
\item Compile commands to a register machine, and show correctness.
\item Prove correct some non-trivial program, e.g., square roots
using the bisection method. Hint: A modular approach of writing and
proving programs may help, e.g., you may try to reuse a program for
multiplication and its correctness proof, rather then inlining the
program and the proof.
\item Formalize $\beta$-reduction for (untyped) lambda calculus.
\end{itemize}
You should yourself set a time limit before starting your project.
Also incomplete/unfinished formalizations are welcome and will be graded!
*}
(*<*)
end
(*>*)
**