theory cm7 imports Main begin (* -------- Model-checking explained in Isabelle/HOL ----------- *) (* States of the automaton *) datatype etat= Init | LuA | LuB | Final (* Letter to type on the digicode *) datatype lettre= A | B | C | D fun transition:: "lettre*etat \ etat" where "transition(A,Init) = LuA" | "transition(_,Init) = Init" | "transition(B,LuA) = LuB" | "transition(A,LuA) = LuA" | "transition(_,LuA) = Init" | "transition(C,LuB) = Final" | "transition(A,LuB) = LuA" | "transition(_,LuB) = Init" | "transition(A,Final) = LuA" | "transition(_,Final) = Init" fun execution:: "lettre list * etat \ etat" where "execution([],e) = e" | "execution((x#xs),e) = execution(xs,transition(x,e))" value "execution([A,B],Init)" value "execution([A,B,C],Init)" (* Exercise 1 *) (* 1) Whatever the state e we start from, after typing [A,B,C] we reach the Final State *) lemma zeroLetter: "" apply (case_tac e) apply auto done (* Exercise 2 *) (* 2) Whatever the state e we start from, the only way to reach the Final State is to type [A,B,C] *) theorem zeroLetter2: "" apply (case_tac x) apply (case_tac [1-] y) apply (case_tac [1-] z) apply (case_tac [1-] e) apply auto done (* 1) can be generalized to any sequence of letters if it ends by [A,B,C] *) theorem execAppend: "\ e. execution(l1@l2,e)= execution(l2,execution(l1,e))" apply (induct l1) apply auto done theorem "execution(l@[A,B,C],e)=Final" by (metis execAppend zeroLetter) (* 2) can be generalized in the same way *) theorem "execution(l@[x,y,z],Init)=Final \ x=A \ y=B \ z=C" by (metis (lifting) execAppend zeroLetter2) (* ----- Static analyzer explained in Isabelle/HOL -------*) (* Exercice 3 *) (* We have D=int and we choose the following abstract domain: D# *) datatype absInt= Neg | Zero | Pos | Undef | Any (* Any / | \ Neg Zero Pos \ | / Undef *) fun infeq:: "absInt \ absInt \ bool" (infix "<#" 65) where "infeq Undef _ = True"| "infeq _ Any = True"| "infeq x y = (x=y)" fun abs:: "int \ absInt" where " = " (* Exercice 4 *) fun absPlus:: "absInt \ absInt \ absInt" (infix "+#" 65) where " = " (* Exercice 5 *) lemma abs_correct: "ALL x y. ..." apply (case_tac "(abs x)") apply (case_tac [1-] "(abs y)") apply auto done end