Theory SquareRoot_concept
section ‹ The Squareroot Example for Symbolic Execution ›
theory SquareRoot_concept
imports Clean.Test_Clean
begin
subsection‹ The Conceptual Algorithm in Clean Notation›
text‹ In high-level notation, the algorithm we are investigating looks like this:
@{cartouche [display=true]
‹‹
function_spec sqrt (a::int) returns int
pre "‹0 ≤ a›"
post "‹λres::int. (res + 1)⇧2 > a ∧ a ≥ (res)⇧2›"
defines " (‹tm := 1› ;-
‹sqsum := 1› ;-
‹i := 0› ;-
(while⇩S⇩E ‹sqsum <= a› do
‹i := i+1› ;-
‹tm := tm + 2› ;-
‹sqsum := tm + sqsum›
od) ;-
return⇩C result_value_update ‹i›
)"
››}
›
subsection‹ Definition of the Global State ›
text‹The state is just a record; and the global variables correspond to fields in this
record. This corresponds to typed, structured, non-aliasing states.
Note that the types in the state can be arbitrary HOL-types - want to have
sets of functions in a ghost-field ? No problem !
›
text‹ The state of the square-root program looks like this : ›
typ "Clean.control_state"
ML‹
val Type(s,t) = StateMgt_core.get_state_type_global @{theory}
val Type(u,v) = @{typ unit}
›
global_vars (state)
tm :: int
i :: int
sqsum :: int
ML‹
val Type(s,t) = StateMgt_core.get_state_type_global @{theory}
val Type(u,v) = @{typ unit}
›
lemma tm_independent [simp]: "♯ tm_update"
unfolding control_independence_def by auto
lemma i_independent [simp]: "♯ i_update"
unfolding control_independence_def by auto
lemma sqsum_independent [simp]: "♯ sqsum_update"
unfolding control_independence_def by auto
subsection‹ Setting for Symbolic Execution ›
text‹ Some lemmas to reason about memory›
lemma tm_simp : "tm (σ⦇tm := t⦈) = t"
using [[simp_trace]] by simp
lemma tm_simp1 : "tm (σ⦇sqsum := s⦈) = tm σ" by simp
lemma tm_simp2 : "tm (σ⦇i := s⦈) = tm σ" by simp
lemma sqsum_simp : "sqsum (σ⦇sqsum := s⦈) = s" by simp
lemma sqsum_simp1 : "sqsum (σ⦇tm := t⦈) = sqsum σ" by simp
lemma sqsum_simp2 : "sqsum (σ⦇i := t⦈) = sqsum σ" by simp
lemma i_simp : "i (σ⦇i := i'⦈) = i'" by simp
lemma i_simp1 : "i (σ⦇tm := i'⦈) = i σ" by simp
lemma i_simp2 : "i (σ⦇sqsum := i'⦈) = i σ" by simp
lemmas memory_theory =
tm_simp tm_simp1 tm_simp2
sqsum_simp sqsum_simp1 sqsum_simp2
i_simp i_simp1 i_simp2
declare memory_theory [memory_theory]
lemma non_exec_assign_globalD':
assumes "♯ upd"
shows "σ ⊨ upd :==⇩G rhs ;- M ⟹ ▹ σ ⟹ upd (λ_. rhs σ) σ ⊨ M"
apply(drule non_exec_assign_global'[THEN iffD1])
using assms exec_stop_vs_control_independence apply blast
by auto
lemmas non_exec_assign_globalD'_tm = non_exec_assign_globalD'[OF tm_independent]
lemmas non_exec_assign_globalD'_i = non_exec_assign_globalD'[OF i_independent]
lemmas non_exec_assign_globalD'_sqsum = non_exec_assign_globalD'[OF sqsum_independent]
text‹ Now we run a symbolic execution. We run match-tactics (rather than the Isabelle simplifier
which would do the trick as well) in order to demonstrate a symbolic execution in Isabelle. ›
subsection‹ A Symbolic Execution Simulation ›
lemma
assumes non_exec_stop[simp]: "¬ exec_stop σ⇩0"
and pos : "0 ≤ (a::int)"
and annotated_program:
"σ⇩0 ⊨ ‹tm := 1› ;-
‹sqsum := 1› ;-
‹i := 0› ;-
(while⇩S⇩E ‹sqsum <= a› do
‹i := i+1› ;-
‹tm := tm + 2› ;-
‹sqsum := tm + sqsum›
od) ;-
assert⇩S⇩E(λσ. σ=σ⇩R)"
shows "σ⇩R ⊨assert⇩S⇩E ‹i⇧2 ≤ a ∧ a < (i + 1)⇧2› "
apply(insert annotated_program)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_tm\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_sqsum\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_i\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"exec_whileD\"}] 1")
apply(tactic "ematch_tac @{context} [@{thm \"if_SE_execE''\"}] 1")
apply(simp_all only: memory_theory MonadSE.bind_assoc')
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_i\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_tm\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_sqsum\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"exec_whileD\"}] 1")
apply(tactic "ematch_tac @{context} [@{thm \"if_SE_execE''\"}] 1")
apply(simp_all only: memory_theory MonadSE.bind_assoc')
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_i\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_tm\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_sqsum\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"exec_whileD\"}] 1")
apply(tactic "ematch_tac @{context} [@{thm \"if_SE_execE''\"}] 1")
apply(simp_all only: memory_theory MonadSE.bind_assoc')
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_i\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_tm\"}] 1",simp)
apply(tactic "dmatch_tac @{context} [@{thm \"non_exec_assign_globalD'_sqsum\"}] 1",simp)
apply(simp_all)
text‹Here are all abstract test-cases explicit. Each subgoal correstponds to
a path taken through the loop.›
txt‹push away the test-hyp: postcond is true for programs with more than
three loop traversals (criterion: all-paths(k). This reveals explicitly
the three test-cases for @{term "k<3"}. ›
defer 1
oops
text‹TODO: re-establish automatic test-coverage tactics of \<^cite>‹"DBLP:conf/tap/Keller18"›.›
end