diff --git a/thys/Clean/ROOT b/thys/Clean/ROOT --- a/thys/Clean/ROOT +++ b/thys/Clean/ROOT @@ -1,54 +1,59 @@ chapter AFP (****************************************************************************** * Clean * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) (* * Clean --- a basic abstract ("shallow") programming language for test and proof. * Authors : Burkhart Wolff, Frédéric Tuong * Contributions by Chantal Keller *) session Clean (AFP) = HOL + options [timeout = 300] + sessions + "HOL-Eisbach" + directories + "src" + "examples" theories - "src/Clean_Main" - "examples/Quicksort_concept" - "examples/SquareRoot_concept" + "Clean_Main" + "Quicksort_concept" + "SquareRoot_concept" document_files "root.tex" "root.bib" "lstisadof.sty" diff --git a/thys/Clean/examples/Quicksort_concept.thy b/thys/Clean/examples/Quicksort_concept.thy --- a/thys/Clean/examples/Quicksort_concept.thy +++ b/thys/Clean/examples/Quicksort_concept.thy @@ -1,449 +1,449 @@ (****************************************************************************** * Clean * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) (* - * Quicksort Concept + * Quicksort Concept * * Authors : Burkhart Wolff, Frédéric Tuong *) 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_Main.Clean - Clean_Main.Hoare_MonadSE + imports Clean + Hoare_MonadSE 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 +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 +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 \<^verbatim>\Clean.thy\, declares the global variable \<^verbatim>\A\. This has the following effect:\ global_vars state A :: "int list" text\... which is reflected in Clean's state-management table:\ -ML\ val Type("Quicksort_concept.global_state_state_scheme",t) +ML\ val Type("Quicksort_concept.global_state_state_scheme",t) = StateMgt_core.get_state_type_global @{theory}; StateMgt_core.get_state_field_tab_global @{theory}\ text\Note that the state-management uses long-names for complete disambiguation.\ section \Encoding swap in Clean\ subsection \\<^verbatim>\swap\ in High-level Notation\ text\Unfortunately, the name \result\ is already used in the logical context; we use local binders instead.\ definition "i = ()" \ \check that \<^term>\i\ can exist as a constant with an arbitrary type before treating \<^theory_text>\function_spec\\ definition "j = ()" \ \check that \<^term>\j\ can exist as a constant with an arbitrary type before treating \<^theory_text>\function_spec\\ function_spec swap (i::nat,j::nat) \ \TODO: the hovering on parameters produces a number of report equal to the number of \<^ML>\Proof_Context.add_fixes\ called in \<^ML>\Function_Specification_Parser.checkNsem_function_spec\\ -pre "\i < length A \ j < length A\" -post "\\res. length A = length(old A) \ res = ()\" -local_vars tmp :: int +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\ " + \ A := list_update A i (A ! j)\ ;- + \ A := list_update A j tmp\ " -text\The body --- heavily using the \\\-lifting cartouche --- corresponds to the low level +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 \) (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)" \ \check that \<^term>\i\ and \<^term>\j\ are pointing to the constants defined before treating \<^theory_text>\function_spec\\ 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 \<^verbatim>\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_state_state_scheme \ bool" where "swap'_pre \ \(i, j) \. i < length (A \) \ j < length (A \)" definition swap'_post :: "'a \ 'b \ 'c global_state_state_scheme \ 'd global_state_state_scheme \ unit \ bool" where "swap'_post \ \(i, j) \\<^sub>p\<^sub>r\<^sub>e \ res. length (A \) = length (A \\<^sub>p\<^sub>r\<^sub>e) \ res = ()" -text\The somewhat vacuous parameter \res\ for the result of the swap-computation is the conseqeuence +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" 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:\ (* Thus, the internal functionality in \local_vars\ is the construction of the two definitions *) definition push_local_swap_state' :: "(unit,'a local_swap'_state_scheme) MON\<^sub>S\<^sub>E" - where "push_local_swap_state' \ = + 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\<^sub>S\<^sub>E" - where "pop_local_swap_state' \ = - Some(hd(local_swap_state.result_value \), + where "pop_local_swap_state' \ = + Some(hd(local_swap_state.result_value \), \ \ recall : returns op value \ \ \ which happens to be unit \ \\local_swap_state.tmp:= tl( local_swap_state.tmp \) \)" definition swap'_core :: "nat \ nat \ (unit,'a local_swap'_state_scheme) MON\<^sub>S\<^sub>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) \)))))" + (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\<^sub>S\<^sub>E" where "swap' \ \(i,j). block\<^sub>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 + 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_state_state_scheme) MON\<^sub>S\<^sub>E" where "swap_opt \ \(i,j). (tmp \ yield\<^sub>C (\\. A \ ! i) ; - ((assign_global A_update (\\. list_update (A \) (i) (A \ ! j))) ;- - (assign_global A_update (\\. list_update (A \) (j) (tmp)))))" + ((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.\ *) section \Encoding \<^verbatim>\partition\ in Clean\ subsection \\<^verbatim>\partition\ in High-level Notation\ function_spec partition (lo::nat, hi::nat) returns nat -pre "\lo < length A \ hi < length A\" -post "\\res::nat. length A = length(old A) \ res = 3\" +pre "\lo < length A \ hi < length A\" +post "\\res::nat. length A = length(old A) \ res = 3\" local_vars pivot :: int i :: nat j :: nat defines " (\pivot := A ! hi \ ;- \i := lo \ ;- \j := lo \ ;- - (while\<^sub>C \j \ hi - 1 \ - do (if\<^sub>C \A ! j < pivot\ + (while\<^sub>C \j \ hi - 1 \ + do (if\<^sub>C \A ! j < pivot\ then call\<^sub>C swap \(i , j) \ ;- \i := i + 1 \ - else skip\<^sub>S\<^sub>E + else skip\<^sub>S\<^sub>E fi) ;- - \j := j + 1 \ + \j := j + 1 \ od) ;- call\<^sub>C swap \(i, j)\ ;- - return\<^sub>C result_value_update \i\ - ) " + return\<^sub>C result_value_update \i\ + ) " text\ The body is a fancy syntax for : @{cartouche [display=true] -\\defines " ((assign_local pivot_update (\\. A \ ! hi )) ;- +\\defines " ((assign_local pivot_update (\\. A \ ! hi )) ;- (assign_local i_update (\\. lo )) ;- - + (assign_local j_update (\\. lo )) ;- - (while\<^sub>C (\\. (hd o j) \ \ hi - 1 ) - do (if\<^sub>C (\\. A \ ! (hd o j) \ < (hd o pivot)\ ) + (while\<^sub>C (\\. (hd o j) \ \ hi - 1 ) + do (if\<^sub>C (\\. A \ ! (hd o j) \ < (hd o pivot)\ ) then call\<^sub>C (swap) (\\. ((hd o i) \, (hd o j) \)) ;- assign_local i_update (\\. ((hd o i) \) + 1) - else skip\<^sub>S\<^sub>E + else skip\<^sub>S\<^sub>E fi) ;- - (assign_local j_update (\\. ((hd o j) \) + 1)) + (assign_local j_update (\\. ((hd o j) \) + 1)) od) ;- call\<^sub>C (swap) (\\. ((hd o i) \, (hd o j) \)) ;- - assign_local result_value_update (\\. (hd o i) \) + assign_local result_value_update (\\. (hd o i) \) \ \ the meaning of the return stmt \ ) "\\}\ text\The effect of this statement is generation of the following definitions in the logical context:\ thm partition_pre_def thm partition_post_def thm push_local_partition_state_def thm pop_local_partition_state_def thm partition_core_def thm partition_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 \<^verbatim>\partition\ in elementary specification constructs:\ definition "partition'_pre \ \(lo, hi) \. lo < length (A \) \ hi < length (A \)" definition "partition'_post \ \(lo, hi) \\<^sub>p\<^sub>r\<^sub>e \ res. length (A \) = length (A \\<^sub>p\<^sub>r\<^sub>e) \ res = 3" text\Recall: list-lifting is automatic in \local_vars_test\:\ local_vars_test partition' "nat" pivot :: "int" i :: "nat" j :: "nat" -text\ ... which results in the internal definition of the respective push and pop operations +text\ ... which results in the internal definition of the respective push and pop operations for the @{term "partition'"} local variable space: \ thm push_local_partition'_state_def thm pop_local_partition'_state_def (* equivalent to *) definition push_local_partition_state' :: "(unit, 'a local_partition'_state_scheme) MON\<^sub>S\<^sub>E" where "push_local_partition_state' \ = Some((), - \\local_partition_state.pivot := undefined # local_partition_state.pivot \, - local_partition_state.i := undefined # local_partition_state.i \, - local_partition_state.j := undefined # local_partition_state.j \, - local_partition_state.result_value + \\local_partition_state.pivot := undefined # local_partition_state.pivot \, + local_partition_state.i := undefined # local_partition_state.i \, + local_partition_state.j := undefined # local_partition_state.j \, + local_partition_state.result_value := undefined # local_partition_state.result_value \ \)" -definition pop_local_partition_state' :: "(nat,'a local_partition_state_scheme) MON\<^sub>S\<^sub>E" +definition pop_local_partition_state' :: "(nat,'a local_partition_state_scheme) MON\<^sub>S\<^sub>E" where "pop_local_partition_state' \ = Some(hd(local_partition_state.result_value \), - \\local_partition_state.pivot := tl(local_partition_state.pivot \), - local_partition_state.i := tl(local_partition_state.i \), - local_partition_state.j := tl(local_partition_state.j \), - local_partition_state.result_value := + \\local_partition_state.pivot := tl(local_partition_state.pivot \), + local_partition_state.i := tl(local_partition_state.i \), + local_partition_state.j := tl(local_partition_state.j \), + local_partition_state.result_value := tl(local_partition_state.result_value \) \)" definition partition'_core :: "nat \ nat \ (unit,'a local_partition'_state_scheme) MON\<^sub>S\<^sub>E" where "partition'_core \ \(lo,hi). - ((assign_local pivot_update (\\. A \ ! hi )) ;- + ((assign_local pivot_update (\\. A \ ! hi )) ;- (assign_local i_update (\\. lo )) ;- - + (assign_local j_update (\\. lo )) ;- - (while\<^sub>C (\\. (hd o j) \ \ hi - 1 ) - do (if\<^sub>C (\\. A \ ! (hd o j) \ < (hd o pivot)\ ) + (while\<^sub>C (\\. (hd o j) \ \ hi - 1 ) + do (if\<^sub>C (\\. A \ ! (hd o j) \ < (hd o pivot)\ ) then call\<^sub>C (swap) (\\. ((hd o i) \, (hd o j) \)) ;- assign_local i_update (\\. ((hd o i) \) + 1) - else skip\<^sub>S\<^sub>E - fi) + else skip\<^sub>S\<^sub>E + fi) od) ;- (assign_local j_update (\\. ((hd o j) \) + 1)) ;- call\<^sub>C (swap) (\\. ((hd o i) \, (hd o j) \)) ;- - assign_local result_value_update (\\. (hd o i) \) + assign_local result_value_update (\\. (hd o i) \) \ \ the meaning of the return stmt \ )" thm partition_core_def (* a block manages the "dynamically" created fresh instances for the local variables of swap *) definition partition' :: "nat \ nat \ (nat,'a local_partition'_state_scheme) MON\<^sub>S\<^sub>E" - where "partition' \ \(lo,hi). block\<^sub>C push_local_partition_state - (partition_core (lo,hi)) + where "partition' \ \(lo,hi). block\<^sub>C push_local_partition_state + (partition_core (lo,hi)) pop_local_partition_state" - + section \Encoding the toplevel : \<^verbatim>\quicksort\ in Clean\ subsection \\<^verbatim>\quicksort\ in High-level Notation\ rec_function_spec quicksort (lo::nat, hi::nat) returns unit pre "\lo \ hi \ hi < length A\" post "\\res::unit. \i\{lo .. hi}. \j\{lo .. hi}. i \ j \ A!i \ A!j\" -variant "hi - lo" -local_vars p :: "nat" -defines " if\<^sub>C \lo < hi\ +variant "hi - lo" +local_vars p :: "nat" +defines " if\<^sub>C \lo < hi\ then (p\<^sub>t\<^sub>m\<^sub>p \ call\<^sub>C partition \(lo, hi)\ ; assign_local p_update (\\. p\<^sub>t\<^sub>m\<^sub>p)) ;- call\<^sub>C quicksort \(lo, p - 1)\ ;- - call\<^sub>C quicksort \(lo, p + 1)\ - else skip\<^sub>S\<^sub>E + call\<^sub>C quicksort \(lo, p + 1)\ + else skip\<^sub>S\<^sub>E fi" thm quicksort_core_def thm quicksort_def thm quicksort_pre_def thm quicksort_post_def subsection \A Similation of \<^verbatim>\quicksort\ in elementary specification constructs:\ -text\This is the most complex form a Clean function may have: it may be directly +text\This is the most complex form a Clean function may have: it may be directly recursive. Two subcases are to be distinguished: either a measure is provided or not.\ text\We start again with our simulation: First, we define the local variable \p\.\ local_vars_test quicksort' "unit" p :: "nat" ML\ val (x,y) = StateMgt_core.get_data_global @{theory}; \ thm pop_local_quicksort'_state_def thm push_local_quicksort'_state_def (* this implies the definitions : *) definition push_local_quicksort_state' :: "(unit, 'a local_quicksort'_state_scheme) MON\<^sub>S\<^sub>E" - where "push_local_quicksort_state' \ = + where "push_local_quicksort_state' \ = Some((), \\local_quicksort'_state.p := undefined # local_quicksort'_state.p \, local_quicksort'_state.result_value := undefined # local_quicksort'_state.result_value \ \)" definition pop_local_quicksort_state' :: "(unit,'a local_quicksort'_state_scheme) MON\<^sub>S\<^sub>E" where "pop_local_quicksort_state' \ = Some(hd(local_quicksort'_state.result_value \), - \\local_quicksort'_state.p := tl(local_quicksort'_state.p \), - local_quicksort'_state.result_value := + \\local_quicksort'_state.p := tl(local_quicksort'_state.p \), + local_quicksort'_state.result_value := tl(local_quicksort'_state.result_value \) \)" text\We recall the structure of the direct-recursive call in Clean syntax: @{cartouche [display=true] \ funct quicksort(lo::int, hi::int) returns unit pre "True" post "True" - local_vars p :: int + local_vars p :: int \if\<^sub>C\<^sub>L\<^sub>E\<^sub>A\<^sub>N \lo < hi\ then p := partition(lo, hi) ;- quicksort(lo, p - 1) ;- quicksort(p + 1, hi) else Skip\ \} \ definition quicksort'_pre :: "nat \ nat \ 'a local_quicksort'_state_scheme \ bool" where "quicksort'_pre \ \(i,j). \\. True " definition quicksort'_post :: "nat \ nat \ unit \ 'a local_quicksort'_state_scheme \ bool" - where "quicksort'_post \ \(i,j). \ res. \\. True" + where "quicksort'_post \ \(i,j). \ res. \\. True" definition quicksort'_core :: " (nat \ nat \ (unit,'a local_quicksort'_state_scheme) MON\<^sub>S\<^sub>E) \ (nat \ nat \ (unit,'a local_quicksort'_state_scheme) MON\<^sub>S\<^sub>E)" - where "quicksort'_core quicksort_rec \ \(lo, hi). - ((if\<^sub>C (\\. lo < hi ) + where "quicksort'_core quicksort_rec \ \(lo, hi). + ((if\<^sub>C (\\. lo < hi ) then (p\<^sub>t\<^sub>m\<^sub>p \ call\<^sub>C partition (\\. (lo, hi)) ; assign_local p_update (\\. p\<^sub>t\<^sub>m\<^sub>p)) ;- call\<^sub>C quicksort_rec (\\. (lo, (hd o p) \ - 1)) ;- - call\<^sub>C quicksort_rec (\\. ((hd o p) \ + 1, hi)) - else skip\<^sub>S\<^sub>E + call\<^sub>C quicksort_rec (\\. ((hd o p) \ + 1, hi)) + else skip\<^sub>S\<^sub>E fi))" term " ((quicksort'_core X) (lo,hi))" definition quicksort' :: " ((nat \ nat) \ (nat \ nat)) set \ (nat \ nat \ (unit,'a local_quicksort'_state_scheme) MON\<^sub>S\<^sub>E)" - where "quicksort' order \ wfrec order (\X. \(lo, hi). block\<^sub>C push_local_quicksort'_state - (quicksort'_core X (lo,hi)) + where "quicksort' order \ wfrec order (\X. \(lo, hi). block\<^sub>C push_local_quicksort'_state + (quicksort'_core X (lo,hi)) pop_local_quicksort'_state)" subsection\Setup for Deductive Verification\ -text\The coupling between the pre- and the post-condition state is done by the +text\The coupling between the pre- and the post-condition state is done by the free variable (serving as a kind of ghost-variable) @{term "\\<^sub>p\<^sub>r\<^sub>e"}. This coupling can also be used to express framing conditions; i.e. parts of the state which are independent and/or not affected by the computations to be verified. \ -lemma quicksort_correct : - "\\\. \exec_stop \ \ quicksort_pre (lo, hi)(\) \ \ = \\<^sub>p\<^sub>r\<^sub>e \ - quicksort (lo, hi) +lemma quicksort_correct : + "\\\. \exec_stop \ \ quicksort_pre (lo, hi)(\) \ \ = \\<^sub>p\<^sub>r\<^sub>e \ + quicksort (lo, hi) \\r \. \exec_stop \ \ quicksort_post(lo, hi)(\\<^sub>p\<^sub>r\<^sub>e)(\)(r) \" oops end diff --git a/thys/Clean/examples/SquareRoot_concept.thy b/thys/Clean/examples/SquareRoot_concept.thy --- a/thys/Clean/examples/SquareRoot_concept.thy +++ b/thys/Clean/examples/SquareRoot_concept.thy @@ -1,235 +1,235 @@ (****************************************************************************** * Clean * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) (* * SquareRoot_concept --- Example of monadic symbolic execution for a WHILE program. * Burkhart Wolff and Chantal Keller, LRI, Univ. Paris-Sud, France *) -section \ The Squareroot Example for Symbolic Execution \ +section \ The Squareroot Example for Symbolic Execution \ theory SquareRoot_concept - imports Clean_Main.Test_Clean + imports 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)\<^sup>2 > a \ a \ (res)\<^sup>2\" +pre "\0 \ a\" +post "\\res::int. (res + 1)\<^sup>2 > a \ a \ (res)\<^sup>2\" defines " (\tm := 1\ ;- \sqsum := 1\ ;- \i := 0\ ;- - (while\<^sub>S\<^sub>E \sqsum <= a\ do + (while\<^sub>S\<^sub>E \sqsum <= a\ do \i := i+1\ ;- \tm := tm + 2\ ;- \sqsum := tm + sqsum\ od) ;- - return\<^sub>C result_value_update \i\ - )" + return\<^sub>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} \ (* could also be local variable, we flipped a coin and it became this way *) 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} \ (* should be automatic *) 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 (* from trace: [1]Procedure "record" produced rewrite rule: - tm (?r\tm := ?k\) \ ?k + tm (?r\tm := ?k\) \ ?k Unfortunately, this lemma is not exported ... It looks as if it is computed on the fly ... This could explain why this is slow for our purposes ... *) 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 - + 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 "\ \ assign_global upd rhs ;- M \\ exec_stop \ \ 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 +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 \\<^sub>0" +lemma + assumes non_exec_stop[simp]: "\ exec_stop \\<^sub>0" and pos : "0 \ (a::int)" - and annotated_program: + and annotated_program: "\\<^sub>0 \ \tm := 1\ ;- \sqsum := 1\ ;- \i := 0\ ;- - (while\<^sub>S\<^sub>E \sqsum <= a\ do + (while\<^sub>S\<^sub>E \sqsum <= a\ do \i := i+1\ ;- \tm := tm + 2\ ;- \sqsum := tm + sqsum\ od) ;- assert\<^sub>S\<^sub>E(\\. \=\\<^sub>R)" shows "\\<^sub>R \assert\<^sub>S\<^sub>E \i\<^sup>2 \ a \ a < (i + 1)\<^sup>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 + 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 + the three test-cases for @{term "k<3"}. \ + defer 1 (* txt\Instead of testing, we @{emph \prove\} that the test cases satisfy the - post-condition for all @{term "k<3"} loop traversals and @{emph \all\} - positive inputs @{term "a "}.\ + post-condition for all @{term "k<3"} loop traversals and @{emph \all\} + positive inputs @{term "a "}.\ apply(auto simp: assert_simp) - *) + *) oops text\TODO: re-establish automatic test-coverage tactics of @{cite "DBLP:conf/tap/Keller18"}.\ end diff --git a/thys/Clean/src/Test_Clean.thy b/thys/Clean/src/Test_Clean.thy --- a/thys/Clean/src/Test_Clean.thy +++ b/thys/Clean/src/Test_Clean.thy @@ -1,49 +1,49 @@ (****************************************************************************** * Clean * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) theory Test_Clean imports Clean_Symbex - "~~/src/HOL/Eisbach/Eisbach" + "HOL-Eisbach.Eisbach" begin named_theorems memory_theory method memory_theory = (simp only: memory_theory MonadSE.bind_assoc') method norm = (auto dest!: assert_D) end