(****************************************************************************** * 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› "