# HG changeset patch # User ryokka # Date 1519113965 -32400 # Node ID c8bfe73b2faf5024d9c8f7d194cc1c6a26d23c48 # Parent 28f900230c26e4f4a325ae84e0b25af4c8874a8b fix final_pre diff -r 28f900230c26 -r c8bfe73b2faf final_pre/fig/goto.pdf Binary file final_pre/fig/goto.pdf has changed diff -r 28f900230c26 -r c8bfe73b2faf final_pre/finalPre.aux --- a/final_pre/finalPre.aux Mon Feb 19 23:32:24 2018 +0900 +++ b/final_pre/finalPre.aux Tue Feb 20 17:06:05 2018 +0900 @@ -1,23 +1,31 @@ \relax \@writefile{toc}{\contentsline {section}{\numberline {1}ソフトウェアの信頼性の保証}{1}} \@writefile{toc}{\contentsline {section}{\numberline {2}Countinuation based C (CbC)}{1}} -\newlabel{src:singlelinked}{{1}{1}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}CbCによるStack}{1}} -\@writefile{toc}{\contentsline {section}{\numberline {3}CbC における Interface の実装}{1}} -\newlabel{src:interface}{{2}{1}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}CbCでのStack-Interfaceの実装}{1}} +\newlabel{src:goto}{{1}{1}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}CbCコードの例}{1}} +\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces ソースコード1\relax の流れ}}{1}} +\newlabel{fig:code_simple}{{1}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {3}CbC における Interface の定義}{1}} +\citation{agda} +\newlabel{src:interface}{{2}{2}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}CbCでのStack-Interfaceの実装}{2}} +\@writefile{toc}{\contentsline {section}{\numberline {4}Agda}{2}} +\newlabel{src:agda-css}{{3}{2}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}Agda における CodeSegment の定義}{2}} +\@writefile{toc}{\contentsline {section}{\numberline {5}Agda における Interface の定義、実装}{2}} +\newlabel{src:agda-interface}{{4}{2}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}Agda における Stack -Interface の定義の一部}{2}} +\newlabel{src:agda-single-linked-stack}{{5}{2}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}Agda における Stack -Interface の実装の一部}{2}} +\@writefile{toc}{\contentsline {section}{\numberline {6}Agda による Interface 部分を含めた Stack の部分的な証明}{2}} +\newlabel{src:agda-in-some-state}{{6}{2}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {6}抽象的なStackの定義とpush$->$push$->$pop2 の証明}{2}} \citation{*} \bibstyle{junsrt} \bibdata{reference} -\bibcite{Yasutaka:2016}{1} -\bibcite{Tatsuki:2016}{2} -\bibcite{kaito:2015}{3} -\bibcite{agda}{4} -\@writefile{toc}{\contentsline {section}{\numberline {4}Agda における Interface の実装}{2}} -\newlabel{src:agda-single-linked-stack}{{3}{2}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}Agda における Stack の実装}{2}} -\@writefile{toc}{\contentsline {section}{\numberline {5}Agda による Interface 部分を含めた Stack の部分的な証明}{2}} -\newlabel{src:agda-in-some-state}{{4}{2}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}抽象的なStackの定義とpush$->$push$->$pop2 の証明}{2}} -\@writefile{toc}{\contentsline {section}{\numberline {6}まとめ}{2}} +\bibcite{agda}{1} +\bibcite{Yasutaka:2016}{2} +\bibcite{Tatsuki:2016}{3} +\bibcite{kaito:2015}{4} \bibcite{agda-documentation}{5} +\@writefile{toc}{\contentsline {section}{\numberline {7}まとめ}{3}} diff -r 28f900230c26 -r c8bfe73b2faf final_pre/finalPre.bbl --- a/final_pre/finalPre.bbl Mon Feb 19 23:32:24 2018 +0900 +++ b/final_pre/finalPre.bbl Tue Feb 20 17:06:05 2018 +0900 @@ -1,5 +1,10 @@ \begin{thebibliography}{1} +\bibitem{agda} +The agda wiki. +\newblock \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. +\newblock Accessed: 2017/10/24(Tue). + \bibitem{Yasutaka:2016} {比嘉 健太, 河野 真治}. \newblock {メタ計算を用いた Continuation based C の検証手法}, 2016. @@ -12,11 +17,6 @@ {徳森 海斗, 河野 真治}. \newblock {LLVM Clang 上の Continuation based C コンパイラ の改良}, 2015. -\bibitem{agda} -The agda wiki. -\newblock \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. -\newblock Accessed: 2017/10/24(Tue). - \bibitem{agda-documentation} Welcome to agda’s documentation! ― agda 2.6.0 documentation. \newblock \url{http://agda.readthedocs.io/en/latest/index.html}. diff -r 28f900230c26 -r c8bfe73b2faf final_pre/finalPre.dvi Binary file final_pre/finalPre.dvi has changed diff -r 28f900230c26 -r c8bfe73b2faf final_pre/finalPre.log --- a/final_pre/finalPre.log Mon Feb 19 23:32:24 2018 +0900 +++ b/final_pre/finalPre.log Tue Feb 20 17:06:05 2018 +0900 @@ -1,4 +1,4 @@ -This is e-pTeX, Version 3.14159265-p3.7-160201-2.6 (utf8.euc) (TeX Live 2016) (preloaded format=platex 2017.4.13) 19 FEB 2018 23:31 +This is e-pTeX, Version 3.14159265-p3.7-160201-2.6 (utf8.euc) (TeX Live 2016) (preloaded format=platex 2017.4.13) 20 FEB 2018 17:04 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -221,30 +221,27 @@ LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <9> not available (Font) Font shape `JY1/gt/m/n' tried instead on input line 99. LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <14.4> not available -(Font) Font shape `JT1/gt/m/n' tried instead on input line 104. +(Font) Font shape `JT1/gt/m/n' tried instead on input line 109. LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <14.4> not available -(Font) Font shape `JY1/gt/m/n' tried instead on input line 104. -LaTeX Font Info: Try loading font information for OMS+cmr on input line 132. +(Font) Font shape `JY1/gt/m/n' tried instead on input line 109. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <7> on input line 137. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <5> on input line 137. +LaTeX Font Info: Try loading font information for OMS+cmr on input line 143. (/usr/local/texlive/2016/texmf-dist/tex/latex/base/omscmr.fd File: omscmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions ) LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <10> not available -(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 132. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <7> on input line 132. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <5> on input line 132. -LaTeX Font Info: Try loading font information for OML+cmr on input line 132. - +(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 143. +File: fig/codesegment.pdf Graphic file (type pdf) -(/usr/local/texlive/2016/texmf-dist/tex/latex/base/omlcmr.fd -File: omlcmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions -) -LaTeX Font Info: Font shape `OML/cmr/m/n' in size <10> not available -(Font) Font shape `OML/cmm/m/it' tried instead on input line 132. + + +LaTeX Warning: File `../pic/emblem-bitmap.pdf' not found on input line 164. + File: ../pic/emblem-bitmap.pdf Graphic file (type pdf) - <../pic/emblem-bitmap.pdf> Package Fancyhdr Warning: \headheight is too small (0.0pt): @@ -256,21 +253,29 @@ ] -Underfull \hbox (badness 10000) in paragraph at lines 193--193 -[]\JY1/mc/m/n/10 ソ ースコ ード \OT1/cmr/m/n/10 4: \JY1/mc/m/n/10 抽象的な \OT1 +LaTeX Font Info: Try loading font information for OML+cmr on input line 164. + + (/usr/local/texlive/2016/texmf-dist/tex/latex/base/omlcmr.fd +File: omlcmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions +) +LaTeX Font Info: Font shape `OML/cmr/m/n' in size <10> not available +(Font) Font shape `OML/cmm/m/it' tried instead on input line 164. + +Underfull \hbox (badness 10000) in paragraph at lines 224--224 +[]\JY1/mc/m/n/10 ソ ースコ ード \OT1/cmr/m/n/10 6: \JY1/mc/m/n/10 抽象的な \OT1 /cmr/m/n/10 Stack \JY1/mc/m/n/10 の定義と [] -(./finalPre.bbl [2]) [3 +[2] (./finalPre.bbl) [3 ] (./finalPre.aux) ) Here is how much of TeX's memory you used: - 2652 strings out of 493693 - 35610 string characters out of 6149787 - 395064 words of memory out of 5000000 - 6194 multiletter control sequences out of 15000+600000 + 2664 strings out of 493693 + 35780 string characters out of 6149787 + 358088 words of memory out of 5000000 + 6201 multiletter control sequences out of 15000+600000 14789 words of font info for 58 fonts, out of 8000000 for 9000 929 hyphenation exceptions out of 8191 - 36i,15n,45p,299b,1738s stack positions out of 5000i,500n,10000p,200000b,80000s + 27i,15n,43p,299b,1499s stack positions out of 5000i,500n,10000p,200000b,80000s -Output written on finalPre.dvi (3 pages, 22724 bytes). +Output written on finalPre.dvi (3 pages, 25448 bytes). diff -r 28f900230c26 -r c8bfe73b2faf final_pre/finalPre.pdf Binary file final_pre/finalPre.pdf has changed diff -r 28f900230c26 -r c8bfe73b2faf final_pre/finalPre.tex --- a/final_pre/finalPre.tex Mon Feb 19 23:32:24 2018 +0900 +++ b/final_pre/finalPre.tex Tue Feb 20 17:06:05 2018 +0900 @@ -99,7 +99,12 @@ \end{onecolabstract}] \thispagestyle{fancy} - +% ソフトウェアの信頼性の保証 +% 　　CbC の話(CG,DGの話も) +% 　　メタ計算を分けてる +% context (Meta DataGear) +% そのために interface +% Agda でも interfece を実装して検証した \section{ソフトウェアの信頼性の保証} ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証す @@ -110,36 +115,51 @@ Countinuation based C (以下 CbC) を開発している。 % 本研究では、検証や証明に直接使用できる言語として CbC を用いる。 -CbC では自由に DataGear を扱う際に直接 CodeGear からアクセスできてしまうと信頼性を損ねる。 -その為に stub CodeGear と呼ばれるデータを扱うための Meta CodeGear を定 -義している。基本的な stub CodeGear は CodeGear から自動で生成することができるよ -うになっている。 -しかし、 CbC で実装していくにつれて stub CodeGear の記述が複雑になることが分かっ -た。　その為、既存の実装をモジュールとして扱うために Interface という仕組みを導 -入した。 +CbC では通常の計算とメタ計算を分けて記述している。 +しかし、CodeGear で DataGear を扱う際、 Context と呼ばれる CodeGear、 DataGear の +リスト等を持っている Meta DataGear を経由する。 +通常の CodeGear から Context を直接扱えるようにするのは信頼性を損なう。そのため、 CbC +では Context を通して、次の CodeGear に接続する MetaCodeGear である stub +CodeGear を定義している。 -本研究では CbC 、 Agda の両方で Interface を実装し、 Interface を含めた Stack と Tree の性質を -部分的に証明した。 +CbC で実装していくにつれて特殊な stub CodeGear の記述が複雑になった。 +そこで既存の実装をモジュールとして扱うために Interface という仕組みを導入した。 +Interface では、DataGear に対しての操作(API)を CodeGear とその CodeGear で扱われ +ている DataGearの集合を抽象的に表現した Meta DataGear として定義されている。 + +本研究では CbCで使われている Interface を 、 Agda 上で定義、実装を行い、 +Interface を含めた Stack と Tree の部分的な証明を行なった。 \section{Countinuation based C (CbC)} Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。 -CbC は C 言語とほぼおなじ構文を持つが、 C の関数の代わりに CodeGear を用いて処理を記述する。 +CbC は C 言語とほぼおなじ構文を持つが、 C の関数の代わりに CodeGear を用いて処理 +を記述する。 +CodeGear は関数定義の先頭に $\_\_code$ をつけて定義する。 CodeGear は処理の単位でそれらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。 DataGear は CodeGear が扱うデータの単位であり、処理に必要なデータが全て入っている。次の CodeGear に処理を移す際は、 goto の後に CodeGear 名と DataGear を指定する。 CbC ではこの継続処理がメタ計算として定義されており、 CodeGear に変更なく検証等を行うことができる。 -例として CbC による Stack に対する操作のコード示す。 - -\lstinputlisting[label=src:singlelinked, caption=CbCによるStack]{./src/SingleLinkedStack.cbc.replace} +例として CbC の簡単な例(ソースコード\ref{src:goto})と、流れ\ref{fig:code_simple}を示す。 -push では新しい element を作成し next に現在の top を入れ、Stack の top を書き換えて次のCodeGearに飛ぶ。 -pop では top に data があればそれを next に入れ、 Stack を更新して次のCodeGearに飛ぶ。 top に data が無ければ NULL を next に入れて次のCodeGearに飛ぶ。 +\lstinputlisting[label=src:goto, caption=CbCコードの例]{./src/goto.cbc} +\begin{figure}[htpb] + \begin{center} + \scalebox{0.7}[0.7]{\includegraphics{fig/codesegment.pdf}} + \end{center} + \caption{ソースコード\ref{src:goto}の流れ} + \label{fig:code_simple} +\end{figure} -\section{CbC における Interface の実装} -CbC で実装していくにつれ、stub CodeGear の記述が複雑になった。 +ソースコード\ref{src:goto}では　cs0、 cs1 が CodeGear で a+b が cs0 の Output DataGear であり、 +cs1 の Input DataGear になる。 +流れ\ref{fig:code_simple}は cs0 から cs1 へ継続した後、 cs0 には戻らずに次の継 +続に指定された CodeGear へ継続する。 + +\section{CbC における Interface の定義} +CbC で実装していくにつれ、stub CodeGear の記述が煩雑になった。 そのため 既存の実装を モジュールとして扱うため Interface を導入した。 Interface は DataGear に対して何らかの操作(API)を行う CodeGear とその CodeGear で使われる DataGear の集合を抽象化した メタレベルの DataGear -として定義した。例として Stack での Interface の実装をみる。 +として定義した。例として Stack での Interface の実装(ソースコード\ref{src:interface})を示す。 \lstinputlisting[label=src:interface, caption=CbCでのStack-Interfaceの実装] {src/singleLinkedStackInterface.cbc} @@ -150,35 +170,46 @@ このように Interface 記述をすることで CbC で通常記述する必要がある一定の部分を省略し呼び出 しが容易になる。 -% \section{Agda} -% Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。 -% 依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。 -% CbC を Agda に変換する場合 DataGear をレコード型、 CodeGear は Agda での通常関数となる。 -% 前項で示した CbC で書かれた Stack の操作を Agda に変換したコードを\ref{src:stack-agda}に示す。 +\section{Agda} +Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。 +依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。 +CbC を Agda に変換する場合 DataGear はレコード型、 CodeGear は Agda での通常関数 +として定義できる。 +前項で示した CbC の簡単な例を Agda に変換する。(ソースコード\ref{src:agda-css}) -% \lstinputlisting[label=src:stack-agda, caption=Agda による Stack の実装]{src/stack.agda.replace} +\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] +{src/CodeSegments.agda} -% Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。関数の型では → または \verb/->/ を使い定義する。 -% Agda のレコード型も存在する。定義をする際は record キーワードのあとにレコード名、 +Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。 +関数の型では → または \verb/->/ を使い定義し、関数本体は関数名の後に$=$をつけて +記述する。 +DataGear はレコード型で表記できるため Agda 上で DataGear を定義することが可能で +ある。 + % 定義をする際は record キーワードのあとにレコード名、 % 型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコー % ドを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙 -% していく。複数の値を列挙する際は ; で区切る。DataGear はレコード型で表記できた -% ため、 Agda での DataGear の変換はレコード型を使う。 -% このように CbC のコードを Agda に変換し、証明を行う。 +% していく。複数の値を列挙する際は ; で区切る。 +% Agda での DataGear の定義の例を以下のソースコード\ref{src:agda-ds}示す +% \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda} +このように CbC のコードを Agda に変換し、証明を行う。 -\section{Agda における Interface の実装} -Agda でも CbC と同様に Interface の実装した。 -例として Agda で実装した Stack 上の interface をみる。 -Stack の実装は SingleLinkedStack(ソースコード\ref{src:agda-single-linked-stack}) +\section{Agda における Interface の定義、実装} +Agda でも CbC と同様に Interface の定義、実装した。 +例として Agda で実装した Stack-interface の一部をみる。 +Stack の定義はソースコード\ref{src:agda-interface}、実装は ソースコード +\ref{src:agda-single-linked-stack} として書かれている。それを Stack 側から interface を通して呼び出している。 +\lstinputlisting[label=src:agda-interface, caption=Agda における Stack +-Interface の定義の一部] {src/AgdaInterface.agda} + \lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack -の実装] {src/AgdaSingleLinkedStack.agda} +-Interface の実装の一部] {src/AgdaSingleLinkedStack.agda} \section{Agda による Interface 部分を含めた Stack の部分的な証明} -Agda で Interface を定義する事ができた。この Interface を通した Stack で push +今回は Interface を通した Stack で push 、 pop などの操作が正しく行われるかの証明を行った。 -ここでの証明とは Stack の処理が特定の性質を持つことを保証することである。 +ここでの証明とは Stack が特定の性質を持つことを保証することである。 Stack の処理として様々な性質が存在するが、ここでは 「どのような状態の Stack でも、値を push した後 pop した値は直前 @@ -205,8 +236,9 @@ Interface を用いたプログラムを実装、検証した。 また、 CbC で記述した時には細かく分かっていなかった Interface の型が明確に なった。 -今後の課題としては、CodeGear、DataGear をベースにした Hoare Logic を Agda で実装する。 -また、その Hoare Logic を使い、いくつかの証明を実際に記述する。 +今後の課題としては、Tree 側では証明が複雑化し、うまく証明できていないことと、 + Hoare Logic 用いての証明を行えるように、CodeGear、DataGear をベースにした Hoare + Logic を Agda 上で定義し、実際に証明を行うことなどが挙げられる。 \nocite{*} \bibliographystyle{junsrt} diff -r 28f900230c26 -r c8bfe73b2faf final_pre/src/AgdaInterface.agda --- a/final_pre/src/AgdaInterface.agda Mon Feb 19 23:32:24 2018 +0900 +++ b/final_pre/src/AgdaInterface.agda Tue Feb 20 17:06:05 2018 +0900 @@ -4,7 +4,3 @@ stackMethods : StackMethods {n} {m} a {t} si pushStack : a -> (Stack a si -> t) -> t pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) - popStack : (Stack a si -> Maybe a -> t) -> t - popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - --- 以下省略 diff -r 28f900230c26 -r c8bfe73b2faf final_pre/src/AgdaSingleLinkedStack.agda --- a/final_pre/src/AgdaSingleLinkedStack.agda Mon Feb 19 23:32:24 2018 +0900 +++ b/final_pre/src/AgdaSingleLinkedStack.agda Tue Feb 20 17:06:05 2018 +0900 @@ -1,15 +1,5 @@ --- Implementation pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t pushSingleLinkedStack stack datum next = next stack1 where element = cons datum (top stack) stack1 = record {top = Just element} - - -popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t -popSingleLinkedStack stack cs with (top stack) -... | Nothing = cs stack Nothing -... | Just d = cs stack1 (Just data1) - where - data1 = datum d - stack1 = record { top = (next d) } diff -r 28f900230c26 -r c8bfe73b2faf final_pre/src/csds.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_pre/src/csds.agda Tue Feb 20 17:06:05 2018 +0900 @@ -0,0 +1,20 @@ +record ds0 : Set where +field +a : Int +b : Int + +record ds1 : Set where +field +c : Int + +cs2 : CodeSegment ds1 ds1 +cs2 = cs id + +cs1 : CodeSegment ds1 ds1 +cs1 = cs (\d -> goto cs2 d) + +cs0 : CodeSegment ds0 ds1 +cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) + +main : ds1 +main = goto cs0 (record {a = 100 ; b = 50})