theory exam_14
imports "AutoCorres"
begin
text {*
This theory is designed to be loaded with the AutoCorres logic/image via e.g.
L4V_ARCH=X64 isabelle jedit -d autocorres-1.4 -l AutoCorres exam_14.thy
OR:
L4V_ARCH=ARM isabelle jedit -d autocorres-1.4 -l AutoCorres exam_14.thy
(it was an older version back in 2014, but updated here to autocorres-1.4
to have the same version than the one used in this year's lecture)
*}
section "Question 1: Lambda Calculus"
text {*
(a) -- (c): Write your answers as Isabelle comments or include them in a separate .pdf
or .txt file.
*}
section "Question 2: Induction"
text {*
(a-i)
*}
inductive_set pal_lists where
pal_nil: "\"
text {*
(a-ii)
*}
lemma pal_lists_Cons:
"xs \ pal_lists ==> x # xs \ pal_lists"
sorry
text {*
(a-iii)
*}
lemma pal_univ: "xs \ pal_lists"
sorry
text {*
(a-iv)
*}
lemma pal_induct:
assumes nil: "P []"
assumes one: "\x. P [x]"
assumes two: "\a xs b. P xs \ P (a # xs @ [b])"
shows "P list"
sorry
text {*
(b)
*}
(* define palindrome *)
text {*
(c)
*}
lemma pal_eq:
"palindrome (a # xs @ [b]) \ a = b"
sorry
text {*
(d)
*}
inductive_set palindromes where
p_nil: "\"
text {*
(e)
*}
lemma "palindrome xs = (xs \ palindromes)"
oops
section "C Verification"
install_C_file "divmod.c"
autocorres [unsigned_word_abs = divmod even] "divmod.c"
context divmod begin
text {*
(a) -- (b): Write your answers as Isabelle comments or include them in a separate .pdf
or .txt file.
*}
text {*
(c)
*}
definition
divmod_spec :: "nat \ nat \ nat \ nat"
where
"divmod_spec n m domod \ if domod \ 0 then n mod m else n div m"
lemma divmod'_correct:
"ovalid (\_. True) (divmod' n m domod) (\r s. r = divmod_spec n m domod)"
sorry
text {*
(d): replace PRE below with a suitable weakest precondition and prove it correct
*}
lemma divmod'_wp:
"ovalid PRE (divmod' n m domod) Q"
sorry
text {*
(e)
*}
lemma even'_correct:
"ovalid (\_. True) (even' n) (\r s. r = (if even n then 1 else 0))"
sorry
text {*
(f): Write your answer as an Isabelle comment or in a separate .pdf or .txt file
*}
end
end