Theory Quicksort_concept
chapter ‹ Clean Semantics : A Coding-Concept Example›
text‹The following show-case introduces subsequently a non-trivial example involving
local and global variable declarations, declarations of operations with pre-post conditions as
well as direct-recursive operations (i.e. C-like functions with side-effects on global and
local variables. ›
theory Quicksort_concept
imports Clean.Clean
Clean.Hoare_Clean
Clean.Clean_Symbex
begin
section‹The Quicksort Example›
text‹ We present the following quicksort algorithm in some conceptual, high-level notation:
\begin{isar}
algorithm (A,i,j) =
tmp := A[i];
A[i]:=A[j];
A[j]:=tmp
algorithm partition(A, lo, hi) is
pivot := A[hi]
i := lo
for j := lo to hi - 1 do
if A[j] < pivot then
swap A[i] with A[j]
i := i + 1
swap A[i] with A[hi]
return i
algorithm quicksort(A, lo, hi) is
if lo < hi then
p := partition(A, lo, hi)
quicksort(A, lo, p - 1)
quicksort(A, p + 1, hi)
\end{isar}
›
text‹In the following, we will present the Quicksort program alternatingly in Clean high-level
notation and simulate its effect by an alternative formalisation representing the semantic
effects of the high-level notation on a step-buy-step basis. Note that Clean does not posses
the concept of call-by-reference parameters; consequently, the algorithm must be specialized
to a variant where @{term A} is just a global variable.›
section‹Clean Encoding of the Global State of Quicksort›
text‹We demonstrate the accumulating effect of some key Clean commands by highlighting the
changes of Clean's state-management module state. At the beginning, the state-type of
the Clean state management is just the type of the @{typ "'a Clean.control_state.control_state_ext"},
while the table of global and local variables is empty.›
ML‹ val Type(s,t) = StateMgt_core.get_state_type_global @{theory};
StateMgt_core.get_state_field_tab_global @{theory}; ›
text‹The ‹global_vars› command, described and defined in ▩‹Clean.thy›,
declares the global variable ▩‹A›. This has the following effect:›
global_vars (S)
A :: "int list"
ML‹
(fst o StateMgt_core.get_data_global) @{theory}
›
global_vars (S2)
B :: "int list"
ML‹
(Int.toString o length o Symtab.dest o fst o StateMgt_core.get_data_global) @{theory}
›
find_theorems (60) name:global_state2_state
find_theorems create⇩L name:"Quick"
text‹... which is reflected in Clean's state-management table:›
ML‹ val Type("Quicksort_concept.global_S2_state_scheme",t)
= StateMgt_core.get_state_type_global @{theory};
(Int.toString o length o Symtab.dest)(StateMgt_core.get_state_field_tab_global @{theory})›
text‹Note that the state-management uses long-names for complete disambiguation.›
subsubsection‹A Simulation of Synthesis of Typed Assignment-Rules›
definition A⇩L' where "A⇩L' ≡ create⇩L global_S_state.A global_S_state.A_update"
lemma A⇩L'_control_indep : "(break_status⇩L ⨝ A⇩L' ∧ return_status⇩L ⨝ A⇩L')"
unfolding A⇩L'_def break_status⇩L_def return_status⇩L_def create⇩L_def upd2put_def
by (simp add: lens_indep_def)
lemma A⇩L'_strong_indep : "♯! A⇩L'"
unfolding strong_control_independence_def
using A⇩L'_control_indep by blast
text‹Specialized Assignment Rule for Global Variable ‹A›.
Note that this specialized rule of @{thm assign_global} does not
need any further side-conditions referring to independence from the control.
Consequently, backward inference in an ‹wp›-calculus will just maintain
the invariant @{term ‹¬ exec_stop σ›}.›
lemma assign_global_A:
"⦃λσ. ▹ σ ∧ P (σ⦇A := rhs σ⦈)⦄ A_update :==⇩G rhs ⦃λr σ. ▹ σ ∧ P σ ⦄"
apply(rule assign_global)
apply(rule strong_vs_weak_upd [of global_S_state.A global_S_state.A_update])
apply (metis A⇩L'_def A⇩L'_strong_indep)
by(rule ext, rule ext, auto)
section ‹Encoding swap in Clean›
subsection ‹▩‹swap› in High-level Notation›
text‹Unfortunately, the name ‹result› is already used in the logical context; we use local binders
instead.›
definition "i = ()"
definition "j = ()"
function_spec swap (i::nat,j::nat)
pre "‹i < length A ∧ j < length A›"
post "‹λres. length A = length(old A) ∧ res = ()›"
local_vars tmp :: int
defines " ‹ tmp := A ! i› ;-
‹ A := list_update A i (A ! j)› ;-
‹ A := list_update A j tmp› "
value "⦇break_status = False, return_status = False, A = [1,2,3],
tmp = [], result_value = [], … = X⦈"
term swap
find_theorems (70) name:"local_swap_state"
value "swap (0,1) ⦇break_status = False, return_status = False, A = [1,2,3], B=[],
tmp = [],
result_value = [],… = X⦈"
text‹The body --- heavily using the ‹λ›-lifting cartouche --- corresponds to the
low level term: ›
text‹ @{cartouche [display=true]
‹‹defines " ((assign_local tmp_update (λσ. (A σ) ! i )) ;-
(assign_global A_update (λσ. list_update (A σ) (i) (A σ ! j))) ;-
(assign_global A_update (λσ. list_update (A σ) (j) ((hd o tmp) σ))))"››}›
text‹The effect of this statement is generation of the following definitions in the logical context:›
term "(i, j)"
thm push_local_swap_state_def
thm pop_local_swap_state_def
thm swap_pre_def
thm swap_post_def
thm swap_core_def
thm swap_def
text‹The state-management is in the following configuration:›
ML‹ val Type(s,t) = StateMgt_core.get_state_type_global @{theory};
StateMgt_core.get_state_field_tab_global @{theory}›
subsection ‹A Similation of ▩‹swap› in elementary specification constructs:›
text‹Note that we prime identifiers in order to avoid confusion with the definitions of the
previous section. The pre- and postconditions are just definitions of the following form:›
definition swap'_pre :: " nat × nat ⇒ 'a global_S_state_scheme ⇒ bool"
where "swap'_pre ≡ λ(i, j) σ. i < length (A σ) ∧ j < length (A σ)"
definition swap'_post :: "'a × 'b ⇒ 'c global_S_state_scheme ⇒ 'd global_S_state_scheme ⇒ unit ⇒ bool"
where "swap'_post ≡ λ(i, j) σ⇩p⇩r⇩e σ res. length (A σ) = length (A σ⇩p⇩r⇩e) ∧ res = ()"
text‹The somewhat vacuous parameter ‹res› for the result of the swap-computation is the conseqeuence
of the implicit definition of the return-type as @{typ "unit"}›
text‹We simulate the effect of the local variable space declaration by the following command
factoring out the functionality into the command ‹local_vars_test› ›
local_vars_test (swap' "unit")
tmp :: "int"
text‹The immediate effect of this command on the internal Clean State Management
can be made explicit as follows: ›
ML‹
val Type(s,t) = StateMgt_core.get_state_type_global @{theory};
val tab = StateMgt_core.get_state_field_tab_global @{theory};
@{term "A::('a local_swap_state_scheme⇒ int list)"}›
text‹This has already the effect of the definition:›
thm push_local_swap_state_def
thm pop_local_swap_state_def
text‹Again, we simulate the effect of this command by more elementary \HOL specification constructs:›
definition push_local_swap_state' :: "(unit,'a local_swap'_state_scheme) MON⇩S⇩E"
where "push_local_swap_state' σ =
Some((),σ⦇local_swap'_state.tmp := undefined # local_swap'_state.tmp σ ⦈)"
definition pop_local_swap_state' :: "(unit,'a local_swap'_state_scheme) MON⇩S⇩E"
where "pop_local_swap_state' σ =
Some(hd(local_swap_state.result_value σ),
σ⦇local_swap_state.tmp:= tl( local_swap_state.tmp σ) ⦈)"
definition swap'_core :: "nat × nat ⇒ (unit,'a local_swap'_state_scheme) MON⇩S⇩E"
where "swap'_core ≡ (λ(i,j).
((assign_local tmp_update (λσ. A σ ! i )) ;-
(assign_global A_update (λσ. list_update (A σ) (i) (A σ ! j))) ;-
(assign_global A_update (λσ. list_update (A σ) (j) ((hd o tmp) σ)))))"
text‹ a block manages the "dynamically" created fresh instances for the local variables of swap ›
definition swap' :: "nat × nat ⇒ (unit,'a local_swap'_state_scheme) MON⇩S⇩E"
where "swap' ≡ λ(i,j). block⇩C push_local_swap_state' (swap_core (i,j)) pop_local_swap_state'"
text‹NOTE: If local variables were only used in single-assignment style, it is possible
to drastically simplify the encoding. These variables were not stored in the state,
just kept as part of the monadic calculation. The simplifications refer both to
calculation as well as well as symbolic execution and deduction.›
text‹The could be represented by the following alternative, optimized version :›
definition swap_opt :: "nat × nat ⇒ (unit,'a global_S_state_scheme) MON⇩S⇩E"
where "swap_opt ≡ λ(i,j). (tmp ← yield⇩C (λσ. A σ ! i) ;
((assign_global A_update (λσ. list_update (A σ) (i) (A σ ! j))) ;-
(assign_global A_update (λσ. list_update (A σ) (j) (tmp)))))"
text‹In case that all local variables are single-assigned in swap, the entire local var definition
could be ommitted.›
text‹A more pretty-printed term representation is:›
term‹ swap_opt = (λ(i, j).
tmp ← (yield⇩C (λσ. A σ ! i));
(A_update :==⇩G (λσ. (A σ)[i := A σ ! j]) ;-
A_update :==⇩G (λσ. (A σ)[j := tmp])))›
subsubsection‹A Simulation of Synthesis of Typed Assignment-Rules›
definition tmp⇩L
where "tmp⇩L ≡ create⇩L local_swap'_state.tmp local_swap'_state.tmp_update"
lemma tmp⇩L_control_indep : "(break_status⇩L ⨝ tmp⇩L ∧ return_status⇩L ⨝ tmp⇩L)"
unfolding tmp⇩L_def break_status⇩L_def return_status⇩L_def create⇩L_def upd2put_def
by (simp add: lens_indep_def)
lemma tmp⇩L_strong_indep : "♯! tmp⇩L"
unfolding strong_control_independence_def
using tmp⇩L_control_indep by blast
text‹Specialized Assignment Rule for Local Variable ‹tmp›.
Note that this specialized rule of @{thm assign_local} does not
need any further side-conditions referring to independence from the control.
Consequently, backward inference in an ‹wp›-calculus will just maintain
the invariant @{term ‹▹ σ›}.›
lemma assign_local_tmp:
"⦃λσ. ▹ σ ∧ P ((tmp_update ∘ upd_hd) (λ_. rhs σ) σ)⦄
local_swap'_state.tmp_update :==⇩L rhs
⦃λr σ. ▹ σ ∧ P σ ⦄"
apply(rule assign_local)
apply(rule strong_vs_weak_upd_list)
apply(rule tmp⇩L_strong_indep[simplified tmp⇩L_def])
by(rule ext, rule ext, auto)
section ‹Encoding ▩‹partition› in Clean›
subsection ‹▩‹partition› in High-level Notation›