Quelle  Examples.thy

(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)
section ‹Examples›

theory Examples
imports
  "../OG_Syntax"
begin

record test =
  x :: nat
  y :: nat

text ‹This is a sequence of two commands, the first being an assign
 protected by two guards. The guards use booleans as their faults.›
definition
  "test_guard ≡ {True} (True, {🍋x=0}),
                       (False, {(0::nat)=0}) ⟼ {True} 🍋y := 0;;
                      {True} 🍋x := 0"

lemma
  "Γ, Θ |⊨_{True}
    COBEGIN test_guard {True},{True}
         ∥ {True} 🍋y:=0 {True}, {True}
    COEND {True},{True}"
  unfolding test_guard_def
  apply oghoare (*11 subgoals*)
           apply simp_all
  done

definition
  "test_try_throw ≡ TRY {True} 🍋y := 0;;
                      {True} THROW
                     CATCH {True} 🍋x := 0
                     END"


subsection ‹Parameterized Examples›

subsubsection ‹Set Elements of an Array to Zero›

record Example1 =
  ex1_a :: "nat ==> nat"

lemma Example1: 
 "Γ, Θ|⊨!!!_F{True}
   COBEGIN SCHEME [0≤i<n] {True} 🍋ex1_a:=🍋ex1_a (i:=0) {🍋ex1_a i=0}, {False} COEND
  {∀i < n. 🍋ex1_a i = 0}, X"
  apply oghoare (* 7 subgoals *)
        apply (simp ; fail)+
 done

text ‹Same example but with a Call.›
definition
   "Example1'a ≡ {True} 🍋ex1_a:=🍋ex1_a (0:=0)"

definition
   "Example1'b ≡ {True} 🍋ex1_a:=🍋ex1_a (1:=0)"

definition "Example1' ≡
  COBEGIN Example1'a {🍋ex1_a 0=0}, {False}
         ∥
         {True} SCALL 0 0
         {🍋ex1_a 1=0}, {False}
  COEND"

definition "Γ' = Map.empty(0 ↦ com Example1'b)"
definition "Θ' = Map.empty(0 :: nat ↦ [ann Example1'b])"

lemma Example1_proc_simp[unfolded Example1'b_def oghoare_simps]:
 "Γ' 0 = Some (com (Example1'b))"
 "Θ' 0 = Some ([ ann(Example1'b)])"
 "[ ann(Example1'b)]!0 = ann(Example1'b)"
 by (simp add: Γ'_def Θ'_def)+

lemma Example1':
notes Example1_proc_simp[proc_simp]
shows
 "Γ', Θ' |⊨_F Example1' {∀i < 2. 🍋ex1_a i = 0}, {False}"
  unfolding Example1'_def 
  apply simp
  unfolding Example1'a_def Example1'b_def
  apply oghoare (*12 subgoals*)
             apply simp+
   using less_2_cases apply blast
  apply simp
  apply (erule disjE ; clarsimp)
done

type_synonym routine = nat

text ‹Same example but with a Call.›
record Example2 =
  ex2_n :: "routine ==> nat"
  ex2_a :: "nat ==> string"

definition
  Example2'n :: "routine ==> (Example2, string × nat, 'f) ann_com"
where
  "Example2'n i ≡ {🍋ex2_n i= i} 🍋ex2_a:=🍋ex2_a((🍋ex2_n i):='''')"

lemma Example2'n_map_of_simps[simp]:
  "i < n ==>
    map_of (map (λi. ((p, i), g i)) [0..<n])
       (p, i) = Some (g i)"
  apply (rule map_of_is_SomeI)
   apply (clarsimp simp: distinct_map o_def)
   apply (meson inj_onI prod.inject)
  apply clarsimp
  done

definition "Γ'' n ≡
  map_of (map (λi. ((''f'', i), com (Example2'n i))) [0..<n])"

definition "Θ'' n ≡
  map_of (map (λi. ((''f'', i), [ann (Example2'n i)])) [0..<n])"

lemma  Example2'n_proc_simp[unfolded Example2'n_def oghoare_simps]:
 "i<n ==> Γ'' n (''f'',i) = Some ( com(Example2'n i))"
 "i<n ==> Θ'' n (''f'',i) = Some ([ ann(Example2'n i)])"
 "[ ann(Example2'n i)]!0 = ann(Example2'n i)"
 by (simp add: Γ''_def Θ''_def)+

lemmas Example2'n_proc_simp[proc_simp add]

lemma Example2:
notes Example2'n_proc_simp[proc_simp]
shows
 "Γ'' n, Θ'' n
 |⊨!!!_F{True}
   COBEGIN SCHEME [0≤i<n]
     {True}
       CALLX (λs. s(ex2_n:=(ex2_n s)(i:=i))) {🍋ex2_n i = i} (''f'', i) 0
       (λs t. t(ex2_n:= (ex2_n t)(i:=(ex2_n s) i))) (λx y. Skip)
       {🍋ex2_a (🍋ex2_n i)='''' ∧ 🍋ex2_n i = i} {🍋ex2_a i=''''} {False} {False}
     {🍋ex2_a i=''''}, {False}
   COEND
  {∀i < n. 🍋ex2_a i = ''''}, {False}"
  unfolding Example2'n_def ann_call_def call_def block_def 
  apply oghoare (* 113 subgoals *)
  apply (clarsimp ; fail)+
 done

lemmas Example2'n_proc_simp[proc_simp del]

text ‹Same example with lists as auxiliary variables.›

record Example2_list =
  ex2_A :: "nat list"

lemma Example2_list: 
 "Γ, Θ |⊨!!!_F{n < length 🍋ex2_A}
   COBEGIN
     SCHEME [0≤i<n] {n < length 🍋ex2_A} 🍋ex2_A:=🍋ex2_A[i:=0] {🍋ex2_A!i=0},{False}
   COEND
    {∀i < n. 🍋ex2_A!i = 0}, X"
  apply oghoare (*7 subgoals*)
        apply force+
 done


lemma exceptions_example:
  "Γ, Θ |⊨_F
   TRY
   {True } 🍋y := 0;;
   { 🍋y = 0 } THROW
   CATCH
     {🍋y = 0} 🍋x := 🍋y + 1
   END
   { 🍋x = 1 ∧ 🍋y = 0}, {False}"
  by oghoare simp_all

lemma guard_example:
  "Γ, Θ |⊨_{42,66}
  {True} (42, {🍋x=0}),
   (66, {🍋y=0}) ⟼ {🍋x = 0}
   🍋y := 0;;
   {True} 🍋x := 0
  { 🍋x = 0}, {False}"
  apply oghoare (*6 subgoals*)
       apply simp_all
 done

subsubsection ‹Peterson's mutex algorithm I (from Hoare-Parallel) ›

text ‹Eike Best. "Semantics of Sequential and Parallel Programs", page 217.›

record Petersons_mutex_1 =
 pr1 :: nat
 pr2 :: nat
 in1 :: bool
 in2 :: bool
 hold :: nat

lemma peterson_thread_1:
 "Γ, Θ |⊨_F {🍋pr1=0 ∧ ¬🍋in1} WHILE True INV {🍋pr1=0 ∧ ¬🍋in1}
  DO
  {🍋pr1=0 ∧ ¬🍋in1} ⟨🍋in1:=True,, 🍋pr1:=1 ⟩;;
  {🍋pr1=1 ∧ 🍋in1} ⟨🍋hold:=1,, 🍋pr1:=2 ⟩;;
  {🍋pr1=2 ∧ 🍋in1 ∧ (🍋hold=1 ∨ 🍋hold=2 ∧ 🍋pr2=2)}
  AWAIT (¬🍋in2 ∨ ¬(🍋hold=1)) THEN
     🍋pr1:=3
  END;;
  {🍋pr1=3 ∧ 🍋in1 ∧ (🍋hold=1 ∨ 🍋hold=2 ∧ 🍋pr2=2)}
   ⟨🍋in1:=False,,🍋pr1:=0⟩
  OD {🍋pr1=0 ∧ ¬🍋in1},{False}
"
  apply oghoare (*7 subgoals*)
        apply (((auto)[1]) ; fail)+
 done


lemma peterson_thread_2:
 "Γ, Θ |⊨_F {🍋pr2=0 ∧ ¬🍋in2}
  WHILE True INV {🍋pr2=0 ∧ ¬🍋in2}
  DO
  {🍋pr2=0 ∧ ¬🍋in2} ⟨🍋in2:=True,, 🍋pr2:=1 ⟩;;
  {🍋pr2=1 ∧ 🍋in2} ⟨ 🍋hold:=2,, 🍋pr2:=2 ⟩ ;;
  {🍋pr2=2 ∧ 🍋in2 ∧ (🍋hold=2 ∨ (🍋hold=1 ∧ 🍋pr1=2))}
  AWAIT (¬🍋in1 ∨ ¬(🍋hold=2)) THEN 🍋pr2:=3 END;;
  {🍋pr2=3 ∧ 🍋in2 ∧ (🍋hold=2 ∨ (🍋hold=1 ∧ 🍋pr1=2))}
    ⟨🍋in2:=False,, 🍋pr2:=0⟩
  OD {🍋pr2=0 ∧ ¬🍋in2},{False}
 "
  apply oghoare (*7 subgoals*)
  by auto

lemma Petersons_mutex_1:
  "Γ, Θ |⊨!!!_F {🍋pr1=0 ∧ ¬🍋in1 ∧ 🍋pr2=0 ∧ ¬🍋in2 }
  COBEGIN
  {🍋pr1=0 ∧ ¬🍋in1 } WHILE True INV {🍋pr1=0 ∧ ¬🍋in1}
  DO
  {🍋pr1=0 ∧ ¬🍋in1} ⟨ 🍋in1:=True,, 🍋pr1:=1 ⟩;;
  {🍋pr1=1 ∧ 🍋in1} ⟨ 🍋hold:=1,, 🍋pr1:=2 ⟩;;
  {🍋pr1=2 ∧ 🍋in1 ∧ (🍋hold=1 ∨ (🍋hold=2 ∧ 🍋pr2=2))}
  AWAIT (¬🍋in2 ∨ ¬(🍋hold=1)) THEN 🍋pr1:=3 END;;
  {🍋pr1=3 ∧ 🍋in1 ∧ (🍋hold=1 ∨ (🍋hold=2 ∧ 🍋pr2=2))}
   ⟨ 🍋in1:=False,, 🍋pr1:=0⟩
  OD {🍋pr1=0 ∧ ¬🍋in1},{False}
  ∥
  {🍋pr2=0 ∧ ¬🍋in2}
  WHILE True INV {🍋pr2=0 ∧ ¬🍋in2}
  DO
  {🍋pr2=0 ∧ ¬🍋in2} ⟨ 🍋in2:=True,, 🍋pr2:=1 ⟩;;
  {🍋pr2=1 ∧ 🍋in2} ⟨ 🍋hold:=2,, 🍋pr2:=2 ⟩ ;;
  {🍋pr2=2 ∧ 🍋in2 ∧ (🍋hold=2 ∨ (🍋hold=1 ∧ 🍋pr1=2))}
  AWAIT (¬🍋in1 ∨ ¬(🍋hold=2)) THEN 🍋pr2:=3 END;;
  {🍋pr2=3 ∧ 🍋in2 ∧ (🍋hold=2 ∨ (🍋hold=1 ∧ 🍋pr1=2))}
    ⟨ 🍋in2:=False,, 🍋pr2:=0⟩
  OD {🍋pr2=0 ∧ ¬🍋in2},{False}
  COEND
  {🍋pr1=0 ∧ ¬🍋in1 ∧ 🍋pr2=0 ∧ ¬🍋in2},{False}"
  apply oghoare
― ‹81 verification conditions.›
  by auto

end