# HG changeset patch
# User ryokka
# Date 1545030530 -32400
# Node ID 8189d4b8f2ac18a442832b37267095d960b707d0
# Parent  100e82a436f6d55c1e1da397800af90bf8038103
fix

diff -r 100e82a436f6 -r 8189d4b8f2ac Paper/tecrep.pdf
Binary file Paper/tecrep.pdf has changed
diff -r 100e82a436f6 -r 8189d4b8f2ac Paper/tecrep.tex
--- a/Paper/tecrep.tex	Sun Dec 16 19:33:11 2018 +0900
+++ b/Paper/tecrep.tex	Mon Dec 17 16:08:50 2018 +0900
@@ -10,6 +10,7 @@
 \usepackage{latexsym}
 %\usepackage[fleqn]{amsmath}
 %\usepackage{amssymb}
+\usepackage{url}
 
 \usepackage{listings}
 \lstset{
@@ -136,6 +137,15 @@
 また Gears OS 自体もこの Code Gear、Data Gear を用いた CbC(Continuation based C) で実装される。
 そのため、Gears OS の実装は Code Gear、Data Gear を用いたプログラミングスタイルの指標となる。
 
+\section{Agda}
+
+
+\section{CbC と Agda}
+%% CbC の CodeGear, DataGear を用いたプログラミングスタイルと Agda での対応
+ここでは CodeGear、DataGear を用いたプログラムを検証するため、
+Agda 上での CodeGear、 DataGear の対応をみていく。
+
+
 CodeGear は Agda では継続渡しで書かれた関数と等価である。
 継続は不定の型 (\verb+t+) を返す関数で表される。
 CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
@@ -188,12 +198,28 @@
 %% CbC で記述された任意の CodeGear と Meta CodeGear が Agda にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。
 
 \section{HoareLogic}
-HoareLogic とはC.A.R Hoare、 R.W Floyd らによるプログラムの検証のアイディアである。
-これは、
+%% HoareLogic の説明と Commands、 Rules の説明。公理としてのものなのですべて説明。
+
+HoareLogic とは C.A.R Hoare、 R.W Floyd らによるプログラムの検証のアイディアである。
+これはプログラムの部分的な正当性を検証するアイディアで、
+事前条件(Pre-Condition) P が成り立つとき、コマンド C を実行した後に
+事後条件(Post-Condition) Q が成り立つ。
+これを ${P} C {Q}$ のように表し、コマンドをつなげてプログラム全体を記述することで、
+プログラム内のすべての部分について検証を行うことができる。
+%% これは、プログラムを Skip、 Abort、 Seq、 PComm、 If、 While の6つの規則で記述することで
+
+HoareLogic ではプログラムを  Assign、 Sequential Composition、 If、 While というコマンドで
+記述する。
+
+%% Skip は動作をしないコマンドで事前条件や事後条件に変化を与えない。
+%% About は途中で処理を中断するコマンドで Skip と同様、条件に変化を与えることはない。
+%% Assign は変数に値を代入するコマンドで、事前条件では代入する前の変数が存在することと
+%% 事後条件ではその変数に値が代入されていることになる。
+%% Sequential
 
 
 \section{AgdaでのHoareLogic}
-本章では、Agda 上での HoareLogic についての記述を行う。
+本章では、Agda 上での HoareLogic についての記述と検証を行う。
 今回は、\ref{agda-while} のような while Loop に対しての検証を行うこととする。
 
 \begin{lstlisting}[caption=while Loop,label=agda-while]
@@ -219,7 +245,7 @@
 Skip は何も変更しない Command で、 Abort はプログラムを中断する Command である。
 
 PComm は PrimComm を受けて Command を返す型で定義されていて、 変数を代入するときに使われる。
-Seq は Sequence で Command を2つ受けて Command を返す型で定義されている。これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。
+Seq は Sequence Composition で Command を2つ受けて Command を返す型で定義されている。これは、ある Command から Command に移り、その結果を次の Command に渡す型になっている。
 If は Cond と Comm を2つ受け取り、 Cond の中身によって Comm を変える Command である。
 While は Cond と Comm を受け取り、 Cond の中身が True である間、 Comm を繰り返す Command である。
 
@@ -288,8 +314,6 @@
 \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 での証明の構成である。
@@ -326,8 +350,8 @@
               HTProof bInv (While b cm) (bInv /\ neg b)
 \end{lstlisting}
 
-\ref{agda-hoare-rule}を使って先程の
-
+\ref{agda-hoare-rule}を使って先程の while Program を証明する。
+証明は \ref{agda-hoare-rule}の proof1 の様になる。
 
 \begin{lstlisting}[caption=Agda 上での WhileLoop の検証,label=agda-hoare-while]
 initCond : Cond
@@ -358,6 +382,16 @@
                      $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
 \end{lstlisting}
 
+proof1 は\ref{agda-hoare-prog}の program と似た形をとっている。
+Comannd に対応する証明規則があるため、証明はプログラムに対応する形になる。
+
+\begin{lstlisting}[caption=Gears 上での WhileLoop の検証,label=Gears-hoare-while]
+proofGears : {c10 :  ℕ } → Set
+proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
+
+proofGearsMeta : {c10 :  ℕ } → whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1(λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))
+proofGearsMeta {c10} = {!!}
+\end{lstlisting}
 
 \begin{thebibliography}{99}
 %\bibitem{ohno}
@@ -384,9 +418,11 @@
 外間政尊, 河野真治, GearsOSのAgdaによる記述と検証，
 \\システムソフトウェアとオペレーティング・システム研究会, 2018.
 
-%% \bibtem{Agda-alfa}
+%% \bibtem{agda-alfa}
 %% \url{http://ocvs.cfv.jp/Agda/}
 
+%% \bibtem{agda2-hoare}
+%% \url{https://github.com/IKEGAMIDaisuke/HoareLogic}
 
 
 \end{thebibliography}