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