Binary file Paper/tecrep.pdf has changed

--- a/Paper/tecrep.tex	Wed Dec 12 18:44:19 2018 +0900
+++ b/Paper/tecrep.tex	Sun Dec 16 18:19:33 2018 +0900
@@ -48,7 +48,7 @@
 \def\BibTeX{{\rmfamily B\kern-.05em{\scshape i\kern-.025em b}\kern-.08em
  T\kern-.1667em\lower.7ex\hbox{E}\kern-.125em X}}
 
-\jtitle{GearsOSのHoare tripleをベースにした検証手法}
+\jtitle{GearsOSのHoare Logicをベースにした検証手法}
 %% \jsubtitle{技術研究報告原稿のための解説とテンプレート}
 %% \etitle{How to Use \LaTeXe\ Class File (\IEICEJcls\ version \IEICEJver) 
 %%         for the Technical Report of the Institute of Electronics, Information 
@@ -94,15 +94,16 @@
 記述する。
 また、継続にはある関数を実行するための事前条件や
 事後条件などをもたせることが可能である。
-Hoare triple では事前条件が成り立っているときにある
+Floyd–Hoare logic (以下 Hoare Logic) は事前条件が成り立っているときにある
 関数を実行して、それが停止する際に事後条件を満た
-すことを確認する。
-これは継続を用いた Agda 上では事前条件を継続で関数
-に渡し、関数からさらに継続した先で事後条件が成り
+すことを確認することで、検証を行うアイディアである。
+これは継続を用いた Agda 上では事前条件とその証明をを継続で関数
+に渡し、関数からさらに継続した先で事後条件とその証明が成り
 立つという形で記述できる。
-本発表では GearsOS の仕様確認に Hoare triple をベースと
+本研究では GearsOS の仕様確認に Hoare Logic をベースと
 した証明を導入し、今まで行っていた証明との比較を
 行う。
+
 \section{GearsOS}
 Gears OS は信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に開発している OSである。
 
@@ -153,7 +154,7 @@
 DataGear に対してメタ計算として証明を行う。証明すべき性質は、不定の型を持つ継続
 \verb+t+ に記述することができる。例えば、 Stack にある値\verb+x+をpushして、pop
 すると \verb+ x'+ が取れてくる。\verb+Just x+ と\verb+Just x'+ は等しい必要があ
-る。これは Agda では \verb+(Just x ≡ x' )+ と記述される。
+る。これは Agda では \verb+(Just x ≡ x')+ と記述される。
 ここで Just とは Agda の以下のデータ構造である。
 
 % \begin{verbatim}
@@ -182,13 +183,181 @@
 
 このように、CodeGear を Agda で記述し、継続部分に証明すべき性質を Agda で記述する。
 
-GearsOS での記述は interface によってモジュール化される。
-よって、このモジュール化もAgda により記述する必要がある。
-CbC で記述された任意の CodeGear と Meta CodeGear が Agda にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。
+%% GearsOS での記述は interface によってモジュール化される。
+%% よって、このモジュール化もAgda により記述する必要がある。
+%% CbC で記述された任意の CodeGear と Meta CodeGear が Agda にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。
+
+\section{HoareLogic}
+HoareLogic とはC.A.R Hoare、 R.W Floyd らによるプログラムの検証のアイディアである。
+これは、
 
 
-\section{AgdaとGearsOS}
-Agda と GearsOS
+\section{AgdaでのHoareLogic}
+本章では、Agda 上での HoareLogic についての記述を行う。
+今回は、\ref{agda-while} のような while Loop に対しての検証を行うこととする。
+
+\begin{lstlisting}[caption=while Loop,label=agda-while]
+  n = 10;
+  i = 0;
+
+  while (n>0)
+  {
+    i++;
+    n--;
+  }
+\end{lstlisting}
+
+\ref{agda-while}では最初期の事前条件は何もなく、プログラムが停止するときの条件として、 $i==10 ∧ n == 0$ が成り立つ。
+また、 $n = 10$、 $i = 0$、 といった代入に事前条件と、事後条件をつけ、 while文 にループの普遍条件をつけることになる。
+
+\ref{agda-hoare} は Agda上での HoareLogic の構築子である。
+
+$Env$ は\ref{agda-while}の n、 i といった変数をまとめたものであり、型として Agda 上での自然数の型である Nat を持つ。
+PrimComm は Primitive Command で、 n、i といった変数に 代入するときに使用される関数である。
+Cond は Condition で、 変数を受け取って　Bool値を返す関数となっている。
+Agda のデータで定義されている Comm は HoareLogic での Command を表す。
+Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。
+
+PComm は PrimComm を受けて Command を返す型で定義されていて、 変数を代入するときに使われる。
+Seq は Sequence で Command を2つ受けて Command を返す型で定義されている。これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。
+If は Cond と Comm を2つ受け取り、 Cond の中身によって Comm を変える Command である。
+While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。
+
+\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare]
+record Env : Set where
+  field
+    varn : ℕ
+    vari : ℕ
+open Env
+
+PrimComm : Set
+PrimComm = Env → Env
+
+Cond : Set
+Cond = (Env → Bool) 
+
+data Comm : Set where
+  Skip  : Comm
+  Abort : Comm
+  PComm : PrimComm -> Comm
+  Seq   : Comm -> Comm -> Comm
+  If    : Cond -> Comm -> Comm -> Comm
+  While : Cond -> Comm -> Comm
+\end{lstlisting}
+
+Agda 上の HoareLogic で使われるプログラムは Comm 型の関数となる。
+プログラムの処理を Seq でつないでいき、最終的な状態にたどり着くと値を返して止まる。
+%% \ref{agda-hoare-simpl} は 変数 $i$、 $n$ に代入を行うプログラムである。
+%% これは Seq で PComm を2つ繋げた形になる。
+\ref{agda-hoare-prog}は\ref{agda-while}で書いた While Loop を HoareLogic での Comm で記述したものである。
+ここでの $\$$は $()$の対応を合わせる Agda の糖衣で、行頭から行末までを $()$で囲っていることと同義である。
+
+\begin{lstlisting}[caption= HoareLogic のプログラム ,label=agda-hoare-prog]
+program : Comm
+program = 
+    Seq ( PComm (λ env → record env {varn = 10}))
+    $ Seq ( PComm (λ env → record env {vari = 0}))
+    $ While (λ env → lt zero (varn env ) )
+      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
+        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
+
+\end{lstlisting}
+
+しかし、 この Comm は Command をならべているだけである。
+そのため、この Command を Agda 上で実行するため、 \ref{agda-hoare-interpret} のような interpreter を記述した。
+\begin{lstlisting}[caption=Agda での HoareLogic interpreter ,label=agda-hoare-interpret]
+{-# TERMINATING #-}
+interpret : Env → Comm → Env
+interpret env Skip = env
+interpret env Abort = env
+interpret env (PComm x) = x env
+interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
+interpret env (If x then else) with x env
+... | true = interpret env then
+... | false = interpret env else
+interpret env (While x comm) with x env
+... | true = interpret (interpret env comm) (While x comm)
+... | false = env
+\end{lstlisting}
+
+\ref{agda-hoare-interpret}は 初期状態の Env と 実行する Command の並びを受けとって、実行後の Env を返すものとなっている。
+
+\begin{lstlisting}[caption=Agda での HoareLogic の実行 ,label=agda-hoare-run]
+test : Env
+test =  interpret ( record { vari = 0  ; varn = 0 } ) programt
+\end{lstlisting}
+\ref{agda-hoare-run}のように interpret に $vari = 0 , varn = 0$ の record を渡し、 実行する Comm を渡して 評価してやると$record { varn = 0 ; vari = 10 }$ のような Env が返ってくる。
+
+
+
+次に先程書いたプログラムの証明について記述する。
+
+\ref{agda-hoare-rule} は Agda 上での HoareLogic での証明の構成である。
+HTProof では Condition と Command もう一つ Condition を受け取って、 Set を返す Agda のデータである。
+-- これは Pre と Post の Condition を Command で変化させる
+
+\begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare-rule]
+data HTProof : Cond -> Comm -> Cond -> Set where
+  PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
+             (pr : Axiom bPre pcm bPost) ->
+             HTProof bPre (PComm pcm) bPost
+  SkipRule : (b : Cond) -> HTProof b Skip b
+  AbortRule : (bPre : Cond) -> (bPost : Cond) ->
+              HTProof bPre Abort bPost
+  WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
+                {bPost' : Cond} -> {bPost : Cond} ->
+                Tautology bPre bPre' ->
+                HTProof bPre' cm bPost' ->
+                Tautology bPost' bPost ->
+                HTProof bPre cm bPost
+  SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
+            {cm2 : Comm} -> {bPost : Cond} ->
+            HTProof bPre cm1 bMid ->
+            HTProof bMid cm2 bPost ->
+            HTProof bPre (Seq cm1 cm2) bPost
+  IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
+           {bPre : Cond} -> {bPost : Cond} ->
+           {b : Cond} ->
+           HTProof (bPre /\ b) cmThen bPost ->
+           HTProof (bPre /\ neg b) cmElse bPost ->
+           HTProof bPre (If b cmThen cmElse) bPost
+  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
+              HTProof (bInv /\ b) cm bInv ->
+              HTProof bInv (While b cm) (bInv /\ neg b)
+\end{lstlisting}
+
+\ref{agda-hoare-rule}を使って先程の
+
+
+\begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]
+initCond : Cond
+initCond env = true
+
+stmt1Cond : Cond
+stmt1Cond env = Equal (varn env) 10
+
+stmt2Cond : Cond
+stmt2Cond env = (Equal (varn env) 10) ∧ (Equal (vari env) 0)
+
+whileInv : Cond
+whileInv env = Equal ((varn env) + (vari env)) 10
+
+whileInv' : Cond
+whileInv' env = Equal ((varn env) + (vari env)) 11
+
+termCond : Cond
+termCond env = Equal (vari env) 10
+  
+proof1 : HTProof initCond program termCond
+proof1 =
+      SeqRule {λ e → true} ( PrimRule empty-case )
+    $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
+    $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
+            WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
+            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
+                     $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
+\end{lstlisting}
+
 
 \begin{thebibliography}{99}
 %\bibitem{ohno}
@@ -215,6 +384,11 @@
 外間政尊, 河野真治, GearsOSのAgdaによる記述と検証，
 \\システムソフトウェアとオペレーティング・システム研究会, 2018.
 
+%% \bibtem{Agda-alfa}
+%% \url{http://ocvs.cfv.jp/Agda/}
+
+
+
 \end{thebibliography}
 
 \end{document}