Theory Examples
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
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
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
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
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
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
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
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
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
by auto
end