# HG changeset patch # User ryokka # Date 1545091174 -32400 # Node ID 08f8641c705b678ca608ca7ac55432750af945cf # Parent 83d000399c9dbba99d5b0d4475e0b60692c44692 fix diff -r 83d000399c9d -r 08f8641c705b Paper/tecrep.bib --- a/Paper/tecrep.bib Tue Dec 18 04:08:28 2018 +0900 +++ b/Paper/tecrep.bib Tue Dec 18 08:59:34 2018 +0900 @@ -85,6 +85,23 @@ note = {Accessed: 2018/12/17(Mon)} } +@misc{coq, + title = {Welcome! | The Coq Proof Assistant}, + howpublished = {\url{https://coq.inria.fr/}}, + note = {Accessed: 2018/12/17(Mon)} +} + +@misc{ats2, + title = {ATS-PL-SYS}, + howpublished = {\url{http://www.ats-lang.org/}}, + note = {Accessed: 2018/12/17(Mon)} +} + +@misc{rust, + title = {Rust programming language}, + howpublished = {\url{https://www.rust-lang.org/}}, + note = {Accessed: 2018/12/17(Mon)} +} @article{Klein:2010:SFV:1743546.1743574, diff -r 83d000399c9d -r 08f8641c705b Paper/tecrep.pdf Binary file Paper/tecrep.pdf has changed diff -r 83d000399c9d -r 08f8641c705b Paper/tecrep.tex --- a/Paper/tecrep.tex Tue Dec 18 04:08:28 2018 +0900 +++ b/Paper/tecrep.tex Tue Dec 18 08:59:34 2018 +0900 @@ -99,7 +99,7 @@ \maketitle \section{まえがき} OS やアプリケーションの信頼性は重要である。 -信頼性を上げるには仕様を満たしていることを検証する必要がある。 +信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。 プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。 HoareLogic は事前条件が成り立っているときにある 関数を実行して、それが停止する際に事後条件を満た @@ -117,24 +117,27 @@ 事後条件などをもたせることが可能である。 そのため Hoare Logic と CodeGear、DataGear という単位を用いたプログラミング手法 -記述と相性が良く、既存の言語とは異なり HoareLogic を使ったプログラミングができると考えている。 +記述とは相性が良く、既存の言語とは異なり HoareLogic を使ったプログラミングが容易に行えると考えている。 -本研究では Agda 上での HoareLogic の記述を使い、簡単なwhile Loop のプログラムを作成し、証明を行った。 +本研究では Agda 上での HoareLogic の記述を使い、簡単な while Loop のプログラムの作成、証明を行った。 また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと したwhile Loop プログラムを記述、その証明を行なった。 - \section{現状} 現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。 -kernel 検証\cite{Klein:2010:SFV:1743546.1743574},\cite{Nelson:2017:HPV:3132747.3132748}の例では C で記述された Kernel に対して。 -また、別のアプローチとしては ATS や Rust などの低レベル記述向けの関数型言語を実装に用いる手法が存在している。 +kernel 検証\cite{Klein:2010:SFV:1743546.1743574},\cite{Nelson:2017:HPV:3132747.3132748}の例では C で記述された Kernel に対して、検証用の別の言語で書かれた等価な kernel を用いて OS の検証を行っている。 +また、別のアプローチとしては ATS2\cite{ats2} や Rust\cite{rust} などの低レベル記述向けの関数型言語を実装に用いる手法が存在している。 + +証明支援向けのプログラミング言語としては Agda\cite{agda}、 Coq\cite{coq} などが存在しているが、これらの言語自体は実行速度が期待できるものではない。 -証明支援向けのプログラミング言語としては Agda、 Coq などが存在しているが、これらの言語は実行速度が期待できるものではない。 - -この現状から、証明の記述とプログラムの記述が別になっていることがネックになっているのではないかと考えている +そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{cbc} という言語を開発している。 +Continuation based C(CbC) では、処理の単位を CodeGear、 データの単位を DataGear としている。 +CodeGear は値を入力として受け取り出力を行う処理の単位であり、 CodeGear の出力を 次の GodeGear に接続してプログラミングを行う。 CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。 +このメタ計算部分で assertion などの検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。 +現段階では CbC 自体に証明を行うためのシステムが存在しないため、証明支援系言語である Agda を用いて等価な実装の検証を行っている。 \section{Agda} -Adga \cite{agda} とは証明支援系言語である。 +Adga \cite{agda} とは証明支援系の関数型言語である。 Agdaにおける型指定は : を用いて行う。例えば、 変数 x が型 A を持つ、ということを表すには x : A と記述する。 データ型は、代数的なデータ構造で、その定義には data キーワードを用いる。 data キーワードの後に data の名前と、型、 where 句を書きインデントを深 くした後、 @@ -218,8 +221,8 @@ %% -- ?2 : Bool %% \end{lstlisting} -この状態で Compile すると ? 部分に入る型を Agda が示してくれるため、始めに変形する等式を ?0 に -記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。 +この状態で実行すると ? 部分に入る型を Agda が示してくれる。 +始めに変形する等式を ?0 に記述し、?1 の中に $x == y$ のような変形規則を入れることで等式を変形して証明することができる。 ここでは \ref{agda-term-mid} の Bool 値 x を受け取って $x \wedge true$ の時必ず x であるという証明 $\wedge$true と 値と Env を受け取って Bool 値を返す stmt1Cond を使って等式変形を行う。 \lstinputlisting[caption=使っている等式変形規則,label=agda-term-mid]{src/term2.agda.replaced} @@ -254,6 +257,8 @@ Gears OS は処理の単位を Code Gear、データの単位を Data Gear と呼ばれる単位でプログラムを構成する。 信頼性や拡張性はメタ計算として、通常の計算とは区別して記述する。 +Gears OS は Code Gear、Data Gear を用いたプログラミング言語である CbC(Continuation based C) で実装される。 +そのため、Gears OS の実装は Gears を用いたプログラミングスタイルの指標となる。 \section{CodeGearとDataGear} Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear @@ -265,10 +270,6 @@ た後に元のコードに戻らず、次の CodeGear へ継続を行う。 これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。 -Gear では処理やデータ構造が CodeGear、 DataGear に閉じている。したがって、 -DataGear は Agda のデータ構造(data と record)で表現できる。 -CodeGear は Agda の CPS (Continuation Passing Style) で関数として表現することができる。 - \begin{figure}[htpb] \begin{center} \scalebox{0.425}{\includegraphics{pic/meta_cg_dg.pdf}} @@ -277,17 +278,18 @@ \label{fig:cgdg} \end{figure} -また Gears OS 自体もこの Code Gear、Data Gear を用いた CbC(Continuation based C) で実装される。 -そのため、Gears OS の実装は Gears を用いたプログラミングスタイルの指標となる。 +CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。 +このメタ計算部分で assertion などの検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。 -\section{CbC と Agda} +\section{Gears と Agda} %% CbC の CodeGear, DataGear を用いたプログラミングスタイルと Agda での対応 ここでは Gears を用いたプログラムを検証するため、 -Agda 上での CodeGear、 DataGear の対応をみていく。 +Agda 上での CodeGear、 DataGear との対応をみていく。 CodeGear は Agda では継続渡しで書かれた関数と等価である。 継続は不定の型 (\verb+t+) を返す関数で表される。 CodeGear 自体も同じ型 \verb+t+ を返す関数となる。 +このとき、継続に渡される引数や、関数から出力される値が DataGear と等価になる。 Code \ref{agda-cg}は Agda で書いた CodeGear の型の例である。 \lstinputlisting[caption= whileTest の型,label=agda-cg]{src/while-test.agda.replaced} @@ -303,7 +305,7 @@ 例えば、 Code \ref{gears-proof} では $(vari e) ≡ 10 $ が証明したい命題で、whileTest から、whileLoop の CodeGear に継続した後、この命題が正しければよい。 この証明は proof1 の型に対応する$\lambda$項を与えると証明が完了したことになる。 -ここで与えている refl は x==x で、命題が正しいことが証明できている。 +ここで与えている refl は左右の項が等しいというもので、ここでの命題が正しいことが証明できている。 % \begin{verbatim} \begin{lstlisting}[caption=Agda での証明の例,label=gears-proof] @@ -464,18 +466,19 @@ WhileRule はループに用いられ、1つの Command と２つの Condition を受け取り、事前条件が成り立っている間、 Command を繰り返すことを保証している。 -\begin{lstlisting}[caption=Axiom と Tautology,label=axiom-taut] -_⇒_ : Bool → Bool → Bool -false ⇒ _ = true -true ⇒ true = true -true ⇒ false = false +\lstinputlisting[caption=Axiom と Tautology,label=axiom-taut]{src/axiom-taut.agda.replaced} +%% \begin{lstlisting}[caption=Axiom と Tautology,label=axiom-taut] +%% _⇒_ : Bool → Bool → Bool +%% false ⇒ _ = true +%% true ⇒ true = true +%% true ⇒ false = false -Axiom : Cond -> PrimComm -> Cond -> Set -Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true +%% Axiom : Cond -> PrimComm -> Cond -> Set +%% Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true -Tautology : Cond -> Cond -> Set -Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true -\end{lstlisting} +%% Tautology : Cond -> Cond -> Set +%% Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true +%% \end{lstlisting} \begin{lstlisting}[caption=Agda での HoareLogic の構成,label=agda-hoare-rule] data HTProof : Cond -> Comm -> Cond -> Set where @@ -517,8 +520,7 @@ initCondのみ無条件で true を返す Condition になっている。 それぞれの Rule の中にそこで証明する必要のある補題が lemma で埋められている。 -lemma1 から lemma5 の証明は長く、 -論文のページ上限を超えてしまうため 当研究室レポジトリ \cite{cr-ryukyu} のプログラムを参照していただきたい。 +lemma1 から lemma5 の証明は幅を取ってしまうため、 詳細は当研究室レポジトリ \cite{cr-ryukyu} のプログラムを参照していただきたい。 これらの lemma は HTProof の Rule に沿って必要なものを記述されており、 lemma1 では PreCondition と PostCondition が存在するときの代入の保証、 @@ -697,7 +699,7 @@ そのため、Input DataGear を PreCondition、 Command を CodeGear、 Output DataGear を PostCondition と そのまま置き換えることができる。 -こちらも通常の HoareLogic と同様に \ref{agda-while} のwhileプログラムと同様のものを記述する +こちらも通常の HoareLogic と同様に Code \ref{agda-while} のwhileプログラムと同様のものを記述する Code \ref{Gears-hoare-while} は、 CodeGear、 DataGear を用いた Agda 上での while Program の記述であり、証明でもある。 \lstinputlisting[caption=Gears 上での WhileLoop の記述と検証,label=Gears-hoare-while]{src/gears.agda.replaced} @@ -782,7 +784,7 @@ また、 Gears を用いた HoareLogic を記述することができた。 さらに、Gears を用いてHoareLocic 記述で、 -証明を引数として受け渡して記述し、証明とプログラムを一体化することができた。 +証明を引数として受け渡して記述することで、証明とプログラムを一体化することができた。 今後の課題としては GearsOS の検証のために、 RedBlackTree や SynchronizedQueue などのデータ構造の検証をHoareLogic ベースで行うことなどが挙げられる。