# HG changeset patch # User ryokka # Date 1544951973 -32400 # Node ID 81e2a6af901e24a7db8b1cef957a81ff64049e3b # Parent df1552e4ac7a29bb0d245698b71394fba54982e4 add section diff -r df1552e4ac7a -r 81e2a6af901e Paper/tecrep.pdf Binary file Paper/tecrep.pdf has changed diff -r df1552e4ac7a -r 81e2a6af901e Paper/tecrep.tex --- 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}