Theory IsPrime

(******************************************************************************
 * 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⇩C ‹n < 2›  
            then return⇘local_isPrime_state.result_value_update⇙ ‹False›
            else skip⇩S⇩E 
          fi ;-
          ‹i := 2› ;- 
          while⇩C ‹i < SQRT_UINT_MAX ∧ i*i ≤ n  › 
            do if⇩C ‹n mod i = 0›  
                  then return⇘local_isPrime_state.result_value_update⇙ ‹False›
                  else skip⇩S⇩E 
                fi ;-
                ‹i := i + 1 › 
            od ;-
         return⇘local_isPrime_state.result_value_update⇙ ‹True›"

find_theorems name:isPrime name:core
term‹isPrime_core›
 
lemma XXX : 
"isPrime_core n ≡
     if⇩C (λσ. n < 2) then (return⇘result_value_update⇙ (λσ. False)) 
                     else skip⇩S⇩E fi;-
     i_update :==⇩L (λσ. 2) ;-
     while⇩C (λσ. (hd∘i)σ < SQRT_UINT_MAX ∧ (hd∘i)σ * (hd∘i)σ ≤ n) 
     do
        (if⇩C (λσ. n mod (hd ∘ i) σ = 0) 
         then (return⇘result_value_update⇙ (λσ. False)) 
         else skip⇩S⇩E fi ;-
        i_update :==⇩L (λσ. (hd ∘ i) σ + 1)) 
     od ;-
     return⇘result_value_update⇙ (λσ. True)"

  by(simp add: isPrime_core_def)

lemma YYY:
"isPrime n ≡ block⇩C push_local_isPrime_state 
                    (isPrime_core n) 
                    pop_local_isPrime_state"
  by(simp add: isPrime_def)

lemma isPrime_correct : 
  "⦃λσ.   ▹ σ ∧ isPrime_pre (n)(σ) ∧ σ = σ⇩p⇩r⇩e ⦄ 
     isPrime n 
   ⦃λr σ. ▹ σ ∧ isPrime_post(n) (σ⇩p⇩r⇩e)(σ)(r) ⦄"
   oops



end