diff --git a/thys/Clean/ROOT b/thys/Clean/ROOT --- a/thys/Clean/ROOT +++ b/thys/Clean/ROOT @@ -1,59 +1,63 @@ -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] + options [timeout=300, document = pdf, document_output = "output"] sessions - "HOL-Eisbach" + "HOL-Eisbach" + "HOL-Computational_Algebra" directories "src" - "examples" + "examples" theories - "Clean_Main" - "Quicksort_concept" - "SquareRoot_concept" + "src/Clean_Main" + "examples/IsPrime" + "examples/LinearSearch" + "examples/Quicksort" + "examples/Quicksort_concept" + "examples/SquareRoot_concept" document_files "root.tex" "root.bib" "lstisadof.sty" + diff --git a/thys/Clean/document/root.tex b/thys/Clean/document/root.tex --- a/thys/Clean/document/root.tex +++ b/thys/Clean/document/root.tex @@ -1,110 +1,113 @@ \documentclass[fontsize=11pt,paper=a4,open=right,twoside,abstract=true]{scrreprt} \usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{lmodern} \usepackage[numbers, sort&compress, sectionbib]{natbib} \usepackage{isabelle,isabellesym} \usepackage[only,bigsqcap]{stmaryrd} \usepackage{ifthen} \usepackage{wrapfig} \usepackage{graphicx} \usepackage{xcolor} \usepackage{listings} \usepackage{lstisadof} \IfFileExists{railsetup.sty}{\usepackage{railsetup}}{} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % command \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]} % from 'iman.sty' \newcommand{\indexdef}[3]% {\ifthenelse{\equal{}{#1}}{\index{#3 (#2)|bold}}{\index{#3 (#1\ #2)|bold}}} % from 'isar.sty' -\newcommand{\isactrlC}{{\bf C}} %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % fix for package declaration to be at the end \usepackage[pdfpagelabels, pageanchor=false, plainpages=false]{hyperref} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % document \urlstyle{rm} \isabellestyle{it} \newcommand{\HOL}{HOL} \newcommand{\eg}{e.g.} \newcommand{\ie}{i.e.} \begin{document} \title{Clean - An Abstract Imperative Programming Language and its Theory} \author{% \href{https://www.lri.fr/~ftuong/}{Fr\'ed\'eric Tuong} \and \href{https://www.lri.fr/~wolff/}{Burkhart Wolff} \\ \and (with Contributions by \href{https://www.lri.fr/~keller/}{Chantal Keller})} \publishers{% \mbox{LRI, Univ. Paris-Sud, CNRS, Universit\'e Paris-Saclay} \\ b\^at. 650 Ada Lovelace, 91405 Orsay, France \texorpdfstring{\\}{} } \maketitle \begin{abstract} Clean is based on a simple, abstract execution model for an imperative target language. ``Abstract'' is understood as contrast to ``Concrete Semantics''; alternatively, the term ``shallow-style embedding'' could be used. It strives for a type-safe notation of program-variables, an incremental construction of the typed state-space, support of incremental verification, and open-world extensibility of new type definitions being intertwined with the program definitions. Clean is based on a ``no-frills'' state-exception monad with the usual definitions of \isa{bind} and \isa{unit} for the compositional glue of state-based computations. Clean offers conditionals and loops supporting C-like control-flow operators such as \isa{break} and \isa{return}. The state-space construction is based on the extensible record package. Direct recursion of procedures is supported. Clean's design strives for extreme simplicity. It is geared towards symbolic execution and proven correct verification tools. The underlying libraries of this package, however, deliberately restrict themselves to the most elementary infrastructure for these tasks. The package is intended to serve -as demonstrator semantic backend for Isabelle/C~\cite{TuongWolff19}, or for the test-generation -techniques described in~\cite{DBLP:conf/tap/Keller18}. +as demonstrator semantic backend for Isabelle/C~\cite{Tuong-IsabelleC:2019}, or for the +test-generation techniques described in~\cite{DBLP:conf/tap/Keller18}. \end{abstract} \newpage \tableofcontents \parindent 0pt\parskip 0.5ex %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % \input{session} \newpage \input{Clean.tex} - \input{Quicksort_concept.tex} +\input{Quicksort.tex} \input{SquareRoot_concept.tex} +\input{IsPrime.tex} +\input{LinearSearch.tex} \newpage \chapter{Appendix : Used Monad Libraries} \input{MonadSE.tex} \input{Seq_MonadSE.tex} \input{Symbex_MonadSE.tex} \input{Clean_Symbex.tex} \input{Test_Clean.tex} \input{Hoare_MonadSE.tex} \input{Hoare_Clean.tex} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \bibliographystyle{abbrvnat} \bibliography{root} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/Clean/examples/IsPrime.thy b/thys/Clean/examples/IsPrime.thy new file mode 100644 --- /dev/null +++ b/thys/Clean/examples/IsPrime.thy @@ -0,0 +1,109 @@ +(****************************************************************************** + * 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. + ******************************************************************************) + +(* + * IsPrime-Test + * + * Authors : Burkhart Wolff, Frédéric Tuong + *) + +chapter \ Clean Semantics : Another Clean Example\ + + +theory IsPrime + imports Clean.Clean + Clean.Hoare_Clean + Clean.Clean_Symbex + "HOL-Computational_Algebra.Primes" +begin + +section\The Primality-Test Example at a Glance\ + +definition "SQRT_UINT_MAX = (65536::nat)" +definition "UINT_MAX = (2^32::nat) - 1" + + +function_spec isPrime(n :: nat) returns bool +pre "\n \ SQRT_UINT_MAX\" +post "\\res. res \ prime n \" +local_vars i :: nat +defines " if\<^sub>C \n < 2\ + then return\<^bsub>local_isPrime_state.result_value_update\<^esub> \False\ + else skip\<^sub>S\<^sub>E + fi ;- + \i := 2\ ;- + while\<^sub>C \i < SQRT_UINT_MAX \ i*i \ n \ + do if\<^sub>C \n mod i = 0\ + then return\<^bsub>local_isPrime_state.result_value_update\<^esub> \False\ + else skip\<^sub>S\<^sub>E + fi ;- + \i := i + 1 \ + od ;- + return\<^bsub>local_isPrime_state.result_value_update\<^esub> \True\" + +find_theorems name:isPrime name:core + +lemma XXX : +"isPrime_core n \ + if\<^sub>C (\\. n < 2) then (return\<^bsub>result_value_update\<^esub> (\\. False)) + else skip\<^sub>S\<^sub>E fi;- + i_update :==\<^sub>L (\\. 2) ;- + while\<^sub>C (\\. (hd\i)\ < SQRT_UINT_MAX \ (hd\i)\ * (hd\i)\ \ n) + do + (if\<^sub>C (\\. n mod (hd \ i) \ = 0) + then (return\<^bsub>result_value_update\<^esub> (\\. False)) + else skip\<^sub>S\<^sub>E fi ;- + i_update :==\<^sub>L (\\. (hd \ i) \ + 1)) + od ;- + return\<^bsub>result_value_update\<^esub> (\\. True)" + + by(simp add: isPrime_core_def) + +lemma YYY: +"isPrime n \ block\<^sub>C push_local_isPrime_state + (isPrime_core n) + pop_local_isPrime_state" + by(simp add: isPrime_def) + +lemma isPrime_correct : + "\\\. \ \ \ isPrime_pre (n)(\) \ \ = \\<^sub>p\<^sub>r\<^sub>e \ + isPrime n + \\r \. \ \ \ isPrime_post(n) (\\<^sub>p\<^sub>r\<^sub>e)(\)(r) \" + oops + + + +end diff --git a/thys/Clean/examples/LinearSearch.thy b/thys/Clean/examples/LinearSearch.thy new file mode 100644 --- /dev/null +++ b/thys/Clean/examples/LinearSearch.thy @@ -0,0 +1,105 @@ +(****************************************************************************** + * 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. + ******************************************************************************) + +(* + * Authors : Burkhart Wolff, Frédéric Tuong + *) + +chapter \ A Clean Semantics Example : Linear Search\ + +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 LinearSearch + imports Clean.Clean + Clean.Hoare_MonadSE +begin + + +section\The LinearSearch Example\ + +definition bool2int where "bool2int x = (if x then 1::int else 0)" + +global_vars state + t :: "int list" + +function_spec linearsearch (x::int, n::int) returns int +pre "\ 0 \ n \ n < int(length t) \ sorted t\" +post "\\res::int. res = bool2int (\ i \ {0 ..< length t}. t!i = x) \" +local_vars i :: int +defines " \i := 0 \ ;- + while\<^sub>C \i < n \ + do if\<^sub>C \t ! (nat i) < x\ + then \i := i + 1 \ + else return\<^sub>C result_value_update \bool2int(t!(nat i) = x)\ + fi + od " + +(* +C\ +/*@ requires "n >= 0" + requires "valid(t+(0..n-1))" + requires "(forall integer i,j; 0<=i<=j t[i] <= t[j])" + ensures "exists integer i; (0<=i result == 1" + ensures "(forall integer i; 0<=i t[i] != x) <==> result == 0" + assigns nothing + */ + +int linearsearch(int x, int t[], int n) { + int i = 0; + + /*@ loop invariant "0<=i<=n" + loop invariant "forall integer j; 0<=j (t[j] != x)" + loop assigns i + loop variant "n-i" + */ + while (i < n) { + if (t[i] < x) { + i++; + } else { + return (t[i] == x); + } + } + + return 0; +} +\ + +*) + +end \ No newline at end of file diff --git a/thys/Clean/examples/Quicksort.thy b/thys/Clean/examples/Quicksort.thy new file mode 100644 --- /dev/null +++ b/thys/Clean/examples/Quicksort.thy @@ -0,0 +1,150 @@ +(****************************************************************************** + * 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 : all at a glance. + * + * 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 + imports Clean.Clean + Clean.Hoare_Clean + Clean.Clean_Symbex +begin + +section\The Quicksort Example - At a Glance\ + +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} +\ + + +section\Clean Encoding of the Global State of Quicksort\ + + +global_vars state + A :: "int list" + +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 +defines " \ tmp := A ! i\ ;- + \ A := list_update A i (A ! j)\ ;- + \ A := list_update A j tmp\ " + + +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\" +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\ + then call\<^sub>C swap \(i , j) \ ;- + \i := i + 1 \ + else skip\<^sub>S\<^sub>E + fi ;- + \j := j + 1 \ + od;- + call\<^sub>C swap \(i, j)\ ;- + return\<^bsub>local_partition_state.result_value_update\<^esub> \i\" + +thm partition_core_def + + +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\ + 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 + fi" + + +thm quicksort_core_def +thm quicksort_def +thm quicksort_pre_def +thm quicksort_post_def + +section\Possible Application Sketch\ + +lemma quicksort_correct : + "\\\. \ \ \ quicksort_pre (lo, hi)(\) \ \ = \\<^sub>p\<^sub>r\<^sub>e \ + quicksort (lo, hi) + \\r \. \ \ \ quicksort_post(lo, hi)(\\<^sub>p\<^sub>r\<^sub>e)(\)(r) \" + oops + + + +end 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,531 @@ (****************************************************************************** * 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 - Hoare_MonadSE + 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 +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" +find_theorems create\<^sub>L name:"Quick" + 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.\ +subsubsection\A Simulation of Synthesis of Typed Assignment-Rules\ +definition A\<^sub>L' where "A\<^sub>L' \ create\<^sub>L global_state_state.A global_state_state.A_update" + +lemma A\<^sub>L'_control_indep : "(break_status\<^sub>L \ A\<^sub>L' \ return_status\<^sub>L \ A\<^sub>L')" + unfolding A\<^sub>L'_def break_status\<^sub>L_def return_status\<^sub>L_def create\<^sub>L_def upd2put_def + by (simp add: lens_indep_def) + +lemma A\<^sub>L'_strong_indep : "\! A\<^sub>L'" + unfolding strong_control_independence_def + using A\<^sub>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 :==\<^sub>G rhs \\r \. \ \ \ P \ \" + apply(rule assign_global) + apply(rule strong_vs_weak_upd [of global_state_state.A global_state_state.A_update]) + apply (metis A\<^sub>L'_def A\<^sub>L'_strong_indep) + by(rule ext, rule ext, auto) + 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 -term: \ +value "\break_status = False, return_status = False, A = [1,2,3], + tmp = [], result_value = [], \ = X\" + +value "swap (0,1) \break_status = False, return_status = False, A = [1,2,3], + 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) \))))"\\}\ + (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 \)" + 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 + 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 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:\ (* 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' \ = - Some((),\\local_swap_state.tmp := undefined # local_swap_state.tmp \ \)" + 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) \)))))" + 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\<^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.\ -*) + +text\A more pretty-printed term representation is:\ +term\ swap_opt = (\(i, j). + tmp \ (yield\<^sub>C (\\. A \ ! i)); + (A_update :==\<^sub>G (\\. (A \)[i := A \ ! j]) ;- + A_update :==\<^sub>G (\\. (A \)[j := tmp])))\ + + +subsubsection\A Simulation of Synthesis of Typed Assignment-Rules\ + +definition tmp\<^sub>L + where "tmp\<^sub>L \ create\<^sub>L local_swap'_state.tmp local_swap'_state.tmp_update" + +lemma tmp\<^sub>L_control_indep : "(break_status\<^sub>L \ tmp\<^sub>L \ return_status\<^sub>L \ tmp\<^sub>L)" + unfolding tmp\<^sub>L_def break_status\<^sub>L_def return_status\<^sub>L_def create\<^sub>L_def upd2put_def + by (simp add: lens_indep_def) + +lemma tmp\<^sub>L_strong_indep : "\! tmp\<^sub>L" + unfolding strong_control_independence_def + using tmp\<^sub>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 :==\<^sub>L rhs + \\r \. \ \ \ P \ \" + apply(rule assign_local) + apply(rule strong_vs_weak_upd_list) + apply(rule tmp\<^sub>L_strong_indep[simplified tmp\<^sub>L_def]) + by(rule ext, rule ext, auto) + 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\ +defines " \pivot := A ! hi \ ;- \i := lo \ ;- \j := lo \ ;- + (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:\ +subsubsection \Contract-Elements\ 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" + +subsubsection\Memory-Model\ 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 \) \)" +subsubsection\Memory-Model\ +text\Independence of Control-Block:\ + + +subsubsection\Monadic Representation of the Body\ 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) - \\r \. \exec_stop \ \ quicksort_post(lo, hi)(\\<^sub>p\<^sub>r\<^sub>e)(\)(r) \" +lemma quicksort_correct : + "\\\. \ \ \ quicksort_pre (lo, hi)(\) \ \ = \\<^sub>p\<^sub>r\<^sub>e \ + quicksort (lo, hi) + \\r \. \ \ \ 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 Test_Clean + 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)\<^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" + shows "\ \ upd :==\<^sub>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 +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/Clean.thy b/thys/Clean/src/Clean.thy --- a/thys/Clean/src/Clean.thy +++ b/thys/Clean/src/Clean.thy @@ -1,1084 +1,1425 @@ (****************************************************************************** * 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. - * Burkhart Wolff, Frédéric Tuong and Chantal Keller, LRI, Univ. Paris-Saclay, France + * Burkhart Wolff and Frédéric Tuong, LRI, Univ. Paris-Saclay, France *) chapter \The Clean Language\ theory Clean - imports Symbex_MonadSE + imports Optics Symbex_MonadSE keywords "global_vars" "local_vars_test" :: thy_decl and "returns" "pre" "post" "local_vars" "variant" and "function_spec" :: thy_decl and "rec_function_spec" :: thy_decl begin text\Clean (pronounced as: ``C lean'' or ``Céline'' [selin]) is a minimalistic imperative language with C-like control-flow operators based on a shallow embedding into the ``State Exception Monads'' theory formalized in \<^file>\MonadSE.thy\. It strives for a type-safe notation of program-variables, an incremental construction of the typed state-space in order to facilitate incremental verification and open-world extensibility to new type definitions intertwined with the program definition. It comprises: \begin{itemize} \item C-like control flow with \<^term>\break\ and \<^term>\return\, \item global variables, \item function calls (seen as monadic executions) with side-effects, recursion and local variables, \item parameters are modeled via functional abstractions (functions are monads); a passing of parameters to local variables might be added later, \item direct recursive function calls, \item cartouche syntax for \\\-lifted update operations supporting global and local variables. \end{itemize} Note that Clean in its current version is restricted to \<^emph>\monomorphic\ global and local variables as well as function parameters. This limitation will be overcome at a later stage. The construction in itself, however, is deeply based on parametric polymorphism (enabling structured proofs over extensible records as used in languages of the ML family \<^url>\http://www.cs.ioc.ee/tfp-icfp-gpce05/tfp-proc/21num.pdf\ and Haskell \<^url>\https://www.schoolofhaskell.com/user/fumieval/extensible-records\). \ (*<*) text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ (*>*) section\A High-level Description of the Clean Memory Model\ subsection\A Simple Typed Memory Model of Clean: An Introduction \ text\ Clean is based on a ``no-frills'' state-exception monad \<^theory_text>\type_synonym ('o, '\) MON\<^sub>S\<^sub>E = \'\ \ ('o \ '\)\\ with the usual definitions of \<^term>\bind\ and \<^term>\unit\. In this language, sequence operators, conditionals and loops can be integrated. \ text\From a concrete program, the underlying state \<^theory_text>\'\\ is \<^emph>\incrementally\ constructed by a sequence of extensible record definitions: \<^enum> Initially, an internal control state is defined to give semantics to \<^term>\break\ and \<^term>\return\ statements: \begin{isar} record control_state = break_val :: bool return_val :: bool \end{isar} \<^theory_text>\control_state\ represents the $\sigma_0$ state. \<^enum> Any global variable definition block with definitions $a_1 : \tau_1$ $\dots$ $a_n : \tau_n$ is translated into a record extension: \begin{isar} record \$_{n+1}$ = \$_n$ + a$_1$ :: $\tau_1$; ...; $a_n$ :: $\tau_n$ \end{isar} \<^enum> Any local variable definition block (as part of a procedure declaration) with definitions $a_1 : \tau_1$ $\dots$ $a_n : \tau_n$ is translated into the record extension: \begin{isar} record \$_{n+1}$ = \$_n$ + a$_1$ :: $\tau_1$ list; ...; $a_n$ :: $\tau_n$ list; result :: $\tau_{result-type}$ list; \end{isar} where the \<^typ>\_ list\-lifting is used to model a \<^emph>\stack\ of local variable instances in case of direct recursions and the \<^term>\result_value\ used for the value of the \<^term>\return\ statement.\ text \ The \<^theory_text>\record\ package creates an \<^theory_text>\'\\ extensible record type \<^theory_text>\'\ control_state_ext\ where the \<^theory_text>\'\\ stands for extensions that are subsequently ``stuffed'' in them. Furthermore, it generates definitions for the constructor, accessor and update functions and automatically derives a number of theorems over them (e.g., ``updates on different fields commute'', ``accessors on a record are surjective'', ``accessors yield the value of the last update''). The collection of these theorems constitutes the \<^emph>\memory model\ of Clean, providing an incrementally extensible state-space for global and local program variables. In contrast to axiomatizations of memory models, our generated state-spaces might be ``wrong'' in the sense that they do not reflect the operational behaviour of a particular compiler or a sufficiently large portion of the C language; however, it is by construction \<^emph>\logically consistent\ since it is impossible to derive falsity from the entire set of conservative extension schemes used in their construction. A particular advantage of the incremental state-space construction is that it supports incremental verification and interleaving of program definitions with theory development.\ subsection\ Formally Modeling Control-States \ text\The control state is the ``root'' of all extensions for local and global variable spaces in Clean. It contains just the information of the current control-flow: a \<^term>\break\ occurred (meaning all commands till the end of the control block will be skipped) or a \<^term>\return\ occurred (meaning all commands till the end of the current function body will be skipped).\ record control_state = break_status :: bool return_status :: bool +(* ML level representation: *) +ML\ val t = @{term "\ \ break_status := False \"}\ + (* break quits innermost while or for, return quits an entire execution sequence. *) definition break :: "(unit, ('\_ext) control_state_ext) MON\<^sub>S\<^sub>E" where "break \ (\ \. Some((), \ \ break_status := True \))" definition unset_break_status :: "(unit, ('\_ext) control_state_ext) MON\<^sub>S\<^sub>E" where "unset_break_status \ (\ \. Some((), \ \ break_status := False \))" definition set_return_status :: " (unit, ('\_ext) control_state_ext) MON\<^sub>S\<^sub>E" where "set_return_status = (\ \. Some((), \ \ return_status := True \))" definition unset_return_status :: "(unit, ('\_ext) control_state_ext) MON\<^sub>S\<^sub>E" where "unset_return_status = (\ \. Some((), \ \ return_status := False \))" definition exec_stop :: "('\_ext) control_state_ext \ bool" where "exec_stop = (\ \. break_status \ \ return_status \ )" + +abbreviation normal_execution :: "('\_ext) control_state_ext \ bool" + where "(normal_execution s) \ (\ exec_stop s)" +notation normal_execution ("\") + + lemma exec_stop1[simp] : "break_status \ \ exec_stop \" unfolding exec_stop_def by simp lemma exec_stop2[simp] : "return_status \ \ exec_stop \" unfolding exec_stop_def by simp text\ On the basis of the control-state, assignments, conditionals and loops are reformulated into \<^term>\break\-aware and \<^term>\return\-aware versions as shown in the definitions of \<^term>\assign\ and \<^term>\if_C\ (in this theory file, see below). \ text\For Reasoning over Clean programs, we need the notion of independance of an update from the control-block: \ +definition break_status\<^sub>L + where "break_status\<^sub>L = create\<^sub>L control_state.break_status control_state.break_status_update" +lemma "vwb_lens break_status\<^sub>L" + unfolding break_status\<^sub>L_def + by (simp add: vwb_lens_def create\<^sub>L_def wb_lens_def mwb_lens_def + mwb_lens_axioms_def upd2put_def wb_lens_axioms_def weak_lens_def) + + + +definition return_status\<^sub>L + where "return_status\<^sub>L = create\<^sub>L control_state.return_status control_state.return_status_update" +lemma "vwb_lens return_status\<^sub>L" + unfolding return_status\<^sub>L_def + by (simp add: vwb_lens_def create\<^sub>L_def wb_lens_def mwb_lens_def + mwb_lens_axioms_def upd2put_def wb_lens_axioms_def weak_lens_def) + +lemma break_return_indep : "break_status\<^sub>L \ return_status\<^sub>L " + by (simp add: break_status\<^sub>L_def lens_indepI return_status\<^sub>L_def upd2put_def create\<^sub>L_def) + +definition strong_control_independence ("\!") + where "\! L = (break_status\<^sub>L \ L \ return_status\<^sub>L \ L)" + +lemma "vwb_lens break_status\<^sub>L" + unfolding vwb_lens_def break_status\<^sub>L_def create\<^sub>L_def wb_lens_def mwb_lens_def + by (simp add: mwb_lens_axioms_def upd2put_def wb_lens_axioms_def weak_lens_def) + + definition control_independence :: "(('b\'b)\'a control_state_scheme \ 'a control_state_scheme) \ bool" ("\") where "\ upd \ (\\ T b. break_status (upd T \) = break_status \ \ return_status (upd T \) = return_status \ \ upd T (\\ return_status := b \) = (upd T \)\ return_status := b \ \ upd T (\\ break_status := b \) = (upd T \)\ break_status := b \) " +lemma strong_vs_weak_ci : "\! L \ \ (\f. \\. lens_put L \ (f (lens_get L \)))" + unfolding strong_control_independence_def control_independence_def + by (simp add: break_status\<^sub>L_def lens_indep_def return_status\<^sub>L_def upd2put_def create\<^sub>L_def) + +lemma expimnt :"\! (create\<^sub>L getv updv) \ (\f \. updv (\_. f (getv \)) \) = updv" + unfolding create\<^sub>L_def strong_control_independence_def + break_status\<^sub>L_def return_status\<^sub>L_def lens_indep_def + apply(rule ext, rule ext) + apply auto + unfolding upd2put_def + (* seems to be independent *) + oops + +lemma expimnt : + "vwb_lens (create\<^sub>L getv updv) \ (\f \. updv (\_. f (getv \)) \) = updv" + unfolding create\<^sub>L_def strong_control_independence_def lens_indep_def + break_status\<^sub>L_def return_status\<^sub>L_def vwb_lens_def + apply(rule ext, rule ext) + apply auto + unfolding upd2put_def wb_lens_def weak_lens_def wb_lens_axioms_def mwb_lens_def + mwb_lens_axioms_def + apply auto + (* seems to be independent *) + oops + +lemma strong_vs_weak_upd : + assumes * : "\! (create\<^sub>L getv updv)" (* getv and upd are constructed as lense *) + and ** : "(\f \. updv (\_. f (getv \)) \) = updv" (* getv and upd are involutive *) + shows "\ (updv)" + apply(insert * **) + unfolding create\<^sub>L_def upd2put_def + by(drule strong_vs_weak_ci, auto) + + +text\This quite tricky proof establishes the fact that the special case + \hd(getv \) = []\ for \getv \ = []\ is finally irrelevant in our setting. + This implies that we don't need the list-lense-construction (so far).\ +lemma strong_vs_weak_upd_list : + assumes * : "\! (create\<^sub>L (getv:: 'b control_state_scheme \ 'c list) + (updv:: ('c list \ 'c list) \ 'b control_state_scheme \ 'b control_state_scheme))" + (* getv and upd are constructed as lense *) + and ** : "(\f \. updv (\_. f (getv \)) \) = updv" (* getv and upd are involutive *) + shows "\ (updv \ upd_hd)" +proof - + have *** : "\! (create\<^sub>L (hd \ getv ) (updv \ upd_hd))" + using * ** by (simp add: indep_list_lift strong_control_independence_def) + show "\ (updv \ upd_hd)" + apply(rule strong_vs_weak_upd) + apply(rule ***) + apply(rule ext, rule ext, simp) + apply(subst (2) **[symmetric]) + proof - + fix f:: "'c \ 'c" fix \ :: "'b control_state_scheme" + show "updv (upd_hd (\_. f (hd (getv \)))) \ = updv (\_. upd_hd f (getv \)) \" + proof (cases "getv \") + case Nil + then show ?thesis + by (simp,metis (no_types) "**" upd_hd.simps(1)) + next + case (Cons a list) + then show ?thesis + proof - + have "(\c. f (hd (getv \))) = ((\c. f a)::'c \ 'c)" + using local.Cons by auto + then show ?thesis + by (metis (no_types) "**" local.Cons upd_hd.simps(2)) + qed + qed + qed +qed lemma exec_stop_vs_control_independence [simp]: "\ upd \ exec_stop (upd f \) = exec_stop \" unfolding control_independence_def exec_stop_def by simp - lemma exec_stop_vs_control_independence' [simp]: "\ upd \ (upd f (\ \ return_status := b \)) = (upd f \)\ return_status := b \" unfolding control_independence_def exec_stop_def by simp lemma exec_stop_vs_control_independence'' [simp]: "\ upd \ (upd f (\ \ break_status := b \)) = (upd f \) \ break_status := b \" unfolding control_independence_def exec_stop_def by simp subsection\An Example for Global Variable Declarations.\ text\We present the above definition of the incremental construction of the state-space in more detail via an example construction. Consider a global variable \A\ representing an array of integer. This \<^emph>\global variable declaration\ corresponds to the effect of the following record declaration: \<^theory_text>\record state0 = control_state + A :: "int list"\ which is later extended by another global variable, say, \B\ representing a real described in the Cauchy Sequence form @{typ "nat \ (int \ int)"} as follows: \<^theory_text>\record state1 = state0 + B :: "nat \ (int \ int)"\. A further extension would be needed if a (potentially recursive) function \f\ with some local variable \tmp\ is defined: \<^theory_text>\record state2 = state1 + tmp :: "nat stack" result_value :: "nat stack" \, where the \stack\ needed for modeling recursive instances is just a synonym for \list\. \ subsection\ The Assignment Operations (embedded in State-Exception Monad) \ text\Based on the global variable states, we define \<^term>\break\-aware and \<^term>\return\-aware version of the assignment. The trick to do this in a generic \<^emph>\and\ type-safe way is to provide the generated accessor and update functions (the ``lens'' representing this global variable, cf. @{cite "Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and "DBLP:conf/ictac/FosterZW16"}) to the generic assign operators. This pair of accessor and update carries all relevant semantic and type information of this particular variable and \<^emph>\characterizes\ this variable semantically. Specific syntactic support~\<^footnote>\via the Isabelle concept of cartouche: \<^url>\https://isabelle.in.tum.de/doc/isar-ref.pdf\\ will hide away the syntactic overhead and permit a human-readable form of assignments or expressions accessing the underlying state. \ consts syntax_assign :: "('\ \ int) \ int \ term" (infix ":=" 60) -definition assign :: "(('\_ext) control_state_scheme \ +definition assign :: "(('\_ext) control_state_scheme \ ('\_ext) control_state_scheme) \ (unit,('\_ext) control_state_scheme)MON\<^sub>S\<^sub>E" - where "assign f = (\\. if exec_stop \ then Some((), \) else Some((), f \))" + where "assign f = (\\. if exec_stop \ then Some((), \) else Some((), f \))" definition assign_global :: "(('a \ 'a ) \ '\_ext control_state_scheme \ '\_ext control_state_scheme) \ ('\_ext control_state_scheme \ 'a) - \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" + \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" (infix ":==\<^sub>G" 100) where "assign_global upd rhs = assign(\\. ((upd) (\_. rhs \)) \)" text\An update of the variable \A\ based on the state of the previous example is done by @{term [source = true] \assign_global A_upd (\\. list_update (A \) (i) (A \ ! j))\} representing \A[i] = A[j]\; arbitrary nested updates can be constructed accordingly.\ text\Local variable spaces work analogously; except that they are represented by a stack in order to support individual instances in case of function recursion. This requires automated generation of specific push- and pop operations used to model the effect of entering or leaving a function block (to be discussed later).\ -fun map_hd :: "('a \ 'a) \ 'a list \ 'a list" - where "map_hd f [] = []" - | "map_hd f (a#S) = f a # S" - -lemma tl_map_hd [simp] :"tl (map_hd f S) = tl S" by (metis list.sel(3) map_hd.elims) - -definition "map_nth = (\i f l. list_update l i (f (l ! i)))" - definition assign_local :: "(('a list \ 'a list) \ '\_ext control_state_scheme \ '\_ext control_state_scheme) \ ('\_ext control_state_scheme \ 'a) - \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" - where "assign_local upd rhs = assign(\\. ((upd o map_hd) (%_. rhs \)) \)" + \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" (infix ":==\<^sub>L" 100) + where "assign_local upd rhs = assign(\\. ((upd o upd_hd) (%_. rhs \)) \)" text\Semantically, the difference between \<^emph>\global\ and \<^emph>\local\ is rather unimpressive as the following lemma shows. However, the distinction matters for the pretty-printing setup of Clean.\ -lemma "assign_local upd rhs = assign_global (upd o map_hd) rhs " +lemma "(upd :==\<^sub>L rhs) = ((upd \ upd_hd) :==\<^sub>G rhs)" unfolding assign_local_def assign_global_def by simp text\The \return\ command in C-like languages is represented basically by an assignment to a local variable \result_value\ (see below in the Clean-package generation), plus some setup of \<^term>\return_status\. Note that a \<^term>\return\ may appear after a \<^term>\break\ and should have no effect in this case.\ +definition return\<^sub>C0 + where "return\<^sub>C0 A = (\\. if exec_stop \ then Some((), \) + else (A ;- set_return_status) \)" + definition return\<^sub>C :: "(('a list \ 'a list) \ '\_ext control_state_scheme \ '\_ext control_state_scheme) \ ('\_ext control_state_scheme \ 'a) - \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" - where "return\<^sub>C upd rhs =(\\. if exec_stop \ then Some((), \) - else (assign_local upd rhs ;- set_return_status) \)" + \ (unit,'\_ext control_state_scheme) MON\<^sub>S\<^sub>E" ("return\") + where "return\<^sub>C upd rhs = return\<^sub>C0 (assign_local upd rhs)" + subsection\Example for a Local Variable Space\ text\Consider the usual operation \swap\ defined in some free-style syntax as follows: @{cartouche [display] \ function_spec swap (i::nat,j::nat) local_vars tmp :: int defines " \ tmp := A ! i\ ;- \ A[i] := A ! j\ ;- \ A[j] := tmp\ "\} \ text\ For the fantasy syntax \tmp := A ! i\, we can construct the following semantic code: @{term [source = true] \assign_local tmp_update (\\. (A \) ! i )\} where \tmp_update\ is the update operation generated by the \<^theory_text>\record\-package, which is generated while treating local variables of \swap\. By the way, a stack for \return\-values is also generated in order to give semantics to a \return\ operation: it is syntactically equivalent to the assignment of the result variable in the local state (stack). It sets the \<^term>\return_val\ flag. The management of the local state space requires function-specific \push\ and \pop\ operations, for which suitable definitions are generated as well: @{cartouche [display] \definition push_local_swap_state :: "(unit,'a local_swap_state_scheme) MON\<^sub>S\<^sub>E" where "push_local_swap_state \ = Some((),\\local_swap_state.tmp := undefined # local_swap_state.tmp \, local_swap_state.result_value := undefined # local_swap_state.result_value \ \)" 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 \), \\local_swap_state.tmp:= tl( local_swap_state.tmp \) \)"\} where \result_value\ is the stack for potential result values (not needed in the concrete example \swap\). \ section\ Global and Local State Management via Extensible Records \ text\In the sequel, we present the automation of the state-management as schematically discussed in the previous section; the declarations of global and local variable blocks are constructed by subsequent extensions of @{typ "'a control_state_scheme"}, defined above.\ ML\ structure StateMgt_core = struct val control_stateT = Syntax.parse_typ @{context} "control_state" val control_stateS = @{typ "('a)control_state_scheme"}; fun optionT t = Type(@{type_name "Option.option"},[t]); fun MON_SE_T res state = state --> optionT(HOLogic.mk_prodT(res,state)); fun merge_control_stateS (@{typ "('a)control_state_scheme"},t) = t |merge_control_stateS (t, @{typ "('a)control_state_scheme"}) = t |merge_control_stateS (t, t') = if (t = t') then t else error"can not merge Clean state" datatype var_kind = global_var of typ | local_var of typ fun type_of(global_var t) = t | type_of(local_var t) = t type state_field_tab = var_kind Symtab.table structure Data = Generic_Data ( type T = (state_field_tab * typ (* current extensible record *)) val empty = (Symtab.empty,control_stateS) val extend = I fun merge((s1,t1),(s2,t2)) = (Symtab.merge (op =)(s1,s2),merge_control_stateS(t1,t2)) ); - val get_data = Data.get o Context.Proof; val map_data = Data.map; val get_data_global = Data.get o Context.Theory; val map_data_global = Context.theory_map o map_data; val get_state_type = snd o get_data val get_state_type_global = snd o get_data_global val get_state_field_tab = fst o get_data val get_state_field_tab_global = fst o get_data_global fun upd_state_type f = map_data (fn (tab,t) => (tab, f t)) fun upd_state_type_global f = map_data_global (fn (tab,t) => (tab, f t)) fun fetch_state_field (ln,X) = let val a::b:: _ = rev (Long_Name.explode ln) in ((b,a),X) end; fun filter_name name ln = let val ((a,b),X) = fetch_state_field ln in if a = name then SOME((a,b),X) else NONE end; fun filter_attr_of name thy = let val tabs = get_state_field_tab_global thy in map_filter (filter_name name) (Symtab.dest tabs) end; fun is_program_variable name thy = Symtab.defined((fst o get_data_global) thy) name fun is_global_program_variable name thy = case Symtab.lookup((fst o get_data_global) thy) name of SOME(global_var _) => true | _ => false fun is_local_program_variable name thy = case Symtab.lookup((fst o get_data_global) thy) name of SOME(local_var _) => true | _ => false fun declare_state_variable_global f field thy = let val Const(name,ty) = Syntax.read_term_global thy field in (map_data_global (apfst (Symtab.update_new(name,f ty))) (thy) handle Symtab.DUP _ => error("multiple declaration of global var")) end; fun declare_state_variable_local f field ctxt = let val Const(name,ty) = Syntax.read_term_global (Context.theory_of ctxt) field in (map_data (apfst (Symtab.update_new(name,f ty)))(ctxt) handle Symtab.DUP _ => error("multiple declaration of global var")) end; end\ subsection\Block-Structures\ text\ On the managed local state-spaces, it is now straight-forward to define the semantics for a \block\ representing the necessary management of local variable instances: \ definition block\<^sub>C :: " (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "block\<^sub>C push core pop \ ( \ \assumes break and return unset \ push ;- \ \create new instances of local variables \ core ;- \ \execute the body \ unset_break_status ;- \ \unset a potential break \ unset_return_status;- \ \unset a potential return break \ (x \ pop; \ \restore previous local var instances \ unit\<^sub>S\<^sub>E(x)))" \ \yield the return value \ text\ Based on this definition, the running \swap\ example is represented as follows: @{cartouche [display] \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) \)))))" 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" \} \ subsection\Call Semantics\ text\It is now straight-forward to define the semantics of a generic call --- -which is simply a monad execution that is \<^term>\break\-aware and \<^term>\return\-aware.\ +which is simply a monad execution that is \<^term>\break\-aware and \<^term>\return\<^bsub>upd\<^esub>\-aware.\ definition call\<^sub>C :: "( '\ \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E) \ ((('\_ext) control_state_ext) \ '\) \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call\<^sub>C M A\<^sub>1 = (\\. if exec_stop \ then Some(undefined, \) else M (A\<^sub>1 \) \)" text\Note that this presentation assumes a uncurried format of the arguments. The question arises if this is the right approach to handle calls of operation with multiple arguments. Is it better to go for an some appropriate currying principle? Here are some more experimental variants for curried operations... \ definition call_0\<^sub>C :: "('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_0\<^sub>C M = (\\. if exec_stop \ then Some(undefined, \) else M \)" text\The generic version using tuples is identical with @{term \call_1\<^sub>C\}.\ definition call_1\<^sub>C :: "( '\ \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E) \ ((('\_ext) control_state_ext) \ '\) \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_1\<^sub>C = call\<^sub>C" definition call_2\<^sub>C :: "( '\ \ '\ \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E) \ ((('\_ext) control_state_ext) \ '\) \ ((('\_ext) control_state_ext) \ '\) \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_2\<^sub>C M A\<^sub>1 A\<^sub>2 = (\\. if exec_stop \ then Some(undefined, \) else M (A\<^sub>1 \) (A\<^sub>2 \) \)" definition call_3\<^sub>C :: "( '\ \ '\ \ '\ \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E) \ ((('\_ext) control_state_ext) \ '\) \ ((('\_ext) control_state_ext) \ '\) \ ((('\_ext) control_state_ext) \ '\) \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "call_3\<^sub>C M A\<^sub>1 A\<^sub>2 A\<^sub>3 = (\\. if exec_stop \ then Some(undefined, \) else M (A\<^sub>1 \) (A\<^sub>2 \) (A\<^sub>3 \) \)" (* and 4 and 5 and ... *) section\ Some Term-Coding Functions \ text\In the following, we add a number of advanced HOL-term constructors in the style of @{ML_structure "HOLogic"} from the Isabelle/HOL libraries. They incorporate the construction of types during term construction in a bottom-up manner. Consequently, the leafs of such terms should always be typed, and anonymous loose-@{ML "Bound"} variables avoided.\ ML\ (* HOLogic extended *) fun mk_None ty = let val none = \<^const_name>\Option.option.None\ val none_ty = ty --> Type(\<^type_name>\option\,[ty]) in Const(none, none_ty) end; fun mk_Some t = let val some = \<^const_name>\Option.option.Some\ val ty = fastype_of t val some_ty = ty --> Type(\<^type_name>\option\,[ty]) in Const(some, some_ty) $ t end; fun dest_listTy (Type(\<^type_name>\List.list\, [T])) = T; fun mk_hdT t = let val ty = fastype_of t in Const(\<^const_name>\List.hd\, ty --> (dest_listTy ty)) $ t end fun mk_tlT t = let val ty = fastype_of t in Const(\<^const_name>\List.tl\, ty --> ty) $ t end fun mk_undefined (@{typ "unit"}) = Const (\<^const_name>\Product_Type.Unity\, \<^typ>\unit\) |mk_undefined t = Const (\<^const_name>\HOL.undefined\, t) fun meta_eq_const T = Const (\<^const_name>\Pure.eq\, T --> T --> propT); fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u; fun mk_pat_tupleabs [] t = t | mk_pat_tupleabs [(s,ty)] t = absfree(s,ty)(t) | mk_pat_tupleabs ((s,ty)::R) t = HOLogic.mk_case_prod(absfree(s,ty)(mk_pat_tupleabs R t)); fun read_constname ctxt n = fst(dest_Const(Syntax.read_term ctxt n)) fun wfrecT order recs = let val funT = domain_type (fastype_of recs) val aTy = domain_type funT val ordTy = HOLogic.mk_setT(HOLogic.mk_prodT (aTy,aTy)) in Const(\<^const_name>\Wfrec.wfrec\, ordTy --> (funT --> funT) --> funT) $ order $ recs end +fun mk_lens_type from_ty to_ty = Type(@{type_name "lens.lens_ext"}, + [from_ty, to_ty, HOLogic.unitT]); \ text\And here comes the core of the \<^theory_text>\Clean\-State-Management: the module that provides the functionality for the commands keywords \<^theory_text>\global_vars\, \<^theory_text>\local_vars\ and \<^theory_text>\local_vars_test\. Note that the difference between \<^theory_text>\local_vars\ and \<^theory_text>\local_vars_test\ is just a technical one: \<^theory_text>\local_vars\ can only be used inside a Clean function specification, made with the \<^theory_text>\function_spec\ command. On the other hand, \<^theory_text>\local_vars_test\ is defined as a global Isar command for test purposes. A particular feature of the local-variable management is the provision of definitions for \<^term>\push\ and \<^term>\pop\ operations --- encoded as \<^typ>\('o, '\) MON\<^sub>S\<^sub>E\ operations --- which are vital for the function specifications defined below. \ ML\ structure StateMgt = struct open StateMgt_core val result_name = "result_value" fun get_result_value_conf name thy = let val S = filter_attr_of name thy in hd(filter (fn ((_,b),_) => b = result_name) S) handle Empty => error "internal error: get_result_value_conf " end; fun mk_lookup_result_value_term name sty thy = let val ((prefix,name),local_var(Type("fun", [_,ty]))) = get_result_value_conf name thy; val long_name = Sign.intern_const thy (prefix^"."^name) val term = Const(long_name, sty --> ty) in mk_hdT (term $ Free("\",sty)) end fun map_to_update sty is_pop thy ((struct_name, attr_name), local_var (Type("fun",[_,ty]))) term = let val tlT = if is_pop then Const(\<^const_name>\List.tl\, ty --> ty) else Const(\<^const_name>\List.Cons\, dest_listTy ty --> ty --> ty) $ mk_undefined (dest_listTy ty) - val update_name = Sign.intern_const thy (struct_name^"."^attr_name^"_update") + val update_name = Sign.intern_const thy (struct_name^"."^attr_name^"_update") in (Const(update_name, (ty --> ty) --> sty --> sty) $ tlT) $ term end | map_to_update _ _ _ ((_, _),_) _ = error("internal error map_to_update") fun mk_local_state_name binding = Binding.prefix_name "local_" (Binding.suffix_name "_state" binding) fun mk_global_state_name binding = Binding.prefix_name "global_" (Binding.suffix_name "_state" binding) fun construct_update is_pop binding sty thy = let val long_name = Binding.name_of( binding) val attrS = StateMgt_core.filter_attr_of long_name thy in fold (map_to_update sty is_pop thy) (attrS) (Free("\",sty)) end fun cmd (decl, spec, prems, params) = #2 oo Specification.definition' decl params prems spec fun mk_push_name binding = Binding.prefix_name "push_" binding +fun mk_lense_name binding = Binding.suffix_name "\<^sub>L" binding + fun push_eq binding name_op rty sty lthy = let val mty = MON_SE_T rty sty val thy = Proof_Context.theory_of lthy val term = construct_update false binding sty thy in mk_meta_eq((Free(name_op, mty) $ Free("\",sty)), mk_Some ( HOLogic.mk_prod (mk_undefined rty,term))) end; fun mk_push_def binding sty lthy = let val name_pushop = mk_push_name binding val rty = \<^typ>\unit\ val eq = push_eq binding (Binding.name_of name_pushop) rty sty lthy val mty = StateMgt_core.MON_SE_T rty sty val args = (SOME(name_pushop, SOME mty, NoSyn), (Binding.empty_atts,eq),[],[]) in cmd args true lthy end; fun mk_pop_name binding = Binding.prefix_name "pop_" binding fun pop_eq binding name_op rty sty lthy = let val mty = MON_SE_T rty sty val thy = Proof_Context.theory_of lthy val res_access = mk_lookup_result_value_term (Binding.name_of binding) sty thy val term = construct_update true binding sty thy in mk_meta_eq((Free(name_op, mty) $ Free("\",sty)), mk_Some ( HOLogic.mk_prod (res_access,term))) end; fun mk_pop_def binding rty sty lthy = let val mty = StateMgt_core.MON_SE_T rty sty val name_op = mk_pop_name binding val eq = pop_eq binding (Binding.name_of name_op) rty sty lthy val args = (SOME(name_op, SOME mty, NoSyn),(Binding.empty_atts,eq),[],[]) in cmd args true lthy end; fun read_parent NONE ctxt = (NONE, ctxt) | read_parent (SOME raw_T) ctxt = (case Proof_Context.read_typ_abbrev ctxt raw_T of Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt) | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); fun read_fields raw_fields ctxt = let val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields); val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts; val ctxt' = fold Variable.declare_typ Ts ctxt; in (fields, ctxt') end; fun parse_typ_'a ctxt binding = let val ty_bind = Binding.prefix_name "'a " (Binding.suffix_name "_scheme" binding) in case Syntax.parse_typ ctxt (Binding.name_of ty_bind) of Type (s, _) => Type (s, [@{typ "'a::type"}]) | _ => error ("Unexpected type" ^ Position.here \<^here>) end +fun define_lense binding sty (attr_name,rty,_) lthy = + let val prefix = Binding.name_of binding^"_" + val name_L = attr_name |> Binding.prefix_name prefix + |> mk_lense_name + val name_upd = Binding.suffix_name "_update" attr_name + val acc_ty = sty --> rty + val upd_ty = (rty --> rty) --> sty --> sty + val cr = Const(@{const_name "Optics.create\<^sub>L"}, + acc_ty --> upd_ty --> mk_lens_type rty sty) + val thy = Proof_Context.theory_of lthy + val acc_name = Sign.intern_const thy (Binding.name_of attr_name) + val upd_name = Sign.intern_const thy (Binding.name_of name_upd) + val acc = Const(acc_name, acc_ty) + val upd = Const(upd_name, upd_ty) + val lens_ty = mk_lens_type rty sty + val eq = mk_meta_eq (Free(Binding.name_of name_L, lens_ty), cr $ acc $ upd) + val args = (SOME(name_L, SOME lens_ty, NoSyn), (Binding.empty_atts,eq),[],[]) + in cmd args true lthy end + fun add_record_cmd0 read_fields overloaded is_global_kind raw_params binding raw_parent raw_fields thy = let val ctxt = Proof_Context.init_global thy; val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; val (parent, ctxt2) = read_parent raw_parent ctxt1; val (fields, ctxt3) = read_fields raw_fields ctxt2; fun lift (a,b,c) = (a, HOLogic.listT b, c) val fields' = if is_global_kind then fields else map lift fields val params' = map (Proof_Context.check_tfree ctxt3) params; val declare = StateMgt_core.declare_state_variable_global fun upd_state_typ thy = let val ctxt = Proof_Context.init_global thy val ty = Syntax.parse_typ ctxt (Binding.name_of binding) in StateMgt_core.upd_state_type_global(K ty)(thy) end fun insert_var ((f,_,_), thy) = if is_global_kind then declare StateMgt_core.global_var (Binding.name_of f) thy else declare StateMgt_core.local_var (Binding.name_of f) thy fun define_push_pop thy = if not is_global_kind then let val sty = parse_typ_'a (Proof_Context.init_global thy) binding; val rty = dest_listTy (#2(hd(rev fields'))) in thy |> Named_Target.theory_map (mk_push_def binding sty) |> Named_Target.theory_map (mk_pop_def binding rty sty) end else thy + fun define_lenses thy = + let val sty = parse_typ_'a (Proof_Context.init_global thy) binding; + in thy |> Named_Target.theory_map (fold (define_lense binding sty) fields') end in thy |> Record.add_record overloaded (params', binding) parent fields' |> (fn thy => List.foldr insert_var (thy) (fields')) |> upd_state_typ |> define_push_pop + |> define_lenses end; fun typ_2_string_raw (Type(s,[TFree _])) = if String.isSuffix "_scheme" s then Long_Name.base_name(unsuffix "_scheme" s) else Long_Name.base_name(unsuffix "_ext" s) |typ_2_string_raw (Type(s,_)) = error ("Illegal parameterized state type - not allowed in Clean:" ^ s) |typ_2_string_raw _ = error "Illegal state type - not allowed in Clean." fun new_state_record0 add_record_cmd is_global_kind (((raw_params, binding), res_ty), raw_fields) thy = let val binding = if is_global_kind then mk_global_state_name binding else mk_local_state_name binding val raw_parent = SOME(typ_2_string_raw (StateMgt_core.get_state_type_global thy)) val pos = Binding.pos_of binding - fun upd_state_typ thy = - StateMgt_core.upd_state_type_global (K (parse_typ_'a (Proof_Context.init_global thy) binding)) thy + fun upd_state_typ thy = StateMgt_core.upd_state_type_global + (K (parse_typ_'a (Proof_Context.init_global thy) binding)) thy val result_binding = Binding.make(result_name,pos) val raw_fields' = case res_ty of NONE => raw_fields | SOME res_ty => raw_fields @ [(result_binding,res_ty, NoSyn)] in thy |> add_record_cmd {overloaded = false} is_global_kind raw_params binding raw_parent raw_fields' |> upd_state_typ end val add_record_cmd = add_record_cmd0 read_fields; val add_record_cmd' = add_record_cmd0 pair; val new_state_record = new_state_record0 add_record_cmd val new_state_record' = new_state_record0 add_record_cmd' val _ = Outer_Syntax.command \<^command_keyword>\global_vars\ "define global state record" ((Parse.type_args_constrained -- Parse.binding) -- Scan.succeed NONE -- Scan.repeat1 Parse.const_binding >> (Toplevel.theory o new_state_record true)); ; val _ = Outer_Syntax.command \<^command_keyword>\local_vars_test\ "define local state record" ((Parse.type_args_constrained -- Parse.binding) -- (Parse.typ >> SOME) -- Scan.repeat1 Parse.const_binding >> (Toplevel.theory o new_state_record false)) ; end \ section\Syntactic Sugar supporting \\\-lifting for Global and Local Variables \ ML \ structure Clean_Syntax_Lift = struct + type T = { is_local : string -> bool + , is_global : string -> bool } + + val init = + Proof_Context.theory_of + #> (fn thy => + { is_local = fn name => StateMgt_core.is_local_program_variable name thy + , is_global = fn name => StateMgt_core.is_global_program_variable name thy }) + local fun mk_local_access X = Const (@{const_name "Fun.comp"}, dummyT) $ Const (@{const_name "List.list.hd"}, dummyT) $ X in - fun app_sigma db tm ctxt = case tm of - Const(name, _) => if StateMgt_core.is_global_program_variable name (Proof_Context.theory_of ctxt) + fun app_sigma0 (st : T) db tm = case tm of + Const(name, _) => if #is_global st name then tm $ (Bound db) (* lambda lifting *) - else if StateMgt_core.is_local_program_variable name (Proof_Context.theory_of ctxt) + else if #is_local st name then (mk_local_access tm) $ (Bound db) (* lambda lifting local *) else tm (* no lifting *) | Free _ => tm | Var _ => tm | Bound n => if n > db then Bound(n + 1) else Bound n - | Abs (x, ty, tm') => Abs(x, ty, app_sigma (db+1) tm' ctxt) - | t1 $ t2 => (app_sigma db t1 ctxt) $ (app_sigma db t2 ctxt) + | Abs (x, ty, tm') => Abs(x, ty, app_sigma0 st (db+1) tm') + | t1 $ t2 => (app_sigma0 st db t1) $ (app_sigma0 st db t2) - fun scope_var name = - Proof_Context.theory_of - #> (fn thy => - if StateMgt_core.is_global_program_variable name thy then SOME true - else if StateMgt_core.is_local_program_variable name thy then SOME false - else NONE) + fun app_sigma db tm = init #> (fn st => app_sigma0 st db tm) + + fun scope_var st name = + if #is_global st name then SOME true + else if #is_local st name then SOME false + else NONE fun assign_update var = var ^ Record.updateN fun transform_term0 abs scope_var tm = case tm of Const (@{const_name "Clean.syntax_assign"}, _) $ (t1 as Const ("_type_constraint_", _) $ Const (name, ty)) $ t2 => Const ( case scope_var name of SOME true => @{const_name "assign_global"} | SOME false => @{const_name "assign_local"} | NONE => raise TERM ("mk_assign", [t1]) , dummyT) $ Const(assign_update name, ty) $ abs t2 | _ => abs tm - fun transform_term ctxt sty = + fun transform_term st sty = transform_term0 - (fn tm => Abs ("\", sty, app_sigma 0 tm ctxt)) - (fn name => scope_var name ctxt) + (fn tm => Abs ("\", sty, app_sigma0 st 0 tm)) + (scope_var st) - fun transform_term' ctxt = transform_term ctxt dummyT + fun transform_term' st = transform_term st dummyT fun string_tr ctxt content args = let fun err () = raise TERM ("string_tr", args) in (case args of [(Const (@{syntax_const "_constrain"}, _)) $ (Free (s, _)) $ p] => (case Term_Position.decode_position p of SOME (pos, _) => Symbol_Pos.implode (content (s, pos)) |> Syntax.parse_term ctxt - |> transform_term ctxt (StateMgt_core.get_state_type ctxt) + |> transform_term (init ctxt) (StateMgt_core.get_state_type ctxt) |> Syntax.check_term ctxt | NONE => err ()) | _ => err ()) end end end \ syntax "_cartouche_string" :: "cartouche_position \ string" ("_") parse_translation \ [(@{syntax_const "_cartouche_string"}, (fn ctxt => Clean_Syntax_Lift.string_tr ctxt (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))] \ section\Support for (direct recursive) Clean Function Specifications \ text\Based on the machinery for the State-Management and implicitly cooperating with the cartouches for assignment syntax, the function-specification \<^theory_text>\function_spec\-package coordinates: \<^enum> the parsing and type-checking of parameters, \<^enum> the parsing and type-checking of pre and post conditions in MOAL notation (using \\\-lifting cartouches and implicit reference to parameters, pre and post states), \<^enum> the parsing local variable section with the local-variable space generation, \<^enum> the parsing of the body in this extended variable space, \<^enum> and optionally the support of measures for recursion proofs. The reader interested in details is referred to the \<^file>\../examples/Quicksort_concept.thy\-example, accompanying this distribution. \ + +text\In order to support the \<^verbatim>\old\-notation known from JML and similar annotation languages, +we introduce the following definition:\ definition old :: "'a \ 'a" where "old x = x" - -ML\ -\ - +text\The core module of the parser and operation specification construct is implemented in the +following module:\ ML \ structure Function_Specification_Parser = struct type funct_spec_src = { - binding: binding, (* name *) - params: (binding*string) list, (* parameters and their type*) - ret_type: string, (* return type; default unit *) - locals: (binding*string*mixfix)list, (* local variables *) - pre_src: string, (* precondition src *) - post_src: string, (* postcondition src *) - variant_src: string option, (* variant src *) - body_src: string * Position.T (* body src *) + binding: binding, (* name *) + params: (binding*string) list, (* parameters and their type*) + ret_type: string, (* return type; default unit *) + locals: (binding*string*mixfix)list, (* local variables *) + pre_src: string, (* precondition src *) + post_src: string, (* postcondition src *) + variant_src: string option, (* variant src *) + body_src: string * Position.T (* body src *) + } + + type funct_spec_sem_old = { + params: (binding*typ) list, (* parameters and their type*) + ret_ty: typ, (* return type *) + pre: term, (* precondition *) + post: term, (* postcondition *) + variant: term option (* variant *) } type funct_spec_sem = { - params: (binding*typ) list, (* parameters and their type*) - ret_ty: typ, (* return type *) - pre: term, (* precondition *) - post: term, (* postcondition *) - variant: term option (* variant *) + binding: binding, (* name *) + params: (binding*string) list, (* parameters and their type*) + ret_type: string, (* return type; default unit *) + locals: (binding*string*mixfix)list, (* local variables *) + read_pre: Proof.context -> term, (* precondition src *) + read_post: Proof.context -> term, (* postcondition src *) + read_variant_opt: (Proof.context->term) option, (* variant src *) + read_body: Proof.context -> typ -> term (* body src *) } - val parse_arg_decl = Parse.binding -- (Parse.$$$ "::" |-- Parse.typ) val parse_param_decls = Args.parens (Parse.enum "," parse_arg_decl) val parse_returns_clause = Scan.optional (\<^keyword>\returns\ |-- Parse.typ) "unit" val locals_clause = (Scan.optional ( \<^keyword>\local_vars\ -- (Scan.repeat1 Parse.const_binding)) ("", [])) val parse_proc_spec = ( Parse.binding -- parse_param_decls -- parse_returns_clause --| \<^keyword>\pre\ -- Parse.term --| \<^keyword>\post\ -- Parse.term - -- (Scan.option ( \<^keyword>\variant\ |-- Parse.term)) + -- (Scan.option ( \<^keyword>\variant\ |-- Parse.term)) -- (Scan.optional( \<^keyword>\local_vars\ |-- (Scan.repeat1 Parse.const_binding))([])) --| \<^keyword>\defines\ -- (Parse.position (Parse.term)) ) >> (fn ((((((((binding,params),ret_ty),pre_src),post_src),variant_src),locals)),body_src) => { binding = binding, params=params, ret_type=ret_ty, pre_src=pre_src, post_src=post_src, variant_src=variant_src, locals=locals, body_src=body_src} : funct_spec_src ) fun read_params params ctxt = let val Ts = Syntax.read_typs ctxt (map snd params); in (Ts, fold Variable.declare_typ Ts ctxt) end; fun read_result ret_ty ctxt = let val [ty] = Syntax.read_typs ctxt [ret_ty] val ctxt' = Variable.declare_typ ty ctxt in (ty, ctxt') end - fun read_function_spec ({ params, ret_type, variant_src, ...} : funct_spec_src) ctxt = + fun read_function_spec ( params, ret_type, read_variant_opt) ctxt = let val (params_Ts, ctxt') = read_params params ctxt val (rty, ctxt'') = read_result ret_type ctxt' - val variant = Option.map (Syntax.read_term ctxt'') variant_src - in ({params = (params, params_Ts), ret_ty = rty,variant = variant},ctxt'') end + val variant = case read_variant_opt of + NONE => NONE + |SOME f => SOME(f ctxt'') + val paramT_l = (map2 (fn (b, _) => fn T => (b, T)) params params_Ts) + in ((paramT_l, rty, variant),ctxt'') end fun check_absence_old term = let fun test (s,ty) = if s = @{const_name "old"} andalso fst (dest_Type ty) = "fun" then error("the old notation is not allowed here!") else false in exists_Const test term end fun transform_old sty term = let fun transform_old0 (Const(@{const_name "old"}, Type ("fun", [_,_])) $ term ) = (case term of (Const(s,ty) $ Bound x) => (Const(s,ty) $ Bound (x+1)) | _ => error("illegal application of the old notation.")) |transform_old0 (t1 $ t2) = transform_old0 t1 $ transform_old0 t2 |transform_old0 (Abs(s,ty,term)) = Abs(s,ty,transform_old0 term) |transform_old0 term = term in Abs("\\<^sub>p\<^sub>r\<^sub>e", sty, transform_old0 term) end - fun define_cond binding f_sty transform_old src_suff check_absence_old params src ctxt = - let val src' = case transform_old (Syntax.read_term ctxt src) of - Abs(nn, sty_pre, term) => mk_pat_tupleabs (map (apsnd #2) params) (Abs(nn,sty_pre(* sty root ! !*),term)) + fun define_cond binding f_sty transform_old check_absence_old cond_suffix params read_cond (ctxt:local_theory) = + let val params' = map (fn(b, ty) => (Binding.name_of b,ty)) params + val src' = case transform_old (read_cond ctxt) of + Abs(nn, sty_pre, term) => mk_pat_tupleabs params' (Abs(nn,sty_pre,term)) | _ => error ("define abstraction for result" ^ Position.here \<^here>) - val bdg = Binding.suffix_name src_suff binding + val bdg = Binding.suffix_name cond_suffix binding val _ = check_absence_old src' - val eq = mk_meta_eq(Free(Binding.name_of bdg, HOLogic.mk_tupleT(map (#2 o #2) params) --> f_sty HOLogic.boolT),src') + val bdg_ty = HOLogic.mk_tupleT(map (#2) params) --> f_sty HOLogic.boolT + val eq = mk_meta_eq(Free(Binding.name_of bdg, bdg_ty),src') val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) in StateMgt.cmd args true ctxt end fun define_precond binding sty = - define_cond binding (fn boolT => sty --> boolT) I "_pre" check_absence_old + define_cond binding (fn boolT => sty --> boolT) I check_absence_old "_pre" fun define_postcond binding rty sty = - define_cond binding (fn boolT => sty --> sty --> rty --> boolT) (transform_old sty) "_post" I + define_cond binding (fn boolT => sty --> sty --> rty --> boolT) (transform_old sty) I "_post" fun define_body_core binding args_ty sty params body = - let val bdg_core = Binding.suffix_name "_core" binding + let val params' = map (fn(b,ty) => (Binding.name_of b, ty)) params + val bdg_core = Binding.suffix_name "_core" binding val bdg_core_name = Binding.name_of bdg_core val umty = args_ty --> StateMgt.MON_SE_T @{typ "unit"} sty - val eq = mk_meta_eq(Free (bdg_core_name, umty),mk_pat_tupleabs(map(apsnd #2)params) body) + val eq = mk_meta_eq(Free (bdg_core_name, umty),mk_pat_tupleabs params' body) val args_core =(SOME (bdg_core, SOME umty, NoSyn), (Binding.empty_atts, eq), [], []) in StateMgt.cmd args_core true end - fun define_body_main {recursive = x:bool} binding rty sty params variant_src _ ctxt = + fun define_body_main {recursive = x:bool} binding rty sty params read_variant_opt _ ctxt = let val push_name = StateMgt.mk_push_name (StateMgt.mk_local_state_name binding) val pop_name = StateMgt.mk_pop_name (StateMgt.mk_local_state_name binding) val bdg_core = Binding.suffix_name "_core" binding val bdg_core_name = Binding.name_of bdg_core val bdg_rec_name = Binding.name_of(Binding.suffix_name "_rec" binding) val bdg_ord_name = Binding.name_of(Binding.suffix_name "_order" binding) - - val args_ty = HOLogic.mk_tupleT (map (#2 o #2) params) - val params' = map (apsnd #2) params + val args_ty = HOLogic.mk_tupleT (map snd params) val rmty = StateMgt_core.MON_SE_T rty sty - val umty = StateMgt.MON_SE_T @{typ "unit"} sty val argsProdT = HOLogic.mk_prodT(args_ty,args_ty) val argsRelSet = HOLogic.mk_setT argsProdT - val measure_term = case variant_src of + val params' = map (fn(b, ty) => (Binding.name_of b,ty)) params + val measure_term = case read_variant_opt of NONE => Free(bdg_ord_name,args_ty --> HOLogic.natT) - | SOME str => (Syntax.read_term ctxt str |> mk_pat_tupleabs params') + | SOME f => ((f ctxt) |> mk_pat_tupleabs params') val measure = Const(@{const_name "Wellfounded.measure"}, (args_ty --> HOLogic.natT) --> argsRelSet ) $ measure_term - val lhs_main = if x andalso is_none variant_src + val lhs_main = if x andalso is_none (read_variant_opt ) then Free(Binding.name_of binding, (args_ty --> HOLogic.natT) --> args_ty --> rmty) $ Free(bdg_ord_name, args_ty --> HOLogic.natT) else Free(Binding.name_of binding, args_ty --> rmty) val rhs_main = mk_pat_tupleabs params' (Const(@{const_name "Clean.block\<^sub>C"}, umty --> umty --> rmty --> rmty) $ Const(read_constname ctxt (Binding.name_of push_name),umty) $ (Const(read_constname ctxt bdg_core_name, args_ty --> umty) $ HOLogic.mk_tuple (map Free params')) $ Const(read_constname ctxt (Binding.name_of pop_name),rmty)) val rhs_main_rec = wfrecT measure (Abs(bdg_rec_name, (args_ty --> umty) , mk_pat_tupleabs params' (Const(@{const_name "Clean.block\<^sub>C"}, umty-->umty-->rmty-->rmty) $ Const(read_constname ctxt (Binding.name_of push_name),umty) $ (Const(read_constname ctxt bdg_core_name, (args_ty --> umty) --> args_ty --> umty) $ (Bound (length params)) $ HOLogic.mk_tuple (map Free params')) $ Const(read_constname ctxt (Binding.name_of pop_name),rmty)))) val eq_main = mk_meta_eq(lhs_main, if x then rhs_main_rec else rhs_main ) val args_main = (SOME(binding,NONE,NoSyn), (Binding.empty_atts,eq_main),[],[]) in ctxt |> StateMgt.cmd args_main true end +val _ = Local_Theory.exit_result_global; +val _ = Named_Target.theory_map_result; +val _ = Named_Target.theory_map; - fun checkNsem_function_spec {recursive = false} ({variant_src=SOME _, ...}) _ = + + + +(* This code is in large parts so messy because the extensible record package (used inside + StateMgt.new_state_record) is only available as transformation on global contexts, + which cuts the local context calculations into two halves. The second halves is cut + again into two halves because the definition of the core apparently does not take effect + before defining the block - structure when not separated (this problem can perhaps be overcome + somehow)) + + Precondition: the terms of the read-functions are full typed in the respective + local contexts. + *) + fun checkNsem_function_spec_gen {recursive = false} ({read_variant_opt=SOME _, ...}) _ = error "No measure required in non-recursive call" - |checkNsem_function_spec (isrec as {recursive = _:bool}) - (args as {binding, ret_type, variant_src, locals, body_src, pre_src, post_src, ...} : funct_spec_src) + |checkNsem_function_spec_gen (isrec as {recursive = _:bool}) + ({binding, ret_type, read_variant_opt, locals, + read_body, read_pre, read_post, params} : funct_spec_sem) thy = - let val (theory_map, thy') = - Named_Target.theory_map_result - (K (fn f => Named_Target.theory_map o f)) - (read_function_spec args - #> uncurry (fn {params=(params, Ts),ret_ty,variant = _} => - pair (fn f => - Proof_Context.add_fixes (map2 (fn (b, _) => fn T => (b, SOME T, NoSyn)) params Ts) + let fun addfixes ((params_Ts,ret_ty,t_opt), ctxt) = + (fn fg => fn ctxt => + ctxt + |> Proof_Context.add_fixes (map (fn (s,ty)=>(s,SOME ty,NoSyn)) params_Ts) (* this declares the parameters of a function specification as Free variables (overrides a possible constant declaration) and assigns the declared type to them *) - #> uncurry (fn params' => f (@{map 3} (fn b' => fn (b, _) => fn T => (b',(b,T))) params' params Ts) ret_ty)))) - thy + |> (fn (X, ctxt) => fg params_Ts ret_ty ctxt) + , ctxt) + val (theory_map, thy') = Named_Target.theory_map_result + (K (fn f => Named_Target.theory_map o f)) + ( read_function_spec (params, ret_type, read_variant_opt) + #> addfixes + ) + (thy) in thy' |> theory_map let val sty_old = StateMgt_core.get_state_type_global thy' - in fn params => fn ret_ty => - define_precond binding sty_old params pre_src - #> define_postcond binding ret_ty sty_old params post_src end + fun parse_contract params ret_ty = + ( define_precond binding sty_old params read_pre + #> define_postcond binding ret_ty sty_old params read_post) + in parse_contract + end |> StateMgt.new_state_record false ((([],binding), SOME ret_type),locals) |> theory_map (fn params => fn ret_ty => fn ctxt => let val sty = StateMgt_core.get_state_type ctxt - val args_ty = HOLogic.mk_tupleT (map (#2 o #2) params) + val args_ty = HOLogic.mk_tupleT (map snd params) val mon_se_ty = StateMgt_core.MON_SE_T ret_ty sty + val body = read_body ctxt mon_se_ty val ctxt' = if #recursive isrec then Proof_Context.add_fixes [(binding, SOME (args_ty --> mon_se_ty), NoSyn)] ctxt |> #2 else ctxt - val body = Syntax.read_term ctxt' (fst body_src) + val body = read_body ctxt' mon_se_ty in ctxt' |> define_body_core binding args_ty sty params body - end) + end) (* separation nasty, but nec. in order to make the body definition + take effect. No other reason. *) + |> theory_map (fn params => fn ret_ty => fn ctxt => let val sty = StateMgt_core.get_state_type ctxt - val body = Syntax.read_term ctxt (fst body_src) - in ctxt |> define_body_main isrec binding ret_ty sty params variant_src body + val mon_se_ty = StateMgt_core.MON_SE_T ret_ty sty + val body = read_body ctxt mon_se_ty + in ctxt |> define_body_main isrec binding ret_ty sty + params read_variant_opt body end) end + fun checkNsem_function_spec (isrec as {recursive = _:bool}) + ( {binding, ret_type, variant_src, locals, + body_src, pre_src, post_src, params} : funct_spec_src) + thy = + checkNsem_function_spec_gen (isrec) + ( {binding = binding, + params = params, + ret_type = ret_type, + read_variant_opt = (case variant_src of + NONE => NONE + | SOME t=> SOME(fn ctxt + => Syntax.read_term ctxt t)), + locals = locals, + read_body = fn ctxt => fn expected_type + => Syntax.read_term ctxt (fst body_src), + read_pre = fn ctxt => Syntax.read_term ctxt pre_src, + read_post = fn ctxt => Syntax.read_term ctxt post_src} : funct_spec_sem) + thy + val _ = Outer_Syntax.command \<^command_keyword>\function_spec\ "define Clean function specification" (parse_proc_spec >> (Toplevel.theory o checkNsem_function_spec {recursive = false})); val _ = Outer_Syntax.command \<^command_keyword>\rec_function_spec\ "define recursive Clean function specification" (parse_proc_spec >> (Toplevel.theory o checkNsem_function_spec {recursive = true})); end \ section\The Rest of Clean: Break/Return aware Version of If, While, etc.\ definition if_C :: "[('\_ext) control_state_ext \ bool, ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E, ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E] \ ('\, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "if_C c E F = (\\. if exec_stop \ then Some(undefined, \) \ \state unchanged, return arbitrary\ else if c \ then E \ else F \)" syntax (xsymbols) "_if_SECLEAN" :: "['\ \ bool,('o,'\)MON\<^sub>S\<^sub>E,('o','\)MON\<^sub>S\<^sub>E] \ ('o','\)MON\<^sub>S\<^sub>E" - ("(if\<^sub>C _ then _ else _fi)" [5,8,8]8) + ("(if\<^sub>C _ then _ else _fi)" [5,8,8]20) translations "(if\<^sub>C cond then T1 else T2 fi)" == "CONST Clean.if_C cond T1 T2" definition while_C :: "(('\_ext) control_state_ext \ bool) \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "while_C c B \ (\\. if exec_stop \ then Some((), \) else ((MonadSE.while_SE (\ \. \exec_stop \ \ c \) B) ;- unset_break_status) \)" syntax (xsymbols) "_while_C" :: "['\ \ bool, (unit, '\)MON\<^sub>S\<^sub>E] \ (unit, '\)MON\<^sub>S\<^sub>E" - ("(while\<^sub>C _ do _ od)" [8,8]8) + ("(while\<^sub>C _ do _ od)" [8,8]20) translations "while\<^sub>C c do b od" == "CONST Clean.while_C c b" - + + +section\Miscellaneous\ + +text\Since \<^verbatim>\int\ were mapped to Isabelle/HOL @{typ "int"} and \<^verbatim>\unsigned int\ to @{typ "nat"}, +there is the need for a common interface for accesses in arrays, which were represented by +Isabelle/HOL lists: +\ + +consts nth\<^sub>C :: "'a list \ 'b \ 'a" +overloading nth\<^sub>C \ "nth\<^sub>C :: 'a list \ nat \ 'a" +begin +definition + nth\<^sub>C_nat : "nth\<^sub>C (S::'a list) (a) \ nth S a" +end + +overloading nth\<^sub>C \ "nth\<^sub>C :: 'a list \ int \ 'a" +begin +definition + nth\<^sub>C_int : "nth\<^sub>C (S::'a list) (a) \ nth S (nat a)" +end + +definition while_C_A :: " (('\_ext) control_state_scheme \ bool) + \ (('\_ext) control_state_scheme \ nat) + \ (('\_ext) control_state_ext \ bool) + \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E + \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" + where "while_C_A Inv f c B \ while_C c B" + + +ML\ + +structure Clean_Term_interface = +struct + +fun mk_seq_C C C' = let val t = fastype_of C + val t' = fastype_of C' + in Const(\<^const_name>\bind_SE'\, t --> t' --> t') end; + +fun mk_skip_C sty = Const(\<^const_name>\skip\<^sub>S\<^sub>E\, StateMgt_core.MON_SE_T HOLogic.unitT sty) + +fun mk_break sty = + Const(\<^const_name>\if_C\, StateMgt_core.MON_SE_T HOLogic.unitT sty ) + +fun mk_return_C upd rhs = + let val ty = fastype_of rhs + val (sty,rty) = case ty of + Type("fun", [sty,rty]) => (sty,rty) + | _ => error "mk_return_C: illegal type for body" + val upd_ty = (HOLogic.listT rty --> HOLogic.listT rty) --> sty --> sty + val rhs_ty = sty --> rty + val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty + in Const(\<^const_name>\return\<^sub>C\, upd_ty --> rhs_ty --> mty) $ upd $ rhs end + +fun mk_assign_global_C upd rhs = + let val ty = fastype_of rhs + val (sty,rty) = case ty of + Type("fun", [sty,rty]) => (sty,rty) + | _ => error "mk_assign_global_C: illegal type for body" + val upd_ty = (rty --> rty) --> sty --> sty + val rhs_ty = sty --> rty + val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty + in Const(\<^const_name>\assign_global\, upd_ty --> rhs_ty --> mty) $ upd $ rhs end + +fun mk_assign_local_C upd rhs = + let val ty = fastype_of rhs + val (sty,rty) = case ty of + Type("fun", [sty,rty]) => (sty,rty) + | _ => error "mk_assign_local_C: illegal type for body" + val upd_ty = (HOLogic.listT rty --> HOLogic.listT rty) --> sty --> sty + val rhs_ty = sty --> rty + val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty + in Const(\<^const_name>\assign_local\, upd_ty --> rhs_ty --> mty) $ upd $ rhs end + +fun mk_call_C opn args = + let val ty = fastype_of opn + val (argty,mty) = case ty of + Type("fun", [argty,mty]) => (argty,mty) + | _ => error "mk_call_C: illegal type for body" + val sty = case mty of + Type("fun", [sty,_]) => sty + | _ => error "mk_call_C: illegal type for body 2" + val args_ty = sty --> argty + in Const(\<^const_name>\call\<^sub>C\, ty --> args_ty --> mty) $ opn $ args end + +(* missing : a call_assign_local and a call_assign_global. Or define at HOL level ? *) + +fun mk_if_C c B B' = + let val ty = fastype_of B + val ty_cond = case ty of + Type("fun", [argty,_]) => argty --> HOLogic.boolT + |_ => error "mk_if_C: illegal type for body" + in Const(\<^const_name>\if_C\, ty_cond --> ty --> ty --> ty) $ c $ B $ B' + end; + +fun mk_while_C c B = + let val ty = fastype_of B + val ty_cond = case ty of + Type("fun", [argty,_]) => argty --> HOLogic.boolT + |_ => error "mk_while_C: illegal type for body" + in Const(\<^const_name>\while_C\, ty_cond --> ty --> ty) $ c $ B + end; + +fun mk_while_anno_C inv f c B = + (* no type-check on inv and measure f *) + let val ty = fastype_of B + val (ty_cond,ty_m) = case ty of + Type("fun", [argty,_]) =>( argty --> HOLogic.boolT, + argty --> HOLogic.natT) + |_ => error "mk_while_anno_C: illegal type for body" + in Const(\<^const_name>\while_C_A\, ty_cond --> ty_m --> ty_cond --> ty --> ty) + $ inv $ f $ c $ B + end; + +fun mk_block_C push body pop = + let val body_ty = fastype_of body + val pop_ty = fastype_of pop + val bty = body_ty --> body_ty --> pop_ty --> pop_ty + in Const(\<^const_name>\block\<^sub>C\, bty) $ push $ body $ pop end + +end;\ + +section\Function-calls in Expressions\ + +text\The precise semantics of function-calls appearing inside expressions is underspecified in C, +which is a notorious problem for compilers and analysis tools. In Clean, it is impossible by +construction --- and the type displine --- to have function-calls inside expressions. +However, there is a somewhat \<^emph>\recommended coding-scheme\ for this feature, which leaves this +issue to decisions in the front-end: +\begin{verbatim} + a = f() + g(); +\end{verbatim} +can be represented in Clean by: +\x \ f(); y \ g(); \a := x + y\ \ or +\x \ g(); y \ f(); \a := y + x\ \ +which makes the evaluation order explicit without introducing +local variables or any form of explicit trace on the state-space of the Clean program. We assume, +however, even in this coding scheme, that \<^verbatim>\f()\ and \<^verbatim>\g()\ are atomic actions; note that this +assumption is not necessarily justified in modern compilers, where actually neither of these +two (atomic) serializations of \<^verbatim>\f()\ and \<^verbatim>\g()\ may exists. + +Note, furthermore, that expressions may not only be right-hand-sides of (local or global) +assignments or conceptually similar return-statements, but also passed as argument of other +function calls, where the same problem arises. +\ + + end - - \ No newline at end of file diff --git a/thys/Clean/src/Clean_Main.thy b/thys/Clean/src/Clean_Main.thy --- a/thys/Clean/src/Clean_Main.thy +++ b/thys/Clean/src/Clean_Main.thy @@ -1,47 +1,48 @@ (****************************************************************************** * 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 *) theory Clean_Main imports Clean Hoare_Clean Test_Clean begin end diff --git a/thys/Clean/src/Clean_Symbex.thy b/thys/Clean/src/Clean_Symbex.thy --- a/thys/Clean/src/Clean_Symbex.thy +++ b/thys/Clean/src/Clean_Symbex.thy @@ -1,425 +1,424 @@ (****************************************************************************** * 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 Clean_Symbex imports Clean begin section\Clean Symbolic Execution Rules \ subsection\Basic NOP - Symbolic Execution Rules. \ text\ As they are equalities, they can also be used as program optimization rules. \ lemma non_exec_assign : -assumes "\ exec_stop \" +assumes "\ \" shows "(\ \ ( _ \ assign f; M)) = ((f \) \ M)" by (simp add: assign_def assms exec_bind_SE_success) lemma non_exec_assign' : -assumes "\ exec_stop \" +assumes "\ \" shows "(\ \ (assign f;- M)) = ((f \) \ M)" by (simp add: assign_def assms exec_bind_SE_success bind_SE'_def) lemma exec_assign : assumes "exec_stop \" shows "(\ \ ( _ \ assign f; M)) = (\ \ M)" by (simp add: assign_def assms exec_bind_SE_success) lemma exec_assign' : assumes "exec_stop \" shows "(\ \ (assign f;- M)) = (\ \ M)" by (simp add: assign_def assms exec_bind_SE_success bind_SE'_def) subsection\Assign Execution Rules. \ lemma non_exec_assign_global : -assumes "\ exec_stop \" +assumes "\ \" shows "(\ \ ( _ \ assign_global upd rhs; M)) = ((upd (\_. rhs \) \) \ M)" by(simp add: assign_global_def non_exec_assign assms) lemma non_exec_assign_global' : -assumes "\ exec_stop \" +assumes "\ \" shows "(\ \ (assign_global upd rhs;- M)) = ((upd (\_. rhs \) \) \ M)" by (metis (full_types) assms bind_SE'_def non_exec_assign_global) lemma exec_assign_global : assumes "exec_stop \" shows "(\ \ ( _ \ assign_global upd rhs; M)) = ( \ \ M)" by (simp add: assign_global_def assign_def assms exec_bind_SE_success) lemma exec_assign_global' : assumes "exec_stop \" shows "(\ \ (assign_global upd rhs;- M)) = ( \ \ M)" by (simp add: assign_global_def assign_def assms exec_bind_SE_success bind_SE'_def) lemma non_exec_assign_local : -assumes "\ exec_stop \" -shows "(\ \ ( _ \ assign_local upd rhs; M)) = ((upd (map_hd (\_. rhs \)) \) \ M)" +assumes "\ \" +shows "(\ \ ( _ \ assign_local upd rhs; M)) = ((upd (upd_hd (\_. rhs \)) \) \ M)" by(simp add: assign_local_def non_exec_assign assms) lemma non_exec_assign_local' : -assumes "\ exec_stop \" -shows "(\ \ (assign_local upd rhs;- M)) = ((upd (map_hd (\_. rhs \)) \) \ M)" +assumes "\ \" +shows "(\ \ (assign_local upd rhs;- M)) = ((upd (upd_hd (\_. rhs \)) \) \ M)" by (metis assms bind_SE'_def non_exec_assign_local) lemmas non_exec_assign_localD'= non_exec_assign[THEN iffD1] lemma exec_assign_local : assumes "exec_stop \" shows "(\ \ ( _ \ assign_local upd rhs; M)) = ( \ \ M)" by (simp add: assign_local_def assign_def assms exec_bind_SE_success) lemma exec_assign_local' : assumes "exec_stop \" shows "(\ \ ( assign_local upd rhs;- M)) = ( \ \ M)" unfolding assign_local_def assign_def by (simp add: assms exec_bind_SE_success2) lemmas exec_assignD = exec_assign[THEN iffD1] thm exec_assignD lemmas exec_assignD' = exec_assign'[THEN iffD1] thm exec_assignD' lemmas exec_assign_globalD = exec_assign_global[THEN iffD1] lemmas exec_assign_globalD' = exec_assign_global'[THEN iffD1] lemmas exec_assign_localD = exec_assign_local[THEN iffD1] thm exec_assign_localD lemmas exec_assign_localD' = exec_assign_local'[THEN iffD1] subsection\Basic Call Symbolic Execution Rules. \ lemma exec_call_0 : assumes "exec_stop \" shows "(\ \ ( _ \ call_0\<^sub>C M; M')) = (\ \ M')" by (simp add: assms call_0\<^sub>C_def exec_bind_SE_success) lemma exec_call_0' : assumes "exec_stop \" shows "(\ \ (call_0\<^sub>C M;- M')) = (\ \ M')" by (simp add: assms bind_SE'_def exec_call_0) lemma exec_call_1 : assumes "exec_stop \" shows "(\ \ ( x \ call_1\<^sub>C M A\<^sub>1; M' x)) = (\ \ M' undefined)" by (simp add: assms call_1\<^sub>C_def call\<^sub>C_def exec_bind_SE_success) lemma exec_call_1' : assumes "exec_stop \" shows "(\ \ (call_1\<^sub>C M A\<^sub>1;- M')) = (\ \ M')" by (simp add: assms bind_SE'_def exec_call_1) lemma exec_call : assumes "exec_stop \" shows "(\ \ ( x \ call\<^sub>C M A\<^sub>1; M' x)) = (\ \ M' undefined)" by (simp add: assms call\<^sub>C_def call_1\<^sub>C_def exec_bind_SE_success) lemma exec_call' : assumes "exec_stop \" shows "(\ \ (call\<^sub>C M A\<^sub>1;- M')) = (\ \ M')" by (metis assms call_1\<^sub>C_def exec_call_1') lemma exec_call_2 : assumes "exec_stop \" shows "(\ \ ( _ \ call_2\<^sub>C M A\<^sub>1 A\<^sub>2; M')) = (\ \ M')" by (simp add: assms call_2\<^sub>C_def exec_bind_SE_success) lemma exec_call_2' : assumes "exec_stop \" shows "(\ \ (call_2\<^sub>C M A\<^sub>1 A\<^sub>2;- M')) = (\ \ M')" by (simp add: assms bind_SE'_def exec_call_2) subsection\Basic Call Symbolic Execution Rules. \ lemma non_exec_call_0 : -assumes "\ exec_stop \" +assumes "\ \" shows "(\ \ ( _ \ call_0\<^sub>C M; M')) = (\ \ M;- M')" by (simp add: assms bind_SE'_def bind_SE_def call_0\<^sub>C_def valid_SE_def) lemma non_exec_call_0' : -assumes "\ exec_stop \" +assumes "\ \" shows "(\ \ call_0\<^sub>C M;- M') = (\ \ M;- M')" by (simp add: assms bind_SE'_def non_exec_call_0) lemma non_exec_call_1 : -assumes "\ exec_stop \" -shows "(\ \ ( x \ (call_1\<^sub>C M A\<^sub>1); M' x)) = (\ \ (x \ M (A\<^sub>1 \); M' x))" +assumes "\ \" +shows "(\ \ ( x \ (call_1\<^sub>C M (A\<^sub>1)); M' x)) = (\ \ (x \ M (A\<^sub>1 \); M' x))" by (simp add: assms bind_SE'_def call\<^sub>C_def bind_SE_def call_1\<^sub>C_def valid_SE_def) lemma non_exec_call_1' : -assumes "\ exec_stop \" -shows "(\ \ call_1\<^sub>C M A\<^sub>1;- M') = (\ \ M (A\<^sub>1 \);- M')" +assumes "\ \" +shows "(\ \ call_1\<^sub>C M (A\<^sub>1);- M') = (\ \ M (A\<^sub>1 \);- M')" by (simp add: assms bind_SE'_def non_exec_call_1) - +(* general case *) lemma non_exec_call : -assumes "\ exec_stop \" -shows "(\ \ ( x \ (call\<^sub>C M A\<^sub>1); M' x)) = (\ \ (x \ M (A\<^sub>1 \); M' x))" +assumes "\ \" +shows "(\ \ ( x \ (call\<^sub>C M (A\<^sub>1)); M' x)) = (\ \ (x \ M (A\<^sub>1 \); M' x))" by (simp add: assms call\<^sub>C_def bind_SE'_def bind_SE_def call_1\<^sub>C_def valid_SE_def) lemma non_exec_call' : -assumes "\ exec_stop \" -shows "(\ \ call\<^sub>C M A\<^sub>1;- M') = (\ \ M (A\<^sub>1 \);- M')" +assumes "\ \" +shows "(\ \ call\<^sub>C M (A\<^sub>1);- M') = (\ \ M (A\<^sub>1 \);- M')" by (simp add: assms bind_SE'_def non_exec_call) lemma non_exec_call_2 : -assumes "\ exec_stop \" -shows "(\ \ ( _ \ (call_2\<^sub>C M A\<^sub>1 A\<^sub>2); M')) = (\ \ M (A\<^sub>1 \) (A\<^sub>2 \);- M')" +assumes "\ \" +shows "(\ \ ( _ \ (call_2\<^sub>C M (A\<^sub>1) (A\<^sub>2)); M')) = (\ \ M (A\<^sub>1 \) (A\<^sub>2 \);- M')" by (simp add: assms bind_SE'_def bind_SE_def call_2\<^sub>C_def valid_SE_def) lemma non_exec_call_2' : -assumes "\ exec_stop \" -shows "(\ \ call_2\<^sub>C M A\<^sub>1 A\<^sub>2;- M') = (\ \ M (A\<^sub>1 \) (A\<^sub>2 \);- M')" +assumes "\ \" +shows "(\ \ call_2\<^sub>C M (A\<^sub>1) (A\<^sub>2);- M') = (\ \ M (A\<^sub>1 \) (A\<^sub>2 \);- M')" by (simp add: assms bind_SE'_def non_exec_call_2) subsection\Conditional. \ lemma exec_If\<^sub>C_If\<^sub>S\<^sub>E : -assumes "\ exec_stop \" -shows " ((if\<^sub>C P then B\<^sub>1 else B\<^sub>2 fi))\ = ((if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi)) \ " +assumes "\ \" +shows "((if\<^sub>C P then B\<^sub>1 else B\<^sub>2 fi))\ = ((if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi)) \ " unfolding if_SE_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def by (simp add: assms bind_SE_def if_C_def) lemma valid_exec_If\<^sub>C : -assumes "\ exec_stop \" -shows "(\ \ (if\<^sub>C P then B\<^sub>1 else B\<^sub>2 fi);-M) = (\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi);-M)" +assumes "\ \" +shows "(\ \ (if\<^sub>C P then B\<^sub>1 else B\<^sub>2 fi);-M) = (\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi);-M)" by (meson assms exec_If\<^sub>C_If\<^sub>S\<^sub>E valid_bind'_cong) lemma exec_If\<^sub>C' : assumes "exec_stop \" -shows "(\ \ (if\<^sub>C P then B\<^sub>1 else B\<^sub>2 fi);-M) = (\ \ M)" +shows "(\ \ (if\<^sub>C P then B\<^sub>1 else B\<^sub>2 fi);-M) = (\ \ M)" unfolding if_SE_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def bind_SE_def by (simp add: assms if_C_def) lemma exec_While\<^sub>C' : assumes "exec_stop \" shows "(\ \ (while\<^sub>C P do B\<^sub>1 od);-M) = (\ \ M)" unfolding while_C_def MonadSE.if_SE_def Symbex_MonadSE.valid_SE_def MonadSE.bind_SE'_def bind_SE_def apply simp using assms by blast -lemma if\<^sub>C_cond_cong : "f \ = g \ \ - (if\<^sub>C f then c else d fi) \ = - (if\<^sub>C g then c else d fi) \" +lemma if\<^sub>C_cond_cong : "f \ = g \ \ (if\<^sub>C f then c else d fi) \ = + (if\<^sub>C g then c else d fi) \" unfolding if_C_def by simp subsection\Break - Rules. \ -lemma break_assign_skip [simp]: "break ;- assign f = break" +lemma break_assign_skip [simp]: "(break ;- assign f) = break" apply(rule ext) unfolding break_def assign_def exec_stop_def bind_SE'_def bind_SE_def by auto -lemma break_if_skip [simp]: "break ;- (if\<^sub>C b then c else d fi) = break" +lemma break_if_skip [simp]: "(break ;- if\<^sub>C b then c else d fi) = break" apply(rule ext) unfolding break_def assign_def exec_stop_def if_C_def bind_SE'_def bind_SE_def by auto -lemma break_while_skip [simp]: "break ;- (while\<^sub>C b do c od) = break" +lemma break_while_skip [simp]: "(break ;- while\<^sub>C b do c od) = break" apply(rule ext) unfolding while_C_def skip\<^sub>S\<^sub>E_def unit_SE_def bind_SE'_def bind_SE_def break_def exec_stop_def by simp lemma unset_break_idem [simp] : - "( unset_break_status ;- unset_break_status ;- M) = (unset_break_status ;- M)" + "(unset_break_status ;- unset_break_status ;- M) = (unset_break_status ;- M)" apply(rule ext) unfolding unset_break_status_def bind_SE'_def bind_SE_def by auto lemma return_cancel1_idem [simp] : - "( return\<^sub>C X E ;- assign_global X E' ;- M) = ( return\<^sub>C X E ;- M)" + "(return\<^bsub>X\<^esub>(E) ;- X :==\<^sub>G E' ;- M) = ( return\<^sub>C X E ;- M)" apply(rule ext, rename_tac "\") unfolding unset_break_status_def bind_SE'_def bind_SE_def - assign_def return\<^sub>C_def assign_global_def assign_local_def + assign_def return\<^sub>C_def return\<^sub>C0_def assign_global_def assign_local_def apply(case_tac "exec_stop \") apply auto by (simp add: exec_stop_def set_return_status_def) lemma return_cancel2_idem [simp] : - "( return\<^sub>C X E ;- assign_local X E' ;- M) = ( return\<^sub>C X E ;- M)" + "( return\<^bsub>X\<^esub>(E) ;- X :==\<^sub>L E' ;- M) = ( return\<^sub>C X E ;- M)" apply(rule ext, rename_tac "\") unfolding unset_break_status_def bind_SE'_def bind_SE_def - assign_def return\<^sub>C_def assign_global_def assign_local_def + assign_def return\<^sub>C_def return\<^sub>C0_def assign_global_def assign_local_def apply(case_tac "exec_stop \") apply auto by (simp add: exec_stop_def set_return_status_def) subsection\While. \ lemma while\<^sub>C_skip [simp]: "(while\<^sub>C (\ x. False) do c od) = skip\<^sub>S\<^sub>E" apply(rule ext) unfolding while_C_def skip\<^sub>S\<^sub>E_def unit_SE_def apply auto unfolding exec_stop_def skip\<^sub>S\<^sub>E_def unset_break_status_def bind_SE'_def unit_SE_def bind_SE_def by simp txt\ Various tactics for various coverage criteria \ definition while_k :: "nat \ (('\_ext) control_state_ext \ bool) \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E \ (unit, ('\_ext) control_state_ext)MON\<^sub>S\<^sub>E" where "while_k _ \ while_C" text\Somewhat amazingly, this unfolding lemma crucial for symbolic execution still holds ... Even in the presence of break or return...\ lemma exec_while\<^sub>C : "(\ \ ((while\<^sub>C b do c od) ;- M)) = (\ \ ((if\<^sub>C b then c ;- ((while\<^sub>C b do c od) ;- unset_break_status) else skip\<^sub>S\<^sub>E fi) ;- M))" proof (cases "exec_stop \") case True then show ?thesis by (simp add: True exec_If\<^sub>C' exec_While\<^sub>C') next case False then show ?thesis proof (cases "\ b \") case True then show ?thesis apply(subst valid_bind'_cong) using \\ exec_stop \\ apply simp_all apply (auto simp: skip\<^sub>S\<^sub>E_def unit_SE_def) apply(subst while_C_def, simp) apply(subst bind'_cong) apply(subst MonadSE.while_SE_unfold) apply(subst if\<^sub>S\<^sub>E_cond_cong [of _ _ "\_. False"]) apply simp_all apply(subst if\<^sub>C_cond_cong [of _ _ "\_. False"], simp add: ) apply(subst exec_If\<^sub>C_If\<^sub>S\<^sub>E,simp_all) by (simp add: exec_stop_def unset_break_status_def) next case False have * : "b \" using False by auto then show ?thesis unfolding while_k_def apply(subst while_C_def) apply(subst if_C_def) apply(subst valid_bind'_cong) apply (simp add: \\ exec_stop \\) apply(subst (2) valid_bind'_cong) apply (simp add: \\ exec_stop \\) apply(subst MonadSE.while_SE_unfold) apply(subst valid_bind'_cong) apply(subst bind'_cong) apply(subst if\<^sub>S\<^sub>E_cond_cong [of _ _ "\_. True"]) apply(simp_all add: \\ exec_stop \\ ) apply(subst bind_assoc', subst bind_assoc') proof(cases "c \") case None then show "(\ \ c;-((while\<^sub>S\<^sub>E (\\. \ exec_stop \ \ b \) do c od);-unset_break_status);-M) = (\ \ c;-(while\<^sub>C b do c od) ;- unset_break_status ;- M)" by (simp add: bind_SE'_def exec_bind_SE_failure) next case (Some a) then show "(\ \ c ;- ((while\<^sub>S\<^sub>E (\\. \ exec_stop \ \ b \) do c od);-unset_break_status);-M) = (\ \ c ;- (while\<^sub>C b do c od) ;- unset_break_status ;- M)" apply(insert \c \ = Some a\, subst (asm) surjective_pairing[of a]) apply(subst exec_bind_SE_success2, assumption) apply(subst exec_bind_SE_success2, assumption) proof(cases "exec_stop (snd a)") case True then show "(snd a \((while\<^sub>S\<^sub>E (\\. \ exec_stop \ \ b \) do c od);-unset_break_status);-M)= (snd a \ (while\<^sub>C b do c od) ;- unset_break_status ;- M)" by (metis (no_types, lifting) bind_assoc' exec_While\<^sub>C' exec_skip if_SE_D2' skip\<^sub>S\<^sub>E_def while_SE_unfold) next case False then show "(snd a \ ((while\<^sub>S\<^sub>E(\\. \exec_stop \ \ b \) do c od);-unset_break_status);-M)= (snd a \ (while\<^sub>C b do c od) ;- unset_break_status ;- M)" unfolding while_C_def by(subst (2) valid_bind'_cong,simp)(simp) qed qed qed qed (* ... although it is, oh my god, amazingly complex to prove. *) lemma while_k_SE : "while_C = while_k k" by (simp only: while_k_def) corollary exec_while_k : "(\ \ ((while_k (Suc n) b c) ;- M)) = (\ \ ((if\<^sub>C b then c ;- (while_k n b c) ;- unset_break_status else skip\<^sub>S\<^sub>E fi) ;- M))" by (metis exec_while\<^sub>C while_k_def) txt\ Necessary prerequisite: turning ematch and dmatch into a proper Isar Method. \ (* TODO : this code shoud go to TestGen Method setups *) ML\ local fun method_setup b tac = Method.setup b (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o K (tac ctxt rules)))) in val _ = Theory.setup ( method_setup @{binding ematch} ematch_tac "fast elimination matching" #> method_setup @{binding dmatch} dmatch_tac "fast destruction matching" #> method_setup @{binding match} match_tac "resolution based on fast matching") end \ lemmas exec_while_kD = exec_while_k[THEN iffD1] end \ No newline at end of file diff --git a/thys/Clean/src/Hoare_Clean.thy b/thys/Clean/src/Hoare_Clean.thy --- a/thys/Clean/src/Hoare_Clean.thy +++ b/thys/Clean/src/Hoare_Clean.thy @@ -1,263 +1,255 @@ (****************************************************************************** * 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. ******************************************************************************) (* * A Hoare Calculus for Clean * - * Authors : Burkhart Wolff + * Author : Burkhart Wolff + * *) theory Hoare_Clean imports Hoare_MonadSE Clean begin subsection\Clean Control Rules\ lemma break1: "\\\. P (\ \ break_status := True \) \ break \\r \. P \ \ break_status \ \" unfolding hoare\<^sub>3_def break_def unit_SE_def by auto lemma unset_break1: "\\\. P (\ \ break_status := False \) \ unset_break_status \\r \. P \ \ \ break_status \ \" unfolding hoare\<^sub>3_def unset_break_status_def unit_SE_def by auto lemma set_return1: "\\\. P (\ \ return_status := True \) \ set_return_status \\r \. P \ \ return_status \ \" unfolding hoare\<^sub>3_def set_return_status_def unit_SE_def by auto lemma unset_return1: "\\\. P (\ \ return_status := False \) \ unset_return_status \\r \. P \ \ \return_status \ \" unfolding hoare\<^sub>3_def unset_return_status_def unit_SE_def by auto subsection\Clean Skip Rules\ lemma assign_global_skip: -"\\\. exec_stop \ \ P \ \ assign_global upd rhs \\r \. exec_stop \ \ P \ \" +"\\\. exec_stop \ \ P \ \ upd :==\<^sub>G rhs \\r \. exec_stop \ \ P \ \" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def by (simp add: assign_def assign_global_def) lemma assign_local_skip: -"\\\. exec_stop \ \ P \ \ assign_local upd rhs \\r \. exec_stop \ \ P \ \" +"\\\. exec_stop \ \ P \ \ upd :==\<^sub>L rhs \\r \. exec_stop \ \ P \ \" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def by (simp add: assign_def assign_local_def) lemma return_skip: "\\\. exec_stop \ \ P \ \ return\<^sub>C upd rhs \\r \. exec_stop \ \ P \ \" - unfolding hoare\<^sub>3_def return\<^sub>C_def unit_SE_def assign_local_def assign_def bind_SE'_def bind_SE_def + unfolding hoare\<^sub>3_def return\<^sub>C_def return\<^sub>C0_def unit_SE_def assign_local_def assign_def + bind_SE'_def bind_SE_def by auto lemma assign_clean_skip: "\\\. exec_stop \ \ P \ \ assign tr \\r \. exec_stop \ \ P \ \" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def by (simp add: assign_def assign_def) lemma if_clean_skip: "\\\. exec_stop \ \ P \ \ if\<^sub>C C then E else F fi \\r \. exec_stop \ \ P \ \" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def if_SE_def by (simp add: if_C_def) lemma while_clean_skip: "\\\. exec_stop \ \ P \ \ while\<^sub>C cond do body od \\r \. exec_stop \ \ P \ \" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def while_C_def by auto lemma if_opcall_skip: "\\\. exec_stop \ \ P \\ (call\<^sub>C M A\<^sub>1) \\r \. exec_stop \ \ P \\" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def call\<^sub>C_def by simp lemma if_funcall_skip: "\\\. exec_stop \ \ P \\(p\<^sub>t\<^sub>m\<^sub>p \ call\<^sub>C fun E ; assign_local upd (\\. p\<^sub>t\<^sub>m\<^sub>p)) \\r \. exec_stop \ \ P \\" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def call\<^sub>C_def assign_local_def assign_def by (simp add: bind_SE_def) lemma if_funcall_skip': "\\\. exec_stop \ \ P \ \(p\<^sub>t\<^sub>m\<^sub>p \ call\<^sub>C fun E ; assign_global upd (\\. p\<^sub>t\<^sub>m\<^sub>p)) \\r \. exec_stop \ \ P \ \" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def call\<^sub>C_def assign_global_def assign_def by (simp add: bind_SE_def) subsection\Clean Assign Rules\ lemma assign_global: assumes * : "\ upd" - shows "\\\. \exec_stop \ \ P (upd (\_. rhs \) \) \ - assign_global upd rhs - \\r \. \exec_stop \ \ P \ \" + shows "\\\. \ \ \ P (upd (\_. rhs \) \) \ upd :==\<^sub>G rhs \\r \. \ \ \ P \ \" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def assign_global_def assign_def by(auto simp: assms) +find_theorems "\ _ " + lemma assign_local: - assumes * : "\ (upd \ map_hd)" - shows "\\\. \ exec_stop \ \ P ((upd \ map_hd) (\_. rhs \) \) \ - assign_local upd rhs - \\r \. \ exec_stop \ \ P \ \" + assumes * : "\ (upd \ upd_hd)" + shows "\\\. \ \ \ P ((upd \ upd_hd) (\_. rhs \) \) \ upd :==\<^sub>L rhs \\r \. \ \ \ P \ \" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def assign_local_def assign_def using assms exec_stop_vs_control_independence by fastforce lemma return_assign: - assumes * : "\ (upd \ map_hd)" - shows "\\ \. \ exec_stop \ \ P ((upd \ map_hd) (\_. rhs \) (\ \ return_status := True \))\ - return\<^sub>C upd rhs - \\r \. P \ \ return_status \ \" - unfolding return\<^sub>C_def hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def assign_local_def assign_def + assumes * : "\ (upd \ upd_hd)" + shows "\\ \. \ \ \ P ((upd \ upd_hd) (\_. rhs \) (\ \ return_status := True \))\ + return\<^bsub>upd\<^esub>(rhs) + \\r \. P \ \ return_status \ \" + unfolding return\<^sub>C_def return\<^sub>C0_def hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def assign_local_def assign_def set_return_status_def bind_SE'_def bind_SE_def proof (auto) fix \ :: "'b control_state_scheme" - assume a1: "P (upd (map_hd (\_. rhs \)) (\\return_status := True\))" - assume "\ exec_stop \" - show "P (upd (map_hd (\_. rhs \)) \\return_status := True\)" + assume a1: "P (upd (upd_hd (\_. rhs \)) (\\return_status := True\))" + assume "\ \" + show "P (upd (upd_hd (\_. rhs \)) \\return_status := True\)" using a1 assms exec_stop_vs_control_independence' by fastforce - qed +qed (* do we need independence of rhs ? Not really. 'Normal' programs would never be control-state dependent, and 'artificial' ones would still be correct ...*) subsection\Clean Construct Rules\ lemma cond_clean : - " \\\. \ exec_stop \ \ P \ \ cond \\ M \Q\ - \ \\\. \ exec_stop \ \ P \ \ \ cond \\ M' \Q\ - \ \\\. \ exec_stop \ \ P \\ if\<^sub>C cond then M else M' fi\Q\" + " \\\. \ \ \ P \ \ cond \\ M \Q\ + \ \\\. \ \ \ P \ \ \ cond \\ M' \Q\ + \ \\\. \ \ \ P \\ if\<^sub>C cond then M else M' fi\Q\" unfolding hoare\<^sub>3_def hoare\<^sub>3'_def bind_SE_def if_SE_def by (simp add: if_C_def) text\There is a particular difficulty with a verification of (terminating) while rules in a Hoare-logic for a language involving break. The first is, that break is not used in the toplevel of a body of a loop (there might be breaks inside an inner loop, though). This scheme is covered by the rule below, which is a generalisation of the classical while loop (as presented by @{thm while}.\ lemma while_clean_no_break : assumes * : "\\\. \ break_status \ \ cond \ \ P \\ M \\_. \\. \ break_status \ \ P \ \" and measure: "\\. \ exec_stop \ \ cond \ \ P \ \ M \ \ None \ f(snd(the(M \))) < ((f \)::nat) " (is "\\. _ \ cond \ \ P \ \ ?decrease \") - shows "\\\. \ exec_stop \ \ P \\ + shows "\\\. \ \ \ P \\ while\<^sub>C cond do M od \\_ \. (return_status \ \ \ cond \) \ \ break_status \ \ P \\" (is "\?pre\ while\<^sub>C cond do M od \\_ \. ?post1 \ \ ?post2 \\") unfolding while_C_def hoare\<^sub>3_def hoare\<^sub>3'_def proof (simp add: hoare\<^sub>3_def[symmetric],rule sequence') show "\?pre\ - while\<^sub>S\<^sub>E (\\. \ exec_stop \ \ cond \) do M od - \\_ \. \ (\ exec_stop \ \ cond \) \ \ break_status \ \ P \\" + while\<^sub>S\<^sub>E (\\. \ \ \ cond \) do M od + \\_ \. \ ( \ \ \ cond \) \ \ break_status \ \ P \\" (is "\?pre\ while\<^sub>S\<^sub>E ?cond' do M od \\_ \. \ ( ?cond' \) \ ?post2 \\") proof (rule consequence_unit) fix \ show " ?pre \ \ ?post2 \" using exec_stop1 by blast next show "\?post2\while\<^sub>S\<^sub>E ?cond' do M od\\x \. \(?cond' \) \ ?post2 \\" proof (rule_tac f = "f" in while, rule consequence_unit) fix \ show "?cond' \ \ ?post2 \ \ \break_status \ \ cond \ \ P \" by simp next show "\\\. \ break_status \ \ cond \ \ P \\ M \\x \. ?post2 \\" using "*" by blast next fix \ show "?post2 \ \ ?post2 \" by blast next show "\\.?cond' \ \ ?post2 \ \ ?decrease \" using measure by blast qed next fix \ show " \?cond' \ \ ?post2 \ \ \?cond' \ \ ?post2 \" by blast qed next - show "\\\. \ (\ exec_stop \ \ cond \) \ ?post2 \\ unset_break_status + show "\\\. \ (\ \ \ cond \) \ ?post2 \\ unset_break_status \\_ \'. (return_status \' \ \ cond \') \ ?post2 \'\" (is "\\\. \ (?cond'' \) \ ?post2 \\ unset_break_status \\_ \'. ?post3 \' \ ?post2 \' \") proof (rule consequence_unit) fix \ show "\ ?cond'' \ \ ?post2 \ \ (\\. P \ \ ?post3 \) (\\break_status := False\)" by (metis (full_types) exec_stop_def surjective update_convs(1)) next show "\\\. (\\. P \ \ ?post3 \) (\\break_status := False\)\ unset_break_status \\x \. ?post3 \ \ \ break_status \ \ P \\" apply(subst (2) conj_commute,subst conj_assoc,subst (2) conj_commute) by(rule unset_break1) next fix \ show "?post3 \ \ ?post2 \ \ ?post3 \ \ ?post2 \" by simp qed qed text\In the following we present a version allowing a break inside the body, which implies that the invariant has been established at the break-point and the condition is irrelevant. A return may occur, but the @{term "break_status"} is guaranteed to be true after leaving the loop.\ lemma while_clean': - assumes M_inv : "\\\. \ exec_stop \ \ cond \ \ P \\ M \\_. P\" + assumes M_inv : "\\\. \ \ \ cond \ \ P \\ M \\_. P\" and cond_idpc : "\x \. (cond (\\break_status := x\)) = cond \ " and inv_idpc : "\x \. (P (\\break_status := x\)) = P \ " - and f_is_measure : "\\. \ exec_stop \ \ cond \ \ P \ \ - M \ \ None \ f(snd(the(M \))) < ((f \)::nat) " -shows "\\\. \ exec_stop \ \ P \\ - while\<^sub>C cond do M od - \\_ \. \ break_status \ \ P \\" + and f_is_measure : "\\. \ \ \ cond \ \ P \ \ M \ \ None \ f(snd(the(M \))) < ((f \)::nat)" +shows "\\\. \ \ \ P \\ while\<^sub>C cond do M od \\_ \. \ break_status \ \ P \\" unfolding while_C_def hoare\<^sub>3_def hoare\<^sub>3'_def proof (simp add: hoare\<^sub>3_def[symmetric], rule sequence') - show "\\\. \ exec_stop \ \ P \\ - while\<^sub>S\<^sub>E (\\. \ exec_stop \ \ cond \) do M od + show "\\\. \ \ \ P \\ + while\<^sub>S\<^sub>E (\\. \ \ \ cond \) do M od \\_ \. P (\\break_status := False\)\" apply(rule consequence_unit, rule impI, erule conjunct2) apply(rule_tac f = "f" in while) using M_inv f_is_measure inv_idpc by auto next show "\\\. P (\\break_status := False\)\ unset_break_status \\x \. \ break_status \ \ P \\" apply(subst conj_commute) by(rule Hoare_Clean.unset_break1) qed text\Consequence and Sequence rules where inherited from the underlying Hoare-Monad theory.\ end - - - - - diff --git a/thys/Clean/src/Hoare_MonadSE.thy b/thys/Clean/src/Hoare_MonadSE.thy --- a/thys/Clean/src/Hoare_MonadSE.thy +++ b/thys/Clean/src/Hoare_MonadSE.thy @@ -1,304 +1,304 @@ (****************************************************************************** * 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. ******************************************************************************) (* * Basic Hoare Calculus for the State Exception Monad * * Authors : Burkhart Wolff *) theory Hoare_MonadSE imports Symbex_MonadSE begin section\Hoare\ definition hoare\<^sub>3 :: "('\ \ bool) \ ('\, '\)MON\<^sub>S\<^sub>E \ ('\ \ '\ \ bool) \ bool" ("(\(1_)\/ (_)/ \(1_)\)" 50) where "\P\ M \Q\ \ (\\. P \ \ (case M \ of None => False | Some(x, \') => Q x \'))" definition hoare\<^sub>3' :: "('\ \ bool) \ ('\, '\)MON\<^sub>S\<^sub>E \ bool" ("(\(1_)\/ (_)/\)" 50) where "\P\ M \ \ (\\. P \ \ (case M \ of None => True | _ => False))" subsection\Basic rules\ lemma skip: " \P\ skip\<^sub>S\<^sub>E \\_. P\" unfolding hoare\<^sub>3_def skip\<^sub>S\<^sub>E_def unit_SE_def by auto lemma fail: "\P\ fail\<^sub>S\<^sub>E \" unfolding hoare\<^sub>3'_def fail_SE_def unit_SE_def by auto lemma assert: "\P\ assert\<^sub>S\<^sub>E P \\ _ _. True\" unfolding hoare\<^sub>3_def assert_SE_def unit_SE_def by auto lemma assert_conseq: "Collect P \ Collect Q \ \P\ assert\<^sub>S\<^sub>E Q \\ _ _. True\" unfolding hoare\<^sub>3_def assert_SE_def unit_SE_def by auto lemma assume_conseq: assumes "\ \. Q \" shows "\P\ assume\<^sub>S\<^sub>E Q \\ _ . Q\" unfolding hoare\<^sub>3_def assume_SE_def unit_SE_def apply (auto simp : someI2) using assms by auto text \assignment missing in the calculus because this is viewed as a state specific operation, definable for concrete instances of @{typ "'\"}.\ subsection \Generalized and special sequence rules\ text\The decisive idea is to factor out the post-condition on the results of @{term M} :\ lemma sequence : " \P\ M \\x \. x\A \ Q x \\ \ \x\A. \Q x\ M' x \R\ \ \P\ x \ M; M' x \R\" unfolding hoare\<^sub>3_def bind_SE_def by(auto,erule_tac x="\" in allE, auto split: Option.option.split_asm Option.option.split) lemma sequence_irpt_l : "\P\ M \ \ \P\ x \ M; M' x \" unfolding hoare\<^sub>3'_def bind_SE_def by(auto,erule_tac x="\" in allE, auto split: Option.option.split_asm Option.option.split) lemma sequence_irpt_r : "\P\ M \\x \. x\A \ Q x \\ \ \x\A. \Q x\ M' x \ \ \P\ x \ M; M' x \" unfolding hoare\<^sub>3'_def hoare\<^sub>3_def bind_SE_def by(auto,erule_tac x="\" in allE, auto split: Option.option.split_asm Option.option.split) lemma sequence' : "\P\ M \\_. Q \ \ \Q\ M' \R\ \ \P\ M;- M' \R\" unfolding hoare\<^sub>3_def hoare\<^sub>3_def bind_SE_def bind_SE'_def by(auto,erule_tac x="\" in allE, auto split: Option.option.split_asm Option.option.split) lemma sequence_irpt_l' : "\P\ M \ \ \P\ M;- M' \" unfolding hoare\<^sub>3'_def bind_SE_def bind_SE'_def by(auto,erule_tac x="\" in allE, auto split: Option.option.split_asm Option.option.split) lemma sequence_irpt_r' : "\P\ M \\_. Q \ \ \Q\ M' \ \ \P\ M;- M' \" unfolding hoare\<^sub>3'_def hoare\<^sub>3_def bind_SE_def bind_SE'_def by(auto,erule_tac x="\" in allE, auto split: Option.option.split_asm Option.option.split) subsection\Generalized and special consequence rules\ lemma consequence : " Collect P \ Collect P' \ \P'\ M \\x \. x\A \ Q' x \\ \ \ x\A. Collect(Q' x) \ Collect (Q x) \ \P\ M \\x \. x\A \ Q x \\" unfolding hoare\<^sub>3_def bind_SE_def by(auto,erule_tac x="\" in allE,auto split: Option.option.split_asm Option.option.split) lemma consequence_unit : assumes "(\ \. P \ \ P' \)" and "\P'\ M \\x::unit. \ \. Q' \\" and " (\ \. Q' \ \ Q \)" shows "\P\ M \\x \. Q \\" proof - have * : "(\x \. Q \) = (\x::unit. \ \. x\UNIV \ Q \) " by auto show ?thesis apply(subst *) apply(rule_tac P' = "P'" and Q' = "%_. Q'" in consequence) apply (simp add: Collect_mono assms(1)) using assms(2) apply auto[1] by (simp add: Collect_mono assms(3)) qed lemma consequence_irpt : " Collect P \ Collect P' \ \P'\ M \ \ \P\ M \" unfolding hoare\<^sub>3_def hoare\<^sub>3'_def bind_SE_def by(auto) lemma consequence_mt_swap : "(\\_. False\ M \) = (\\_. False\ M \P\)" unfolding hoare\<^sub>3_def hoare\<^sub>3'_def bind_SE_def by auto subsection\Condition rules\ lemma cond : " \\\. P \ \ cond \\ M \Q\ \ \\\. P \ \ \ cond \\ M' \Q\ \ \P\if\<^sub>S\<^sub>E cond then M else M' fi\Q\" unfolding hoare\<^sub>3_def hoare\<^sub>3'_def bind_SE_def if_SE_def by auto lemma cond_irpt : " \\\. P \ \ cond \\ M \ \ \\\. P \ \ \ cond \\ M' \ \ \P\if\<^sub>S\<^sub>E cond then M else M' fi \" unfolding hoare\<^sub>3_def hoare\<^sub>3'_def bind_SE_def if_SE_def by auto text\ Note that the other four combinations can be directly derived via the @{thm consequence_mt_swap} rule.\ subsection\While rules\ text\The only non-trivial proof is, of course, the while loop rule. Note that non-terminating loops were mapped to @{term None} following the principle that our monadic state-transformers represent partial functions in the mathematical sense.\ lemma while : assumes * : "\\\. cond \ \ P \\ M \\_. P\" and measure: "\\. cond \ \ P \ \ M \ \ None \ f(snd(the(M \))) < ((f \)::nat) " shows "\P\while\<^sub>S\<^sub>E cond do M od \\_ \. \cond \ \ P \\" unfolding hoare\<^sub>3_def hoare\<^sub>3'_def bind_SE_def if_SE_def proof auto have * : "\n. \ \. P \ \ f \ \ n \ (case (while\<^sub>S\<^sub>E cond do M od) \ of None \ False | Some (x, \') \ \ cond \' \ P \')" (is "\n. ?P n") proof (rule allI, rename_tac n, induct_tac n) fix n show "?P 0" apply(auto) apply(subst while_SE_unfold) by (metis (no_types, lifting) gr_implies_not0 if_SE_def measure option.case_eq_if option.sel option.simps(3) prod.sel(2) split_def unit_SE_def) next fix n show " ?P n \ ?P (Suc n)" apply(auto,subst while_SE_unfold) apply(case_tac "\cond \") apply (simp add: if_SE_def unit_SE_def) apply(simp add: if_SE_def) apply(case_tac "M \ = None") using measure apply blast proof (auto simp: bind_SE'_def bind_SE_def) fix \ \' assume 1 : "cond \" and 2 : "M \ = Some ((), \')" and 3 : " P \" and 4 : " f \ \ Suc n" and hyp : "?P n" have 5 : "P \'" by (metis (no_types, lifting) * 1 2 3 case_prodD hoare\<^sub>3_def option.simps(5)) have 6 : "snd(the(M \)) = \'" by (simp add: 2) have 7 : "cond \' \ f \' \ n" using 1 3 4 6 leD measure by auto show "case (while\<^sub>S\<^sub>E cond do M od) \' of None \ False | Some (xa, \') \ \ cond \' \ P \'" using 1 3 4 5 6 hyp measure by auto qed qed show "\\. P \ \ case (while\<^sub>S\<^sub>E cond do M od) \ of None \ False | Some (x, \') \ \ cond \' \ P \'" using "*" by blast qed lemma while_irpt : assumes * : "\\\. cond \ \ P \\ M \\_. P\ \ \\\. cond \ \ P \\ M \" and measure: "\\. cond \ \ P \ \ M \ = None \ f(snd(the(M \))) < ((f \)::nat)" and enabled: "\\. P \ \ cond \" shows "\P\while\<^sub>S\<^sub>E cond do M od \" unfolding hoare\<^sub>3_def hoare\<^sub>3'_def bind_SE_def if_SE_def proof auto have * : "\n. \ \. P \ \ f \ \ n \ (case (while\<^sub>S\<^sub>E cond do M od) \ of None \ True | Some a \ False)" (is "\n. ?P n ") proof (rule allI, rename_tac n, induct_tac n) fix n have 1 : "\\. P \ \ cond \" by (simp add: enabled * ) show "?P 0 " apply(auto,frule 1) by (metis assms(2) bind_SE'_def bind_SE_def gr_implies_not0 if_SE_def option.case(1) option.case_eq_if while_SE_unfold) next fix k n assume hyp : "?P n" have 1 : "\\. P \ \ cond \" by (simp add: enabled * ) show "?P (Suc n) " apply(auto, frule 1) apply(subst while_SE_unfold, auto simp: if_SE_def) proof(insert *,simp_all add: hoare\<^sub>3_def hoare\<^sub>3'_def, erule disjE) fix \ assume "P \" and "f \ \ Suc n" and "cond \" and ** : "\\. cond \ \ P \ \ (case M \ of None \ False | Some (x, \') \ P \')" obtain "(case M \ of None \ False | Some (x, \') \ P \')" by (simp add: "**" \P \\ \cond \\) then show "case (M ;- (while\<^sub>S\<^sub>E cond do M od)) \ of None \ True | Some a \ False" apply(case_tac "M \", auto, rename_tac \', simp add: bind_SE'_def bind_SE_def) proof - fix \' assume "P \'" and "M \ = Some ((), \')" have "cond \'" by (simp add: \P \'\ enabled) have "f \' \ n" using \M \ = Some ((), \')\ \P \\ \cond \\ \f \ \ Suc n\ measure by fastforce show "case (while\<^sub>S\<^sub>E cond do M od) \' of None \ True | Some a \ False" using hyp by (simp add: \P \'\ \f \' \ n\) qed next fix \ assume "P \" and "f \ \ Suc n" and "cond \" and * : "\\. cond \ \ P \ \ (case M \ of None \ True | Some a \ False)" obtain ** : "(case M \ of None \ True | Some a \ False)" by (simp add: "*" \P \\ \cond \\) have "M \ = None" by (simp add: "**" option.disc_eq_case(1)) show "case (M ;- (while\<^sub>S\<^sub>E cond do M od)) \ of None \ True | Some a \ False" by (simp add: \M \ = None\ bind_SE'_def bind_SE_def) qed qed show "\\. P \ \ case (while\<^sub>S\<^sub>E cond do M od) \ of None \ True | Some a \ False" using * by blast qed subsection\Experimental Alternative Definitions (Transformer-Style Rely-Guarantee)\ definition hoare\<^sub>1 :: "('\ \ bool) \ ('\, '\)MON\<^sub>S\<^sub>E \ ('\ \ '\ \ bool) \ bool" ("\\<^sub>1 ({(1_)}/ (_)/ {(1_)})" 50) -where "(\\<^sub>1{P} M {Q} ) = (\\. \ \ (_ \ assume\<^sub>S\<^sub>E P ; x \ M; assert\<^sub>S\<^sub>E (Q x)))" +where "(\\<^sub>1{P} M {Q} ) = (\\. (\ \ (_ \ assume\<^sub>S\<^sub>E P ; x \ M; assert\<^sub>S\<^sub>E (Q x))))" -(* Problem: Severe Deviation for the case of an unsatisfyabke precondition *) +(* Problem: Severe Deviation for the case of an unsatisfyable precondition *) definition hoare\<^sub>2 :: "('\ \ bool) \ ('\, '\)MON\<^sub>S\<^sub>E \ ('\ \ '\ \ bool) \ bool" ("\\<^sub>2 ({(1_)}/ (_)/ {(1_)})" 50) where "(\\<^sub>2{P} M {Q} ) = (\\. P \ \ (\ \ (x \ M; assert\<^sub>S\<^sub>E (Q x))))" end \ No newline at end of file diff --git a/thys/Clean/src/Lens_Laws.thy b/thys/Clean/src/Lens_Laws.thy new file mode 100644 --- /dev/null +++ b/thys/Clean/src/Lens_Laws.thy @@ -0,0 +1,332 @@ +(******************************************************************************) +(* Project: The Isabelle/UTP Proof System *) +(* File: Lens_Laws *) +(* Authors: Simon Foster and Frank Zeyda *) +(* Authors: Burkhart Wolff (slight modifications) *) +(* Emails: simon.foster@york.ac.uk frank.zeyda@york.ac.uk *) +(******************************************************************************) +(* LAST REVIEWED: 7/12/2016 *) + +text\ This file is an except from the "Optics" module of the AFP + \<^url>\https://www.isa-afp.org/entries/Optics.html\. \ + +section \Core Lens Laws\ + +theory Lens_Laws + imports Main +begin + +subsection \Lens Signature\ + +text \This theory introduces the signature of lenses and indentifies the core algebraic hierarchy of lens + classes, including laws for well-behaved, very well-behaved, and bijective lenses~\cite{Foster07,Fischer2015,Gibbons17}.\ + +record ('a, 'b) lens = + lens_get :: "'b \ 'a" ("get\") + lens_put :: "'b \ 'a \ 'b" ("put\") + +type_notation + lens (infixr "\" 0) + +text \ + \begin{figure} + \begin{center} + \includegraphics[width=6cm]{figures/Lens} + \end{center} + \vspace{-5ex} + \caption{Visualisation of a simple lens} + \label{fig:Lens} + \end{figure} + + A lens $X : \view \lto \src$, for source type $\src$ and view type $\view$, identifies + $\view$ with a subregion of $\src$~\cite{Foster07,Foster09}, as illustrated in Figure~\ref{fig:Lens}. The arrow denotes + $X$ and the hatched area denotes the subregion $\view$ it characterises. Transformations on + $\view$ can be performed without affecting the parts of $\src$ outside the hatched area. The lens + signature consists of a pair of functions $\lget_X : \src \Rightarrow \view$ that extracts a view + from a source, and $\lput_X : \src \Rightarrow \view \Rightarrow \src$ that updates a view within + a given source. \ + +named_theorems lens_defs + +text \ \lens_source\ gives the set of constructible sources; that is those that can be built + by putting a value into an arbitrary source. \ + +definition lens_source :: "('a \ 'b) \ 'b set" ("\\") where +"lens_source X = {s. \ v s'. s = put\<^bsub>X\<^esub> s' v}" + +abbreviation some_source :: "('a \ 'b) \ 'b" ("src\") where +"some_source X \ (SOME s. s \ \\<^bsub>X\<^esub>)" + +definition lens_create :: "('a \ 'b) \ 'a \ 'b" ("create\") where +[lens_defs]: "create\<^bsub>X\<^esub> v = put\<^bsub>X\<^esub> (src\<^bsub>X\<^esub>) v" + +text \ Function $\lcreate_X~v$ creates an instance of the source type of $X$ by injecting $v$ + as the view, and leaving the remaining context arbitrary. \ + +subsection \Weak Lenses\ + +text \ Weak lenses are the least constrained class of lenses in our algebraic hierarchy. They + simply require that the PutGet law~\cite{Foster09,Fischer2015} is satisfied, meaning that + $\lget$ is the inverse of $\lput$. \ + +locale weak_lens = + fixes x :: "'a \ 'b" (structure) + assumes put_get: "get (put \ v) = v" +begin + lemma source_nonempty: "\ s. s \ \" + by (auto simp add: lens_source_def) + + lemma put_closure: "put \ v \ \" + by (auto simp add: lens_source_def) + + lemma create_closure: "create v \ \" + by (simp add: lens_create_def put_closure) + + lemma src_source [simp]: "src \ \" + using some_in_eq source_nonempty by auto + + lemma create_get: "get (create v) = v" + by (simp add: lens_create_def put_get) + + lemma create_inj: "inj create" + by (metis create_get injI) + + text \ The update function is analogous to the record update function which lifts a function + on a view type to one on the source type. \ + + definition update :: "('a \ 'a) \ ('b \ 'b)" where + [lens_defs]: "update f \ = put \ (f (get \))" + + lemma get_update: "get (update f \) = f (get \)" + by (simp add: put_get update_def) + + lemma view_determination: + assumes "put \ u = put \ v" + shows "u = v" + by (metis assms put_get) + + lemma put_inj: "inj (put \)" + by (simp add: injI view_determination) +end + +declare weak_lens.put_get [simp] +declare weak_lens.create_get [simp] + +subsection \Well-behaved Lenses\ + +text \ Well-behaved lenses add to weak lenses that requirement that the GetPut law~\cite{Foster09,Fischer2015} + is satisfied, meaning that $\lput$ is the inverse of $\lget$. \ + +locale wb_lens = weak_lens + + assumes get_put: "put \ (get \) = \" +begin + + lemma put_twice: "put (put \ v) v = put \ v" + by (metis get_put put_get) + + lemma put_surjectivity: "\ \ v. put \ v = \" + using get_put by blast + + lemma source_stability: "\ v. put \ v = \" + using get_put by auto + + lemma source_UNIV [simp]: "\ = UNIV" + by (metis UNIV_eq_I put_closure wb_lens.source_stability wb_lens_axioms) + +end + +declare wb_lens.get_put [simp] + +lemma wb_lens_weak [simp]: "wb_lens x \ weak_lens x" + by (simp add: wb_lens_def) + +subsection \ Mainly Well-behaved Lenses \ + +text \ Mainly well-behaved lenses extend weak lenses with the PutPut law that shows how one put + override a previous one. \ + +locale mwb_lens = weak_lens + + assumes put_put: "put (put \ v) u = put \ u" +begin + + lemma update_comp: "update f (update g \) = update (f \ g) \" + by (simp add: put_get put_put update_def) + + text \ Mainly well-behaved lenses give rise to a weakened version of the $get-put$ law, + where the source must be within the set of constructible sources. \ + + lemma weak_get_put: "\ \ \ \ put \ (get \) = \" + by (auto simp add: lens_source_def put_get put_put) + + lemma weak_source_determination: + assumes "\ \ \" "\ \ \" "get \ = get \" "put \ v = put \ v" + shows "\ = \" + by (metis assms put_put weak_get_put) + + lemma weak_put_eq: + assumes "\ \ \" "get \ = k" "put \ u = put \ v" + shows "put \ k = \" + by (metis assms put_put weak_get_put) + + text \ Provides $s$ is constructible, then @{term get} can be uniquely determined from @{term put} \ + + lemma weak_get_via_put: "s \ \ \ get s = (THE v. put s v = s)" + by (rule sym, auto intro!: the_equality weak_get_put, metis put_get) + +end + +declare mwb_lens.put_put [simp] +declare mwb_lens.weak_get_put [simp] + +lemma mwb_lens_weak [simp]: + "mwb_lens x \ weak_lens x" + by (simp add: mwb_lens.axioms(1)) + +subsection \Very Well-behaved Lenses\ + +text \Very well-behaved lenses combine all three laws, as in the literature~\cite{Foster09,Fischer2015}.\ + +locale vwb_lens = wb_lens + mwb_lens +begin + + lemma source_determination: + assumes "get \ = get \" "put \ v = put \ v" + shows "\ = \" + by (metis assms get_put put_put) + + lemma put_eq: + assumes "get \ = k" "put \ u = put \ v" + shows "put \ k = \" + using assms weak_put_eq[of \ k u \ v] by (simp) + + text \ @{term get} can be uniquely determined from @{term put} \ + + lemma get_via_put: "get s = (THE v. put s v = s)" + by (simp add: weak_get_via_put) + +end + +lemma vwb_lens_wb [simp]: "vwb_lens x \ wb_lens x" + by (simp add: vwb_lens_def) + +lemma vwb_lens_mwb [simp]: "vwb_lens x \ mwb_lens x" + using vwb_lens_def by auto + +subsection \ Ineffectual Lenses \ + +text \Ineffectual lenses can have no effect on the view type -- application of the $\lput$ function + always yields the same source. They are thus, trivially, very well-behaved lenses.\ + +locale ief_lens = weak_lens + + assumes put_inef: "put \ v = \" +begin + +sublocale vwb_lens +proof + fix \ v u + show "put \ (get \) = \" + by (simp add: put_inef) + show "put (put \ v) u = put \ u" + by (simp add: put_inef) +qed + +lemma ineffectual_const_get: + "\ v. \ \\\. get \ = v" + using put_get put_inef by auto + +end + +abbreviation "eff_lens X \ (weak_lens X \ (\ ief_lens X))" + +subsection \ Bijective Lenses \ + +text \Bijective lenses characterise the situation where the source and view type are equivalent: + in other words the view type full characterises the whole source type. It is often useful + when the view type and source type are syntactically different, but nevertheless correspond + precisely in terms of what they observe. Bijective lenses are formulates using + the strong GetPut law~\cite{Foster09,Fischer2015}.\ + +locale bij_lens = weak_lens + + assumes strong_get_put: "put \ (get \) = \" +begin + +sublocale vwb_lens +proof + fix \ v u + show "put \ (get \) = \" + by (simp add: strong_get_put) + show "put (put \ v) u = put \ u" + by (metis bij_lens.strong_get_put bij_lens_axioms put_get) +qed + + lemma put_bij: "bij_betw (put \) UNIV UNIV" + by (metis bijI put_inj strong_get_put surj_def) + + lemma put_is_create: "\ \ \ \ put \ v = create v" + by (metis create_get strong_get_put) + + lemma get_create: "\ \ \ \ create (get \) = \" + by (simp add: lens_create_def strong_get_put) + +end + +declare bij_lens.strong_get_put [simp] +declare bij_lens.get_create [simp] + +lemma bij_lens_weak [simp]: + "bij_lens x \ weak_lens x" + by (simp_all add: bij_lens_def) + +lemma bij_lens_vwb [simp]: "bij_lens x \ vwb_lens x" + by (metis bij_lens.strong_get_put bij_lens_weak mwb_lens.intro mwb_lens_axioms.intro vwb_lens_def wb_lens.intro wb_lens_axioms.intro weak_lens.put_get) + +subsection \Lens Independence\ + +text \ + \begin{figure} + \begin{center} + \includegraphics[width=6cm]{figures/Independence} + \end{center} + \vspace{-5ex} + \caption{Lens Independence} + \label{fig:Indep} + \end{figure} + + Lens independence shows when two lenses $X$ and $Y$ characterise disjoint regions of the + source type, as illustrated in Figure~\ref{fig:Indep}. We specify this by requiring that the $\lput$ + functions of the two lenses commute, and that the $\lget$ function of each lens is unaffected by + application of $\lput$ from the corresponding lens. \ + +locale lens_indep = + fixes X :: "'a \ 'c" and Y :: "'b \ 'c" + assumes lens_put_comm: "put\<^bsub>X\<^esub> (put\<^bsub>Y\<^esub> \ v) u = put\<^bsub>Y\<^esub> (put\<^bsub>X\<^esub> \ u) v" + and lens_put_irr1: "get\<^bsub>X\<^esub> (put\<^bsub>Y\<^esub> \ v) = get\<^bsub>X\<^esub> \" + and lens_put_irr2: "get\<^bsub>Y\<^esub> (put\<^bsub>X\<^esub> \ u) = get\<^bsub>Y\<^esub> \" + +notation lens_indep (infix "\" 50) + +lemma lens_indepI: + "\ \ u v \. lens_put x (lens_put y \ v) u = lens_put y (lens_put x \ u) v; + \ v \. lens_get x (lens_put y \ v) = lens_get x \; + \ u \. lens_get y (lens_put x \ u) = lens_get y \ \ \ x \ y" + by (simp add: lens_indep_def) + +text \Lens independence is symmetric.\ + +lemma lens_indep_sym: "x \ y \ y \ x" + by (simp add: lens_indep_def) + +lemma lens_indep_sym': "(x \ y) = (y \ x)" + by (auto simp: lens_indep_def) + + +lemma lens_indep_comm: + "x \ y \ lens_put x (lens_put y \ v) u = lens_put y (lens_put x \ u) v" + by (simp add: lens_indep_def) + +lemma lens_indep_get [simp]: + assumes "x \ y" + shows "lens_get x (lens_put y \ v) = lens_get x \" + using assms lens_indep_def by fastforce + +end \ No newline at end of file diff --git a/thys/Clean/src/MonadSE.thy b/thys/Clean/src/MonadSE.thy --- a/thys/Clean/src/MonadSE.thy +++ b/thys/Clean/src/MonadSE.thy @@ -1,400 +1,400 @@ (***************************************************************************** * Clean * * HOL-TestGen --- theorem-prover based test case generation * http://www.brucker.ch/projects/hol-testgen/ * * Copyright (c) 2005-2007 ETH Zurich, Switzerland * 2009-2017 Univ. Paris-Sud, France * 2009-2012 Achim D. Brucker, Germany * 2015-2017 University Sheffield, UK * 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. ******************************************************************************) (* * Monads --- a base testing theory for sequential computations. * This file is part of HOL-TestGen. *) theory MonadSE imports Main begin section\Definition : Standard State Exception Monads\ text\State exception monads in our sense are a direct, pure formulation of automata with a partial transition function.\ subsection\Definition : Core Types and Operators\ type_synonym ('o, '\) MON\<^sub>S\<^sub>E = "'\ \ ('o \ '\)" (* = '\ \ ('o \ '\)option *) definition bind_SE :: "('o,'\)MON\<^sub>S\<^sub>E \ ('o \ ('o','\)MON\<^sub>S\<^sub>E) \ ('o','\)MON\<^sub>S\<^sub>E" where "bind_SE f g = (\\. case f \ of None \ None | Some (out, \') \ g out \')" notation bind_SE ("bind\<^sub>S\<^sub>E") syntax (xsymbols) "_bind_SE" :: "[pttrn,('o,'\)MON\<^sub>S\<^sub>E,('o','\)MON\<^sub>S\<^sub>E] \ ('o','\)MON\<^sub>S\<^sub>E" ("(2 _ \ _; _)" [5,8,8]8) translations "x \ f; g" == "CONST bind_SE f (% x . g)" definition unit_SE :: "'o \ ('o, '\)MON\<^sub>S\<^sub>E" ("(result _)" 8) where "unit_SE e = (\\. Some(e,\))" notation unit_SE ("unit\<^sub>S\<^sub>E") text\In the following, we prove the required Monad-laws\ lemma bind_right_unit[simp]: "(x \ m; result x) = m" apply (simp add: unit_SE_def bind_SE_def) apply (rule ext) apply (case_tac "m \", simp_all) done lemma bind_left_unit [simp]: "(x \ result c; P x) = P c" by (simp add: unit_SE_def bind_SE_def) lemma bind_assoc[simp]: "(y \ (x \ m; k x); h y) = (x \ m; (y \ k x; h y))" apply (simp add: unit_SE_def bind_SE_def, rule ext) apply (case_tac "m \", simp_all) apply (case_tac "a", simp_all) done subsection\Definition : More Operators and their Properties\ definition fail_SE :: "('o, '\)MON\<^sub>S\<^sub>E" where "fail_SE = (\\. None)" notation fail_SE ("fail\<^sub>S\<^sub>E") definition assert_SE :: "('\ \ bool) \ (bool, '\)MON\<^sub>S\<^sub>E" where "assert_SE P = (\\. if P \ then Some(True,\) else None)" notation assert_SE ("assert\<^sub>S\<^sub>E") definition assume_SE :: "('\ \ bool) \ (unit, '\)MON\<^sub>S\<^sub>E" where "assume_SE P = (\\. if \\ . P \ then Some((), SOME \ . P \) else None)" notation assume_SE ("assume\<^sub>S\<^sub>E") lemma bind_left_fail_SE[simp] : "(x \ fail\<^sub>S\<^sub>E; P x) = fail\<^sub>S\<^sub>E" by (simp add: fail_SE_def bind_SE_def) text\We also provide a "Pipe-free" - variant of the bind operator. Just a "standard" programming sequential operator without output frills.\ (* TODO: Eliminate/Modify this. Is a consequence of the Monad-Instantiation. *) -definition bind_SE' :: "('\, '\)MON\<^sub>S\<^sub>E \ ('\, '\)MON\<^sub>S\<^sub>E \ ('\, '\)MON\<^sub>S\<^sub>E" (infixr ";-" 60) -where "f ;- g = (_ \ f ; g)" +definition bind_SE' :: "('\, '\)MON\<^sub>S\<^sub>E \ ('\, '\)MON\<^sub>S\<^sub>E \ ('\, '\)MON\<^sub>S\<^sub>E" (infixr ";-" 10) +where "(f ;- g) = (_ \ f ; g)" -lemma bind_assoc'[simp]: "((m;- k);- h ) = (m;- (k;- h))" +lemma bind_assoc'[simp]: "((m ;- k);- h ) = (m;- (k;- h))" by(simp add:bind_SE'_def) lemma bind_left_unit' [simp]: "((result c);- P) = P" by (simp add: bind_SE'_def) lemma bind_left_fail_SE'[simp]: "(fail\<^sub>S\<^sub>E;- P) = fail\<^sub>S\<^sub>E" by (simp add: bind_SE'_def) lemma bind_right_unit'[simp]: "(m;- (result ())) = m" by (simp add: bind_SE'_def) text\The bind-operator in the state-exception monad yields already a semantics for the concept of an input sequence on the meta-level:\ lemma syntax_test: "(o1 \ f1 ; o2 \ f2; result (post o1 o2)) = X" oops definition yield\<^sub>C :: "('a \ 'b) \ ('b,'a ) MON\<^sub>S\<^sub>E" where "yield\<^sub>C f \ (\\. Some(f \, \))" definition try_SE :: "('o,'\) MON\<^sub>S\<^sub>E \ ('o option,'\) MON\<^sub>S\<^sub>E" ("try\<^sub>S\<^sub>E") where "try\<^sub>S\<^sub>E ioprog = (\\. case ioprog \ of None \ Some(None, \) | Some(outs, \') \ Some(Some outs, \'))" text\In contrast, mbind as a failure safe operator can roughly be seen as a foldr on bind - try: m1 ; try m2 ; try m3; ... Note, that the rough equivalence only holds for certain predicates in the sequence - length equivalence modulo None, for example. However, if a conditional is added, the equivalence can be made precise:\ text\On this basis, a symbolic evaluation scheme can be established that reduces mbind-code to try\_SE\_code and ite-cascades.\ definition alt_SE :: "[('o, '\)MON\<^sub>S\<^sub>E, ('o, '\)MON\<^sub>S\<^sub>E] \ ('o, '\)MON\<^sub>S\<^sub>E" (infixl "\\<^sub>S\<^sub>E" 10) where "(f \\<^sub>S\<^sub>E g) = (\ \. case f \ of None \ g \ | Some H \ Some H)" definition malt_SE :: "('o, '\)MON\<^sub>S\<^sub>E list \ ('o, '\)MON\<^sub>S\<^sub>E" where "malt_SE S = foldr alt_SE S fail\<^sub>S\<^sub>E" notation malt_SE ("\\<^sub>S\<^sub>E") lemma malt_SE_mt [simp]: "\\<^sub>S\<^sub>E [] = fail\<^sub>S\<^sub>E" by(simp add: malt_SE_def) lemma malt_SE_cons [simp]: "\\<^sub>S\<^sub>E (a # S) = (a \\<^sub>S\<^sub>E (\\<^sub>S\<^sub>E S))" by(simp add: malt_SE_def) subsection\Definition : Programming Operators and their Properties\ definition "skip\<^sub>S\<^sub>E = unit\<^sub>S\<^sub>E ()" definition if_SE :: "['\ \ bool, ('\, '\)MON\<^sub>S\<^sub>E, ('\, '\)MON\<^sub>S\<^sub>E] \ ('\, '\)MON\<^sub>S\<^sub>E" where "if_SE c E F = (\\. if c \ then E \ else F \)" syntax (xsymbols) "_if_SE" :: "['\ \ bool,('o,'\)MON\<^sub>S\<^sub>E,('o','\)MON\<^sub>S\<^sub>E] \ ('o','\)MON\<^sub>S\<^sub>E" ("(if\<^sub>S\<^sub>E _ then _ else _fi)" [5,8,8]8) translations "(if\<^sub>S\<^sub>E cond then T1 else T2 fi)" == "CONST if_SE cond T1 T2" subsection\Theory of a Monadic While\ text\Prerequisites\ fun replicator :: "[('a, '\)MON\<^sub>S\<^sub>E, nat] \ (unit, '\)MON\<^sub>S\<^sub>E" (infixr "^^^" 60) where "f ^^^ 0 = (result ())" | "f ^^^ (Suc n) = (f ;- f ^^^ n)" fun replicator2 :: "[('a, '\)MON\<^sub>S\<^sub>E, nat, ('b, '\)MON\<^sub>S\<^sub>E] \ ('b, '\)MON\<^sub>S\<^sub>E" (infixr "^:^" 60) where "(f ^:^ 0) M = (M )" | "(f ^:^ (Suc n)) M = (f ;- ((f ^:^ n) M))" text\First Step : Establishing an embedding between partial functions and relations\ (* plongement *) definition Mon2Rel :: "(unit, '\)MON\<^sub>S\<^sub>E \ ('\ \ '\) set" where "Mon2Rel f = {(x, y). (f x = Some((), y))}" (* ressortir *) definition Rel2Mon :: " ('\ \ '\) set \ (unit, '\)MON\<^sub>S\<^sub>E " where "Rel2Mon S = (\ \. if \\'. (\, \') \ S then Some((), SOME \'. (\, \') \ S) else None)" lemma Mon2Rel_Rel2Mon_id: assumes det:"single_valued R" shows "(Mon2Rel \ Rel2Mon) R = R" apply (simp add: comp_def Mon2Rel_def Rel2Mon_def,auto) apply (case_tac "\\'. (a, \') \ R", auto) apply (subst (2) some_eq_ex) using det[simplified single_valued_def] by auto lemma Rel2Mon_Id: "(Rel2Mon \ Mon2Rel) x = x" apply (rule ext) apply (auto simp: comp_def Mon2Rel_def Rel2Mon_def) apply (erule contrapos_pp, drule HOL.not_sym, simp) done lemma single_valued_Mon2Rel: "single_valued (Mon2Rel B)" by (auto simp: single_valued_def Mon2Rel_def) text\Second Step : Proving an induction principle allowing to establish that lfp remains deterministic\ (* A little complete partial order theory due to Tobias Nipkow *) definition chain :: "(nat \ 'a set) \ bool" where "chain S = (\i. S i \ S(Suc i))" lemma chain_total: "chain S ==> S i \ S j \ S j \ S i" by (metis chain_def le_cases lift_Suc_mono_le) definition cont :: "('a set => 'b set) => bool" where "cont f = (\S. chain S \ f(UN n. S n) = (UN n. f(S n)))" lemma mono_if_cont: fixes f :: "'a set \ 'b set" assumes "cont f" shows "mono f" proof fix a b :: "'a set" assume "a \ b" let ?S = "\n::nat. if n=0 then a else b" have "chain ?S" using \a \ b\ by(auto simp: chain_def) hence "f(UN n. ?S n) = (UN n. f(?S n))" using assms by (metis cont_def) moreover have "(UN n. ?S n) = b" using \a \ b\ by (auto split: if_splits) moreover have "(UN n. f(?S n)) = f a \ f b" by (auto split: if_splits) ultimately show "f a \ f b" by (metis Un_upper1) qed lemma chain_iterates: fixes f :: "'a set \ 'a set" assumes "mono f" shows "chain(\n. (f^^n) {})" proof- { fix n have "(f ^^ n) {} \ (f ^^ Suc n) {}" using assms by(induction n) (auto simp: mono_def) } thus ?thesis by(auto simp: chain_def) qed theorem lfp_if_cont: assumes "cont f" shows "lfp f = (\n. (f ^^ n) {})" (is "_ = ?U") proof show "lfp f \ ?U" proof (rule lfp_lowerbound) have "f ?U = (UN n. (f^^Suc n){})" using chain_iterates[OF mono_if_cont[OF assms]] assms by(simp add: cont_def) also have "\ = (f^^0){} \ \" by simp also have "\ = ?U" apply(auto simp del: funpow.simps) by (metis empty_iff funpow_0 old.nat.exhaust) finally show "f ?U \ ?U" by simp qed next { fix n p assume "f p \ p" have "(f^^n){} \ p" proof(induction n) case 0 show ?case by simp next case Suc from monoD[OF mono_if_cont[OF assms] Suc] \f p \ p\ show ?case by simp qed } thus "?U \ lfp f" by(auto simp: lfp_def) qed lemma single_valued_UN_chain: assumes "chain S" "(!!n. single_valued (S n))" shows "single_valued(UN n. S n)" proof(auto simp: single_valued_def) fix m n x y z assume "(x, y) \ S m" "(x, z) \ S n" with chain_total[OF assms(1), of m n] assms(2) show "y = z" by (auto simp: single_valued_def) qed lemma single_valued_lfp: fixes f :: "('a \ 'a) set \ ('a \ 'a) set" assumes "cont f" "\r. single_valued r \ single_valued (f r)" shows "single_valued(lfp f)" unfolding lfp_if_cont[OF assms(1)] proof(rule single_valued_UN_chain[OF chain_iterates[OF mono_if_cont[OF assms(1)]]]) fix n show "single_valued ((f ^^ n) {})" by(induction n)(auto simp: assms(2)) qed text\Third Step: Definition of the Monadic While \ \\ definition \ :: "['\ \ bool,('\ \ '\) set] \ (('\ \ '\) set \ ('\ \ '\) set)" where "\ b cd = (\cw. {(s,t). if b s then (s, t) \ cd O cw else s = t})" definition while_SE :: "['\ \ bool, (unit, '\)MON\<^sub>S\<^sub>E] \ (unit, '\)MON\<^sub>S\<^sub>E" where "while_SE c B \ (Rel2Mon(lfp(\ c (Mon2Rel B))))" syntax (xsymbols) "_while_SE" :: "['\ \ bool, (unit, '\)MON\<^sub>S\<^sub>E] \ (unit, '\)MON\<^sub>S\<^sub>E" ("(while\<^sub>S\<^sub>E _ do _ od)" [8,8]8) translations "while\<^sub>S\<^sub>E c do b od" == "CONST while_SE c b" lemma cont_\: "cont (\ c b)" by (auto simp: cont_def \_def) text\The fixpoint theory now allows us to establish that the lfp constructed over @{term Mon2Rel} remains deterministic\ theorem single_valued_lfp_Mon2Rel: "single_valued (lfp(\ c (Mon2Rel B)))" apply(rule single_valued_lfp, simp_all add: cont_\) apply(auto simp: \_def single_valued_def) apply(metis single_valued_Mon2Rel[of "B"] single_valued_def) done lemma Rel2Mon_if: "Rel2Mon {(s, t). if b s then (s, t) \ Mon2Rel c O lfp (\ b (Mon2Rel c)) else s = t} \ = (if b \ then Rel2Mon (Mon2Rel c O lfp (\ b (Mon2Rel c))) \ else Some ((), \))" by (simp add: Rel2Mon_def) lemma Rel2Mon_homomorphism: assumes determ_X: "single_valued X" and determ_Y: "single_valued Y" - shows "Rel2Mon (X O Y) = (Rel2Mon X) ;- (Rel2Mon Y)" + shows "Rel2Mon (X O Y) = ((Rel2Mon X) ;- (Rel2Mon Y))" proof - have relational_partial_next_in_O: "\x E F. (\y. (x, y) \ (E O F)) \ (\y. (x, y) \ E)" by (auto) have some_eq_intro: "\ X x y . single_valued X \ (x, y) \ X \ (SOME y. (x, y) \ X) = y" by (auto simp: single_valued_def) show ?thesis apply (simp add: Rel2Mon_def bind_SE'_def bind_SE_def) apply (rule ext, rename_tac "\") apply (case_tac " \ \'. (\, \') \ X O Y") apply (simp only: HOL.if_True) apply (frule relational_partial_next_in_O) apply (auto simp: single_valued_relcomp some_eq_intro determ_X determ_Y relcomp.relcompI) by blast qed text\Putting everything together, the theory of embedding and the invariance of determinism of the while-body, gives us the usual unfold-theorem:\ theorem while_SE_unfold: "(while\<^sub>S\<^sub>E b do c od) = (if\<^sub>S\<^sub>E b then (c ;- (while\<^sub>S\<^sub>E b do c od)) else result () fi)" apply (simp add: if_SE_def bind_SE'_def while_SE_def unit_SE_def) apply (subst lfp_unfold [OF mono_if_cont, OF cont_\]) apply (rule ext) apply (subst \_def) apply (auto simp: Rel2Mon_if Rel2Mon_homomorphism bind_SE'_def Rel2Mon_Id [simplified comp_def] single_valued_Mon2Rel single_valued_lfp_Mon2Rel ) done lemma bind_cong : " f \ = g \ \ (x \ f ; M x)\ = (x \ g ; M x)\" unfolding bind_SE'_def bind_SE_def by simp lemma bind'_cong : " f \ = g \ \ (f ;- M )\ = (g ;- M )\" unfolding bind_SE'_def bind_SE_def by simp lemma if\<^sub>S\<^sub>E_True [simp]: "(if\<^sub>S\<^sub>E (\ x. True) then c else d fi) = c" apply(rule ext) by (simp add: MonadSE.if_SE_def) lemma if\<^sub>S\<^sub>E_False [simp]: "(if\<^sub>S\<^sub>E (\ x. False) then c else d fi) = d" apply(rule ext) by (simp add: MonadSE.if_SE_def) lemma if\<^sub>S\<^sub>E_cond_cong : "f \ = g \ \ (if\<^sub>S\<^sub>E f then c else d fi) \ = (if\<^sub>S\<^sub>E g then c else d fi) \" unfolding if_SE_def by simp lemma while\<^sub>S\<^sub>E_skip[simp] : "(while\<^sub>S\<^sub>E (\ x. False) do c od) = skip\<^sub>S\<^sub>E" apply(rule ext,subst MonadSE.while_SE_unfold) by (simp add: MonadSE.if_SE_def skip\<^sub>S\<^sub>E_def) end \ No newline at end of file diff --git a/thys/Clean/src/Optics.thy b/thys/Clean/src/Optics.thy new file mode 100644 --- /dev/null +++ b/thys/Clean/src/Optics.thy @@ -0,0 +1,47 @@ +text\This is an excerpt of the Optics library + \<^url>\https://www.isa-afp.org/entries/Optics.html\ by Frank Zeyda and + Simon Foster. It provides a rich infrastructure for \<^emph>\algebraic lenses\, + an abstract theory allowing to describe parts of memory and their + independence. We use it to abstractly model typed program variables and + framing conditions. + + Optics provides a rich framework for lense compositions and sub-lenses + which we will not use in the context of Clean; even the offered concept + of a list-lense, a possible means to model the stack-infrastructure + required for local variables, is actually richer than needed. + + Since Clean strives for minimality, we restrict ourselves to this "proxy" + theory for Optics. +\ + +theory Optics + imports Lens_Laws +begin + + +fun upd_hd :: "('a \ 'a) \ 'a list \ 'a list" + where "upd_hd f [] = []" + | "upd_hd f (a#S) = f a # S" + +lemma [simp] :"tl (upd_hd f S) = tl S" + by (metis list.sel(3) upd_hd.elims) + + +definition upd2put :: "(('d \ 'b) \ 'a \ 'c) \ 'a \ 'b \ 'c" + where "upd2put f = (\\. \ b. f (\_. b) \)" + +definition create\<^sub>L + where "create\<^sub>L getv updv = \lens_get = getv,lens_put = upd2put updv\" + +definition "hd\<^sub>L = create\<^sub>L hd upd_hd" (* works since no partial lenses needed in Clean*) + +definition "map_nth i = (\f l. list_update l i (f (l ! i)))" + +lemma indep_list_lift : + "X \ create\<^sub>L getv updv + \ (\f \. updv (\_. f (getv \)) \) = updv + \ X \ create\<^sub>L (hd \ getv ) (updv \ upd_hd)" + unfolding create\<^sub>L_def o_def Lens_Laws.lens_indep_def upd2put_def + by (auto,metis (no_types)) (metis (no_types)) + +end \ No newline at end of file diff --git a/thys/Clean/src/Symbex_MonadSE.thy b/thys/Clean/src/Symbex_MonadSE.thy --- a/thys/Clean/src/Symbex_MonadSE.thy +++ b/thys/Clean/src/Symbex_MonadSE.thy @@ -1,566 +1,567 @@ (****************************************************************************** * 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 Symbex_MonadSE imports Seq_MonadSE begin subsection\Definition and Properties of Valid Execution Sequences\ text\A key-notion in our framework is the \emph{valid} execution sequence, \ie{} a sequence that: \begin{enumerate} \item terminates (not obvious since while), \item results in a final @{term True}, \item does not fail globally (but recall the FailSave and FailPurge variants of @{term mbind}-operators, that handle local exceptions in one or another way). \end{enumerate} Seen from an automata perspective (where the monad - operations correspond to the step function), valid execution sequences can be used to model ``feasible paths'' across an automaton.\ -definition valid_SE :: "'\ \ (bool,'\) MON\<^sub>S\<^sub>E \ bool" (infix "\" 15) +definition valid_SE :: "'\ \ (bool,'\) MON\<^sub>S\<^sub>E \ bool" (infix "\" 9) where "(\ \ m) = (m \ \ None \ fst(the (m \)))" text\This notation consideres failures as valid -- a definition inspired by I/O conformance.\ subsubsection\Valid Execution Sequences and their Symbolic Execution\ lemma exec_unit_SE [simp]: "(\ \ (result P)) = (P)" by(auto simp: valid_SE_def unit_SE_def) lemma exec_unit_SE' [simp]: "(\\<^sub>0 \ (\\. Some (f \, \))) = (f \\<^sub>0)" by(simp add: valid_SE_def ) lemma exec_fail_SE [simp]: "(\ \ fail\<^sub>S\<^sub>E) = False" by(auto simp: valid_SE_def fail_SE_def) lemma exec_fail_SE'[simp]: "\(\\<^sub>0 \ (\\. None))" by(simp add: valid_SE_def ) text\The following the rules are in a sense the heart of the entire symbolic execution approach\ lemma exec_bind_SE_failure: "A \ = None \ \(\ \ ((s \ A ; M s)))" by(simp add: valid_SE_def unit_SE_def bind_SE_def) lemma exec_bind_SE_failure2: "A \ = None \ \(\ \ ((A ;- M)))" by(simp add: valid_SE_def unit_SE_def bind_SE_def bind_SE'_def) lemma exec_bind_SE_success: "A \ = Some(b,\') \ (\ \ ((s \ A ; M s))) = (\' \ (M b))" by(simp add: valid_SE_def unit_SE_def bind_SE_def ) lemma exec_bind_SE_success2: "A \ = Some(b,\') \ (\ \ ((A ;- M))) = (\' \ M)" by(simp add: valid_SE_def unit_SE_def bind_SE_def bind_SE'_def ) lemma exec_bind_SE_success': (* atomic boolean Monad "Query Functions" *) "M \ = Some(f \,\) \ (\ \ M) = f \" by(simp add: valid_SE_def unit_SE_def bind_SE_def ) lemma exec_bind_SE_success'': -"\ \ ((s \ A ; M s)) \ \ v \'. the(A \) = (v,\') \ \' \ (M v)" +"\ \ ((s \ A ; M s)) \ \ v \'. the(A \) = (v,\') \ (\' \ M v)" apply(auto simp: valid_SE_def unit_SE_def bind_SE_def) apply(cases "A \", simp_all) apply(drule_tac x="A \" and f=the in arg_cong, simp) apply(rule_tac x="fst aa" in exI) apply(rule_tac x="snd aa" in exI, auto) done lemma exec_bind_SE_success''': -"\ \ ((s \ A ; M s)) \ \ a. (A \) = Some a \ (snd a) \ (M (fst a))" +"\ \ ((s \ A ; M s)) \ \ a. (A \) = Some a \ (snd a \ M (fst a))" apply(auto simp: valid_SE_def unit_SE_def bind_SE_def) apply(cases "A \", simp_all) apply(drule_tac x="A \" and f=the in arg_cong, simp) apply(rule_tac x="fst aa" in exI) apply(rule_tac x="snd aa" in exI, auto) done lemma exec_bind_SE_success'''' : -"\ \ ((s \ A ; M s)) \ \ v \'. A \ = Some(v,\') \ \' \ (M v)" +"\ \ ((s \ A ; M s)) \ \ v \'. A \ = Some(v,\') \ (\' \ M v)" apply(auto simp: valid_SE_def unit_SE_def bind_SE_def) apply(cases "A \", simp_all) apply(drule_tac x="A \" and f=the in arg_cong, simp) apply(rule_tac x="fst aa" in exI) apply(rule_tac x="snd aa" in exI, auto) done lemma valid_bind_cong : " f \ = g \ \ (\ \ (x \ f ; M x)) = (\ \ (x \ g ; M x))" unfolding bind_SE'_def bind_SE_def valid_SE_def by simp lemma valid_bind'_cong : " f \ = g \ \ (\ \ f ;- M) = (\ \ g ;- M)" unfolding bind_SE'_def bind_SE_def valid_SE_def by simp text\Recall \verb+mbind_unit+ for the base case.\ lemma valid_mbind_mt : "(\ \ ( s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e [] f; unit\<^sub>S\<^sub>E (P s))) = P [] " by simp lemma valid_mbind_mtE: "\ \ ( s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e [] f; unit\<^sub>S\<^sub>E (P s)) \ (P [] \ Q) \ Q" by(auto simp: valid_mbind_mt) lemma valid_mbind'_mt : "(\ \ ( s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p [] f; unit\<^sub>S\<^sub>E (P s))) = P [] " by simp lemma valid_mbind'_mtE: "\ \ ( s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p [] f; unit\<^sub>S\<^sub>E (P s)) \ (P [] \ Q) \ Q" by(auto simp: valid_mbind'_mt) lemma valid_mbind''_mt : "(\ \ ( s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e [] f; unit\<^sub>S\<^sub>E (P s))) = P [] " by(simp add: mbind''.simps valid_SE_def bind_SE_def unit_SE_def) lemma valid_mbind''_mtE: "\ \ ( s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e [] f; unit\<^sub>S\<^sub>E (P s)) \ (P [] \ Q) \ Q" by(auto simp: valid_mbind''_mt) lemma exec_mbindFSave_failure: "ioprog a \ = None \ (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e (a#S) ioprog ; M s)) = (\ \ (M []))" by(simp add: valid_SE_def unit_SE_def bind_SE_def) lemma exec_mbindFStop_failure: "ioprog a \ = None \ (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (a#S) ioprog ; M s)) = (False)" by(simp add: exec_bind_SE_failure) lemma exec_mbindFPurge_failure: "ioprog a \ = None \ - (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e (a#S) ioprog ; M s)) = (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e (S) ioprog ; M s))" + (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e (a#S) ioprog ; M s)) = + (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e (S) ioprog ; M s))" by(simp add: valid_SE_def unit_SE_def bind_SE_def mbind''.simps) lemma exec_mbindFSave_success : "ioprog a \ = Some(b,\') \ (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e (a#S) ioprog ; M s)) = (\' \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e S ioprog ; M (b#s)))" unfolding valid_SE_def unit_SE_def bind_SE_def by(cases "mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e S ioprog \'", auto) lemma exec_mbindFStop_success : "ioprog a \ = Some(b,\') \ (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (a#S) ioprog ; M s)) = (\' \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S ioprog ; M (b#s)))" unfolding valid_SE_def unit_SE_def bind_SE_def by(cases "mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S ioprog \'", auto simp: mbind'.simps) lemma exec_mbindFPurge_success : "ioprog a \ = Some(b,\') \ (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e (a#S) ioprog ; M s)) = (\' \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e S ioprog ; M (b#s)))" unfolding valid_SE_def unit_SE_def bind_SE_def by(cases "mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e S ioprog \'", auto simp: mbind''.simps) lemma exec_mbindFSave: "(\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e (a#S) ioprog ; return (P s))) = (case ioprog a \ of None \ (\ \ (return (P []))) | Some(b,\') \ (\' \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e S ioprog ; return (P (b#s)))))" apply(case_tac "ioprog a \") apply(auto simp: exec_mbindFSave_failure exec_mbindFSave_success split: prod.splits) done lemma mbind_eq_sexec: assumes * : "\b \'. f a \ = Some(b,\') \ (os \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S f; P (b#os)) = (os \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S f; P' (b#os))" shows "( a \ f a; x \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S f; P (a # x)) \ = ( a \ f a; x \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S f; P'(a # x)) \" apply(cases "f a \ = None") apply(subst bind_SE_def, simp) apply(subst bind_SE_def, simp) apply auto apply(subst bind_SE_def, simp) apply(subst bind_SE_def, simp) apply(simp add: *) done lemma mbind_eq_sexec': assumes * : "\b \'. f a \ = Some(b,\') \ (P (b))\' = (P' (b))\'" shows "( a \ f a; P (a)) \ = ( a \ f a; P'(a)) \" apply(cases "f a \ = None") apply(subst bind_SE_def, simp) apply(subst bind_SE_def, simp) apply auto apply(subst bind_SE_def, simp) apply(subst bind_SE_def, simp) apply(simp add: *) done lemma mbind'_concat: "(os \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (S@T) f; P os) = (os \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S f; os' \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p T f; P (os @ os'))" proof (rule ext, rename_tac "\", induct S arbitrary: \ P) case Nil show ?case by simp next case (Cons a S) show ?case apply(insert Cons.hyps, simp) by(rule mbind_eq_sexec',simp) qed lemma assert_suffix_inv : "\ \ ( _ \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p xs istep; assert\<^sub>S\<^sub>E (P)) \ \\. P \ \ (\ \ (_ \ istep x; assert\<^sub>S\<^sub>E (P))) \ \ \ ( _ \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (xs @ [x]) istep; assert\<^sub>S\<^sub>E (P))" apply(subst mbind'_concat, simp) unfolding bind_SE_def assert_SE_def valid_SE_def apply(auto split: option.split option.split_asm) apply(case_tac "aa",simp_all) apply(case_tac "P bb",simp_all) apply (metis option.distinct(1)) apply(case_tac "aa",simp_all) apply(case_tac "P bb",simp_all) by (metis option.distinct(1)) text\Universal splitting and symbolic execution rule\ lemma exec_mbindFSave_E: assumes seq : "(\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e (a#S) ioprog ; (P s)))" and none: "ioprog a \ = None \ (\ \ (P [])) \ Q" and some: "\ b \'. ioprog a \ = Some(b,\') \ (\' \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e S ioprog;(P (b#s)))) \ Q " shows "Q" using seq proof(cases "ioprog a \") case None assume ass:"ioprog a \ = None" show "Q" apply(rule none[OF ass]) apply(insert ass, erule_tac ioprog1=ioprog in exec_mbindFSave_failure[THEN iffD1],rule seq) done next case (Some aa) assume ass:"ioprog a \ = Some aa" show "Q" apply(insert ass,cases "aa",simp, rename_tac "out" "\'") apply(erule some) apply(insert ass,simp) apply(erule_tac ioprog1=ioprog in exec_mbindFSave_success[THEN iffD1],rule seq) done qed text\The next rule reveals the particular interest in deduction; as an elimination rule, it allows for a linear conversion of a validity judgement @{term "mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p"} over an input list @{term "S"} into a constraint system; without any branching ... Symbolic execution can even be stopped tactically whenever @{term "ioprog a \ = Some(b,\')"} comes to a contradiction.\ lemma exec_mbindFStop_E: assumes seq : "(\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (a#S) ioprog ; (P s)))" and some: "\b \'. ioprog a \ = Some(b,\') \ (\'\ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S ioprog;(P(b#s)))) \ Q" shows "Q" using seq proof(cases "ioprog a \") case None assume ass:"ioprog a \ = None" show "Q" apply(insert ass seq) apply(drule_tac \=\ and S=S and M=P in exec_mbindFStop_failure, simp) done next case (Some aa) assume ass:"ioprog a \ = Some aa" show "Q" apply(insert ass,cases "aa",simp, rename_tac "out" "\'") apply(erule some) apply(insert ass,simp) apply(erule_tac ioprog1=ioprog in exec_mbindFStop_success[THEN iffD1],rule seq) done qed lemma exec_mbindFPurge_E: assumes seq : "(\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e (a#S) ioprog ; (P s)))" and none: "ioprog a \ = None \ (\ \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e S ioprog;(P (s)))) \ Q" and some: "\ b \'. ioprog a \ = Some(b,\') \ (\' \ (s \ mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>P\<^sub>u\<^sub>r\<^sub>g\<^sub>e S ioprog;(P (b#s)))) \ Q " shows "Q" using seq proof(cases "ioprog a \") case None assume ass:"ioprog a \ = None" show "Q" apply(rule none[OF ass]) apply(insert ass, erule_tac ioprog1=ioprog in exec_mbindFPurge_failure[THEN iffD1],rule seq) done next case (Some aa) assume ass:"ioprog a \ = Some aa" show "Q" apply(insert ass,cases "aa",simp, rename_tac "out" "\'") apply(erule some) apply(insert ass,simp) apply(erule_tac ioprog1=ioprog in exec_mbindFPurge_success[THEN iffD1],rule seq) done qed lemma assert_disch1 :" P \ \ (\ \ (x \ assert\<^sub>S\<^sub>E P; M x)) = (\ \ (M True))" by(auto simp: bind_SE_def assert_SE_def valid_SE_def) lemma assert_disch2 :" \ P \ \ \ (\ \ (x \ assert\<^sub>S\<^sub>E P ; M s))" by(auto simp: bind_SE_def assert_SE_def valid_SE_def) lemma assert_disch3 :" \ P \ \ \ (\ \ (assert\<^sub>S\<^sub>E P))" by(auto simp: bind_SE_def assert_SE_def valid_SE_def) lemma assert_disch4 :" P \ \ (\ \ (assert\<^sub>S\<^sub>E P))" by(auto simp: bind_SE_def assert_SE_def valid_SE_def) lemma assert_simp : "(\ \ assert\<^sub>S\<^sub>E P) = P \" by (meson assert_disch3 assert_disch4) lemmas assert_D = assert_simp[THEN iffD1] (* legacy *) lemma assert_bind_simp : "(\ \ (x \ assert\<^sub>S\<^sub>E P; M x)) = (P \ \ (\ \ (M True)))" by(auto simp: bind_SE_def assert_SE_def valid_SE_def split: HOL.if_split_asm) lemmas assert_bindD = assert_bind_simp[THEN iffD1] (* legacy *) lemma assume_D : "(\ \ (_ \ assume\<^sub>S\<^sub>E P; M)) \ \ \. (P \ \ (\ \ M) )" apply(auto simp: bind_SE_def assume_SE_def valid_SE_def split: HOL.if_split_asm) apply(rule_tac x="Eps P" in exI, auto) apply(subst Hilbert_Choice.someI,assumption,simp) done lemma assume_E : assumes * : "\ \ ( _ \ assume\<^sub>S\<^sub>E P; M) " and ** : "\ \. P \ \ \ \ M \ Q" shows "Q" apply(insert *) by(insert *[THEN assume_D], auto intro: **) lemma assume_E' : assumes * : "\ \ assume\<^sub>S\<^sub>E P ;- M" and ** : "\ \. P \ \ \ \ M \ Q" shows "Q" by(insert *[simplified "bind_SE'_def", THEN assume_D], auto intro: **) text\These two rule prove that the SE Monad in connection with the notion of valid sequence is actually sufficient for a representation of a Boogie-like language. The SBE monad with explicit sets of states --- to be shown below --- is strictly speaking not necessary (and will therefore be discontinued in the development).\ term "if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi" lemma if_SE_D1 : "P \ \ (\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi)) = (\ \ B\<^sub>1)" by(auto simp: if_SE_def valid_SE_def) lemma if_SE_D1' : "P \ \ (\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi);-M) = (\ \ (B\<^sub>1;-M))" by(auto simp: if_SE_def valid_SE_def bind_SE'_def bind_SE_def) lemma if_SE_D2 : "\ P \ \ (\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi)) = (\ \ B\<^sub>2)" by(auto simp: if_SE_def valid_SE_def) lemma if_SE_D2' : "\ P \ \ (\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi);-M) = (\ \ B\<^sub>2;-M)" by(auto simp: if_SE_def valid_SE_def bind_SE'_def bind_SE_def) lemma if_SE_split_asm : "(\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi)) = ((P \ \ (\ \ B\<^sub>1)) \ (\ P \ \ (\ \ B\<^sub>2)))" by(cases "P \",auto simp: if_SE_D1 if_SE_D2) lemma if_SE_split_asm': "(\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi);-M) = ((P \ \ (\ \ B\<^sub>1;-M)) \ (\ P \ \ (\ \ B\<^sub>2;-M)))" by(cases "P \",auto simp: if_SE_D1' if_SE_D2') lemma if_SE_split: "(\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi)) = ((P \ \ (\ \ B\<^sub>1)) \ (\ P \ \ (\ \ B\<^sub>2)))" by(cases "P \", auto simp: if_SE_D1 if_SE_D2) lemma if_SE_split': "(\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi);-M) = ((P \ \ (\ \ B\<^sub>1;-M)) \ (\ P \ \ (\ \ B\<^sub>2;-M)))" by(cases "P \", auto simp: if_SE_D1' if_SE_D2') lemma if_SE_execE: assumes A: "\ \ ((if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi))" and B: "P \ \ \ \ (B\<^sub>1) \ Q" and C: "\ P \\ \ \ (B\<^sub>2) \ Q" shows "Q" by(insert A [simplified if_SE_split],cases "P \", simp_all, auto elim: B C) lemma if_SE_execE': assumes A: "\ \ ((if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi);-M)" and B: "P \ \ \ \ (B\<^sub>1;-M) \ Q" and C: "\ P \\ \ \ (B\<^sub>2;-M) \ Q" shows "Q" by(insert A [simplified if_SE_split'],cases "P \", simp_all, auto elim: B C) lemma exec_while : "(\ \ ((while\<^sub>S\<^sub>E b do c od) ;- M)) = (\ \ ((if\<^sub>S\<^sub>E b then c ;- (while\<^sub>S\<^sub>E b do c od) else unit\<^sub>S\<^sub>E ()fi) ;- M))" apply(subst while_SE_unfold) by(simp add: bind_SE'_def ) lemmas exec_whileD = exec_while[THEN iffD1] lemma if_SE_execE'': "\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi) ;- M \ (P \ \ \ \ B\<^sub>1 ;- M \ Q) \ (\ P \ \ \ \ B\<^sub>2 ;- M \ Q) \ Q" by(auto elim: if_SE_execE') definition "opaque (x::bool) = x" lemma if_SE_execE''_pos: "\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi) ;- M \ (P \ \ \ \ B\<^sub>1 ;- M \ Q) \ (opaque (\ \ (if\<^sub>S\<^sub>E P then B\<^sub>1 else B\<^sub>2 fi) ;- M) \ Q) \ Q" using opaque_def by auto lemma [code]: "(\ \ m) = (case (m \) of None \ False | (Some (x,y)) \ x)" apply(simp add: valid_SE_def) apply(cases "m \ = None", simp_all) apply(insert not_None_eq, auto) done (* for the moment no good idea to state the case where the body eventually crashes. *) lemma "P \ \ (_ \ assume\<^sub>S\<^sub>E P ; x \ M; assert\<^sub>S\<^sub>E (\\. (x=X) \ Q x \))" oops lemma "\\. \ X. \ \ (_ \ assume\<^sub>S\<^sub>E P ; x \ M; assert\<^sub>S\<^sub>E (\\. x=X \ Q x \))" oops lemma monadic_sequence_rule: "\ X \\<^sub>1. (\ \ (_ \ assume\<^sub>S\<^sub>E (\\'. (\=\') \ P \) ; x \ M; assert\<^sub>S\<^sub>E (\\. (x=X) \ (\=\\<^sub>1) \ Q x \))) \ (\\<^sub>1 \ (_ \ assume\<^sub>S\<^sub>E (\\. (\=\\<^sub>1) \ Q x \) ; y \ M'; assert\<^sub>S\<^sub>E (\\. R x y \))) \ \ \ (_ \ assume\<^sub>S\<^sub>E (\\'. (\=\') \ P \) ; x \ M; y \ M'; assert\<^sub>S\<^sub>E (R x y))" apply(elim exE impE conjE) apply(drule assume_D) apply(elim exE impE conjE) unfolding valid_SE_def assume_SE_def assert_SE_def bind_SE_def apply(auto split: if_split HOL.if_split_asm Option.option.split Option.option.split_asm) apply (metis (mono_tags, lifting) option.simps(3) someI_ex) oops lemma "\ X. \ \ (_ \ assume\<^sub>S\<^sub>E P ; x \ M; assert\<^sub>S\<^sub>E (\\. x=X \ Q x \)) \ \ \ (_ \ assume\<^sub>S\<^sub>E P ; x \ M; assert\<^sub>S\<^sub>E (\\. Q x \))" unfolding valid_SE_def assume_SE_def assert_SE_def bind_SE_def by(auto split: if_split HOL.if_split_asm Option.option.split Option.option.split_asm) lemma exec_skip: "(\ \ skip\<^sub>S\<^sub>E ;- M) = (\ \ M)" by (simp add: skip\<^sub>S\<^sub>E_def) lemmas exec_skipD = exec_skip[THEN iffD1] text\Test-Refinements will be stated in terms of the failsave @{term mbind}, opting more generality. The following lemma allows for an optimization both in test execution as well as in symbolic execution for an important special case of the post-codition: Whenever the latter has the constraint that the length of input and output sequence equal each other (that is to say: no failure occured), failsave mbind can be reduced to failstop mbind ...\ lemma mbindFSave_vs_mbindFStop : "(\ \ (os \ (mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e \s ioprog); result(length \s = length os \ P \s os))) = (\ \ (os \ (mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p \s ioprog); result(P \s os)))" apply(rule_tac x=P in spec) apply(rule_tac x=\ in spec) proof(induct "\s") case Nil show ?case by(simp_all add: mbind_try try_SE_def del: Seq_MonadSE.mbind.simps) case (Cons a \s) show ?case apply(rule allI, rename_tac "\",rule allI, rename_tac "P") apply(insert Cons.hyps) apply(case_tac "ioprog a \") apply(simp only: exec_mbindFSave_failure exec_mbindFStop_failure, simp) apply(simp add: split_paired_all del: Seq_MonadSE.mbind.simps ) apply(rename_tac "\'") apply(subst exec_mbindFSave_success, assumption) apply(subst (2) exec_bind_SE_success, assumption) apply(erule_tac x="\'" in allE) apply(erule_tac x="\\s s. P (a # \s) (aa # s)" in allE) (* heureka ! *) apply(simp) done qed lemma mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e_vs_mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p: assumes A: "\ \ \. ioprog \ \ \ None" shows "(\ \ (os \ (mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e \s ioprog); P os)) = (\ \ (os \ (mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p \s ioprog); P os))" proof(induct "\s") case Nil show ?case by simp next case (Cons a \s) from Cons.hyps have B:"\ S f \. mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e S f \ \ None " by simp have C:"\\. mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p \s ioprog \ = mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e \s ioprog \" apply(induct \s, simp) apply(rule allI,rename_tac "\") apply(simp add: Seq_MonadSE.mbind'.simps(2)) apply(insert A, erule_tac x="a" in allE) apply(erule_tac x="\" and P="\\ . ioprog a \ \ None" in allE) apply(auto split:option.split) done show ?case apply(insert A,erule_tac x="a" in allE,erule_tac x="\" in allE) apply(simp, elim exE) apply(rename_tac "out" "\'") apply(insert B, erule_tac x=\s in allE, erule_tac x=ioprog in allE, erule_tac x=\' in allE) apply(subst(asm) not_None_eq, elim exE) apply(subst exec_bind_SE_success) apply(simp split: option.split, auto) apply(rule_tac s="(\ a b c. a # (fst c)) out \' (aa, b)" in trans, simp,rule refl) apply(rule_tac s="(\ a b c. (snd c)) out \' (aa, b)" in trans, simp,rule refl) apply(simp_all) apply(subst exec_bind_SE_success, assumption) apply(subst exec_bind_SE_success) apply(rule_tac s="Some (aa, b)" in trans,simp_all add:C) apply(subst(asm) exec_bind_SE_success, assumption) apply(subst(asm) exec_bind_SE_success) apply(rule_tac s="Some (aa, b)" in trans,simp_all add:C) done qed subsection\Miscellaneous\ no_notation unit_SE ("(result _)" 8) end \ No newline at end of file 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 +theory Test_Clean imports Clean_Symbex "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