# HG changeset patch
# User ryokka
# Date 1581664787 -32400
# Node ID 36fb80fdcc3ebec4e7e9da8f81fe9e39c731d85c
# Parent  19ab6b8055ea8f4344972ed3111b1451794e6e86
fix paper

diff -r 19ab6b8055ea -r 36fb80fdcc3e paper/hoare.tex
--- a/paper/hoare.tex	Wed Feb 12 05:02:27 2020 +0900
+++ b/paper/hoare.tex	Fri Feb 14 16:19:47 2020 +0900
@@ -10,8 +10,10 @@
 といった形で表される。
 
 Hoare Logic ではプログラムの部分的な正当性を検証することができ、
-事後条件のあとに別の コマンド をつなげてプログラムを構築することで、
-シンプルな計算に対する検証することができる。
+事後条件のあとに別のコマンドをつなげてプログラムを構築することで、
+プログラムに対する検証を行える。
+
+
 
 本章は Agda で実装された Hoare Logic について解説し、
 実際に Hoare Logic を用いた検証を行う。
@@ -31,7 +33,7 @@
 while loop が終了したとき成り立っている条件を $i = 10$
 としている。
 
-同様のプログラムを Hoare Logic 上で同様のプログラムを作成し、検証を行う。
+Hoare Logic 上で同様のプログラムを作成し、検証を行う。
 
 \begin{lstlisting}[caption=while Loop Program,label=c-while]
 n = 10;
diff -r 19ab6b8055ea -r 36fb80fdcc3e slide/slide.md
--- a/slide/slide.md	Wed Feb 12 05:02:27 2020 +0900
+++ b/slide/slide.md	Fri Feb 14 16:19:47 2020 +0900
@@ -624,32 +624,3 @@
   - 並列実行での検証
 
 
-```AGDA
-loopPPSem : (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
-  → (varn input + vari input ≡ c10 input ) → (varn input + vari input ≡ c10 input ) implies (vari output ≡ c10 output)
-loopPPSem input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
-  where
-    lem : (n : ℕ) → (env : Envc) → n + suc (vari env) ≡ suc (n + vari env)
-    lem n env = +-suc (n) (vari env)
-    loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) 
-        →  (loopeq : output ≡ loopPP n current eq)
-      → (whileTestStateP s2 current ) 
-      → (whileTestStateP s2 current ) implies (vari output ≡ c10 output)
-    loopPPSemInduct zero current refl loopeq refl rewrite loopeq = proof (λ x → refl)
-    loopPPSemInduct (suc n) current refl loopeq refl rewrite (sym (lem n current)) =
-        whileLoopPSem current refl
-            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
-            (λ output x → loopPPSemInduct n (record { c10 = n + suc (vari current) ; varn = n ; vari = suc (vari current) }) refl loopeq refl)
-```
-
-```AGDA
-whileLoopPSem : {l : Level} {t : Set l} → (input : Envc ) → varn input + vari input ≡ c10 input 
-    → (next : (output : Envc ) 
-        → (varn input + vari input ≡ c10 input) implies (varn output + vari output ≡ c10 output )  → t)
-    → (exit : (output : Envc ) 
-        → (varn input + vari input ≡ c10 input ) implies (vari env) ≡ (c10 env) → t) → t
-whileLoopPSem env s next exit with varn env | s
-... | zero | _ = exit env (proof (λ z → z))
-... | (suc varn ) | refl = next ( record env { varn = varn ; vari = suc (vari env) } )   
-    (proof λ x → +-suc varn (vari env) )
-```