Mercurial > hg > Papers > 2020 > soto-midterm
changeset 11:a8bc8c6b48bd default tip
fix
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Tue, 15 Sep 2020 07:06:29 +0900 |
| parents | c162ca9b997e |
| children | |
| files | 175706_mid_thesis.pdf mid_thesis.pdf mid_thesis.tex soto.bib tex/abstract.tex tex/agda.tex tex/future.tex tex/hoare.tex tex/intro.tex tex/rbtree.tex tex/spec.tex |
| diffstat | 11 files changed, 128 insertions(+), 102 deletions(-) [+] |
line wrap: on
line diff
--- a/mid_thesis.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/mid_thesis.tex Tue Sep 15 07:06:29 2020 +0900 @@ -55,15 +55,15 @@ \usepackage{url} \usepackage{amssymb} -%\bibliographystyle{plain} -%\bibliography{soto} -\usepackage[backend=biber, style=numeric]{biblatex} +\usepackage[backend=biber, style=numeric, bibstyle=ieee]{biblatex} \nocite{*} \addbibresource{soto.bib} -%\bibliography{soto} %hoge.bibから拡張子を外した名前 -%\bibliographystyle{junsrt} %参考文献出力スタイル \setlength{\columnsep}{5mm} +\def\lstlistingname{ソースコード} + +\newcommand\figref[1]{図 \ref{#1}} +\newcommand\coderef[1]{ソースコード \ref{#1}} \begin{document} \ltjsetparameter{jacharrange={-3}} @@ -85,39 +85,7 @@ \input{tex/rbtree.tex} % 赤黒木の説明 \input{tex/spec.tex}% 手法 \input{tex/future.tex}% 今後の課題 - -% 参考文献 -% \begin{thebibliography}{9} -% \bibitem{cbc} -% cbc-gcc - 並列信頼研 mercurial repository. \\ -% \url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}. 2020/09/10. -% \bibitem{ryokka} -% Continuation based C での Hoare Logic を用いた仕様記述と検証. Master's thesis,\\ -% 琉球大学 大学院理工学研究科 情報工学専攻, 2020. -% \bibitem{hoare} -% C. A. R. Hoare. An axiomatic basis for computer programming. \\ -% Commun. ACM, Vol. 12, No. 10, p. 576–580, October 1969. -% \bibitem{agda-wiki} -% The agda wiki. \\ -% \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. 2020/09/10. -% \bibitem{agda-doc} -% Welcome to agda’s documentation!. \\ -% \url{http://agda.readthedocs.io/en/latest/}. 2020/09/10. -% \bibitem{agda-book} -% Aaron Stump. Verified Functional Programming in Agda. -% Association for Computing Machinery and Morgan; Claypool, New York, NY, USA, 2016. -% \bibitem{atton} -% 比嘉健太. メタ計算を用いた continuation based c の検証手法. Master's thesis, \\ -% 琉球大学 大学院理工学研究科 情報工学専攻, 2017. -% \bibitem{meta} -% 徳森海斗. Llvm clang 上の continuation based c コンパイラ の改良. Master's thesis, \\ -% 琉球大学 大学院理工学研究科 情報工学専攻, 2016. -% \bibitem{rbtree} -% 渡邉敏正. データ構造と基本アルゴリズム. \\ -% 共立出版株式会社, 2015. -% \end{thebibliography} -% \printbibliography[title=参考文献] - \printbibliography + \printbibliography[title={参考文献}] \end{multicols*} \end{document}
--- a/soto.bib Tue Sep 15 04:49:26 2020 +0900 +++ b/soto.bib Tue Sep 15 07:06:29 2020 +0900 @@ -1,4 +1,73 @@ @misc{cbc-gcc, title = {Hoare Logic - 並列信頼研 mercurial repository}, howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/}}, - note = {Accessed: 2020/2/9(Sun)},} + note = {Accessed: 2020/09/10},} + + +@mastersthesis{ryokka-master, + author = "外間政尊", + title = "Continuation based C での Hoare Logic を用いた仕様記述と検証", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2019" +} + +@article{hoare, + author = {Hoare, C. A. R.}, + title = {An Axiomatic Basis for Computer Programming}, + year = {1969}, + issue_date = {October 1969}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + volume = {12}, + number = {10}, + issn = {0001-0782}, + url = {https://doi.org/10.1145/363235.363259}, + doi = {10.1145/363235.363259}, + journal = {Commun. ACM}, + month = oct, + pages = {576–580}, + numpages = {5}, + keywords = {programming language design, theory of programming’ proofs of programs, machine-independent programming, program documentation, axiomatic method, formal language definition} +} + +@misc{agda-wiki, + title = {The Agda wiki}, + howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}, + note = {Accessed: 2020/09/10}, +} + +@misc{agda-documentation, + title = {Welcome to Agda’s documentation! — Agda latest documentation}, + howpublished = {\url{http://agda.readthedocs.io/en/latest/}}, + note = {Accessed: 2020/09/10}, +} + +@book{Stump:2016:VFP:2841316, + author = {Stump, Aaron}, + title = {Verified Functional Programming in Agda}, + year = {2016}, + isbn = {978-1-97000-127-3}, + publisher = {Association for Computing Machinery and Morgan \&\#38; Claypool}, + address = {New York, NY, USA}, +} + +@mastersthesis{atton-master, + author = "比嘉健太", + title = "メタ計算を用いた Continuation based C の検証手法", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2017" +} + +@mastersthesis{utah-master, + author = "徳森海斗", + title = "LLVM Clang 上の Continuation based C コンパイラ の改良", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2016" +} + +@misc{rbtree, + title={データ構造と基本アルゴリズム}, + author={渡邉}, + year={2000}, + publisher={共立出版} +}
--- a/tex/abstract.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/tex/abstract.tex Tue Sep 15 07:06:29 2020 +0900 @@ -1,14 +1,14 @@ \renewcommand{\abstractname}{\normalsize 要 旨} \begin{abstract} - 当研究室にて Continuation based C \cite{cbc-gcc} (以下CbC) なるC言語の下位言語に当たる言語を開発している。 - 先行研究にて Floyd-Hoare Logic(以下Hoare Logic)を用いてその検証を行なった。 - 本稿では、先行研究にて実施されなかった CbC における赤黒木の検証を Hoare Logic を用いて検証することを目指す。 + 当研究室にて Continuation based C\cite{cbc-gcc} (以下CbC) なるC言語の下位言語に当たる言語を開発している。 + 先行研究\cite{ryokka-master}にて Floyd-Hoare Logic\cite{hoare}(以下Hoare Logic)を用いてその検証を行なった。 + 本稿では、先行研究にて実施されなかった CbC における RedBlackTree の検証を Hoare Logic を用いて検証することを目指す。 \end{abstract} \renewcommand{\abstractname}{\normalsize Abstract} \begin{abstract} - We are developing a language called Continuation based C (CbC), which is a lower language of the C. - In a previous study, Floyd-Hoare Logic (Hoare Logic) was used to validate it. + We are developing a language called Continuation based C\cite{cbc-gcc} (CbC), which is a lower language of the C. + In a previous study\cite{ryokka-master} , Floyd-Hoare Logic\cite{hoare} (Hoare Logic) was used to validate it. In this paper, we aim to use Hoare Logic to validate the red-black tree in CbC, which was not performed in previous studies. \end{abstract}
--- a/tex/agda.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/tex/agda.tex Tue Sep 15 07:06:29 2020 +0900 @@ -6,20 +6,19 @@ は記述したプログラムを証明することができる。 \subsection{プログラムの読み方} -以下は Agda プログラムの一例となる。 -本節ではAgdaの基本事項について解説する。 +本節ではAgdaの基本事項について \coderef{plus} を例として解説する。 -基本事項として、ℕ というのは自然数 (Natulal Number) のことである。 +基本事項として、$ \mathbb{N} $ というのは自然数 (Natulal Number) のことである。 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、 ここでは関数を実行した際の例を記述している。 -したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。 +したがって、これは2つの自然数を受け取って足す関数であることが推測できる。 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda} この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。 この : の前が関数名になり、その後ろがその関数の定義となる。 -: 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。 -→ 以降は関数が返す型を記述している。 +: 以降の (x y : $ \mathbb{N} $) は関数は x, y の自然数2つを受けとるという意味になる。 +$ \rightarrow $ 以降は関数が返す型を記述している。 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、 自然数を返すという定義になる。 @@ -39,13 +38,13 @@ \subsection{Data 型} Deta 型とは分岐のことである。 そのため、それぞれの動作について実装する必要がある。 -例として既出で Data 型である ℕ の実装を見てみる。 +例として既出で Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。 \lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda} -実装から、ℕ という型は zero と suc の2つのコンストラクタを持っていることが分かる。 -それぞれの仕様を見てみると、zeroは ℕ のみであるが、suc は (n : ℕ) → ℕ である。 -つまり、suc 自体の型は ℕ であるが、そこから ℕ に遷移するということである。 +実装から、$ \mathbb{N} $ という型は zero と suc の2つのコンストラクタを持っていることが分かる。 +それぞれの仕様を見てみると、zeroは $ \mathbb{N} $ のみであるが、suc は (n : $ \mathbb{N} $ ) $ \rightarrow \ \mathbb{N} $ である。 +つまり、suc 自体の型は $ \mathbb{N} $ であるが、そこから $ \mathbb{N} $ に遷移するということである。 そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。 したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。 @@ -53,11 +52,9 @@ 言い換えればパターンマッチをする必要があると言える。 これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。 - - \subsection{Record 型} Record 型とはオブジェクトあるいは構造体ののようなものである。 -以下の関数は AND となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 +\coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 \lstinputlisting[label=And, caption=And] {src/agda/And.agda} @@ -65,20 +62,13 @@ これを使用して三段論法を定義することができる。 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。 -コードを以下に示す。 +\coderef{syllogism}を以下に示す。 \lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda} コードの解説をすると、引数として x と a が関数に与えられている。 -引数 x の中身は((A → B) ∧ (B → C))、引数 a の中身は A である。 -したがって、(\_∧\_.p1 x a) で (A → B) に A を与えて B を取得し、 -\_∧\_.p2 x で (B → C) であるため、これに B を与えると C が取得できる。 +引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身は A である。 +したがって、(\_∧\_.p1 x a) で (A $ \rightarrow $ B) に A を与えて B を取得し、 +\_∧\_.p2 x で (B $ \rightarrow $ C) であるため、これに B を与えると C が取得できる。 よって A を与えて C を取得することができたため、三段論法を定義できた。 -%\subsection{Agdaの基本操作} - -%\subsection{定理証明支援器としての Agda} - -%\subsectoin{} - -
--- a/tex/future.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/tex/future.tex Tue Sep 15 07:06:29 2020 +0900 @@ -1,12 +1,16 @@ \section{今後の課題} 今後の課題として、以下が挙げられる。 -赤黒木の基本操作として insert や delete が挙げられる。 -通常は、再代入などを用いて実装を行うと思われるが、agda が変数への代入を許していないため、 -操作後の赤黒木を再構成するように実装を行う必要がある。 +RedBlackTree の基本操作として insert や delete が挙げられる。 +通常は、再代入などを用いて実装を行うと思われるが、Agda が変数への代入を許していないため、 +操作後の RedBlackTree を再構成するように実装を行う必要がある。 その際にどこの状態の検証を行うかが課題になっている。 先行研究にて、 -個々の Code Gear の条件を書いてそれを接続することは agda で実装されている。 +個々の Code Gear の条件を書いてそれを接続することは Agda で実装されている。 しかし、接続された条件が健全であるか証明されていない。 -今後はこの接続された条件の健全性の証明からしていく。 +証明されていない部分というのは、プログラム全体はいくつかの Code Gear の集まりだが、 +Code Gear 実行後の事後条件が正しく次に実行される Code Gear の事前条件として成り立っているか、 +それが最初からプログラムの停止まで正しく行われているかという部分である。 + +今後はこの接続された条件の健全性の証明から行っていく。
--- a/tex/hoare.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/tex/hoare.tex Tue Sep 15 07:06:29 2020 +0900 @@ -1,5 +1,5 @@ \section{Hoare Logic} -Hoare Logic とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。 +Hoare Logic\ref{hoare} とは C.A.R Hoare、 R.W Floyd が考案したプログラムの検証の手法である。 これは、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」 というもので、CbCの実行を継続するという性質に非常に相性が良い。 Hoare Logic を表記すると以下のようになる。 @@ -13,7 +13,7 @@ \subsection{Hoare による Code Gear の検証 } -以下の図が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。 +\figref{hoare}が agda にて Hoare Logic を用いて Code Gear を検証する際の流れになる。 input DataGear が Hoare Logic上の Pre Condition(事前条件)となり、output DataGear が Post Conditionとなる。 各DataGear が Pre / Post Condition を満たしているかの検証は、各 Condition を Meta DataGear で定義し、 条件を満たしているのかをMeta CodeGear で検証する。
--- a/tex/intro.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/tex/intro.tex Tue Sep 15 07:06:29 2020 +0900 @@ -1,19 +1,25 @@ \section{研究目的} OS やアプリケーションの信頼性を高めることは重要な課題である。 -信頼性を高める為には仕様を満たしたプログラムが実装されていることを検証する必要がある。 +信頼性を高める為にはプログラムが仕様を満たした実装をされていることを検証する必要がある。 具体的には「モデル検査」や「定理証明」などが検証手法として挙げられる。 -研究室で CbC という言語を開発している。 +当研究室では CbC という言語を開発している。 CbC とは、C言語からループ制御構造とサブルーチンコールを取り除き、継続を導入した C言語の下位言語である。 この言語の信用性を検証したい。 仕様に合った実装を実施していることの検証手法として Hoare Logic が知られている。 Hoare Logic は事前条件が成り立っているときにある計算(以下コマンド)を実行した後に、 -に事後条件が成り立つことでコマンドの検証を行う。 +事後条件が成り立つことでコマンドの検証を行う。 この定義が CbC の実行を継続するという性質と相性が良い。 CbCでは実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。 -それを繋げていくので、個々の関数の +それを繋げていくため、個々の関数の 正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。 +CbCではループ制御構造を取り除いているため、CbCにてループが含まれるプログラムを作成した際の検証を行う必要がある。 +先行研究ではCbCにおけるWhileLoopの検証を行なっている。 + +Agdaが変数への再代入を許していない為、 +ループが存在し、かつ再代入がプログラムに含まれる RedBlackTree の検証を行いたい。 + % これらのことから、本稿では Hoare Logic を用いて CbC を検証することを目指す。 -これらのことから、本稿では CbC に対応するようにagdaで記述し、Hoare Logic により検証を行うことを目指す。 +これらのことから、CbC に対応するように Agda で RedBlackTree を記述し、Hoare Logic により検証を行うことを目指す。
--- a/tex/rbtree.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/tex/rbtree.tex Tue Sep 15 07:06:29 2020 +0900 @@ -1,7 +1,7 @@ -\section{赤黒木} -赤黒木とは平衡2分探索木の一つである。 +\section{RedBlackTree} +RedBlackTree (または赤黒木)とは平衡2分探索木の一つである。 2分探索木の点にランクという概念を追加し、そのランクの違いを赤と黒の色で分け、以下の定義に基づくように -木を構成した物である。 +木を構成した物である。図では省略しているが、値を持っている点の下に黒色の空の葉があり、それが外点となる \begin{enumerate} \item 各点は赤か黒の色である。 @@ -9,9 +9,9 @@ \item 外点(葉。つまり一番下の点)は黒である。 \item 任意の点から外点までの黒色の点はいずれも同数となる。 \end{enumerate} -参考となるグラフを以下に示す。上記の定義を満たしていることが分かる。 +参考となる\figref{rbtree}を以下に示す。上記の定義を満たしていることが分かる。 \begin{center} \includegraphics[height=3.5cm]{pic/rbtree.pdf} -\caption{CodeGear、DataGear での Hoare Logic} -\label{hoare} +\caption{RedBlackTree の一例} +\label{rbtree} \end{center}
--- a/tex/spec.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/tex/spec.tex Tue Sep 15 07:06:29 2020 +0900 @@ -1,15 +1,13 @@ \section{検証手法} -現在提案している手法は、Hoare Logic は事前条件がある際、コマンド実行後の事後条件が成り立つ場合に -コマンドの部分的な正当性を導けることを前述した。 -その為、agdaでのcbcの検証は下図のようになる。 -流れを説明すると、 +本章では検証する際の手法を説明する。 CodeGear の引数となる DataGear が事前条件となり、 それを検証する為のPre Conditionを検証する為の Meta Gearsが存在する。 その後、さらに事後条件となる DetaGear も Meta Gears にて検証する。 +これらを用いて Hoare Logic によりプログラムの検証を行いたい。 \subsection{CbC記法で書くagda} -CbCプログラムの検証をするに当たり、agdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 -以下が例となるコードである。 +CbCプログラムの検証をするに当たり、AgdaコードもCbC記法で記述を行う。つまり継続渡しを用いて記述する必要がある。 +\coderef{agda-cg}が例となるコードである。 \lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg]{src/cbc-agda.agda} @@ -18,7 +16,7 @@ \subsection{agda による Meta Gears} 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 -今回はその Meta Gears をagdaによる検証の為に用いる。 +今回はその Meta Gears をAgdaによる検証の為に用いる。 \begin{itemize} \item Meta DataGear \mbox{}\\ @@ -31,12 +29,3 @@ す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである \end{itemize} -\subsection{Code Gear の 遷移の検証} -これまで述べた手法にて、CodeGear の検証をすることができる。 -しかし、CodeGear から 次の CodeGear へ正しく事後条件と事前条件が遷移していることを検証する必要がある。 -% また、各 CodeGear が正しく停止することも重要である。 - -遷移の検証のために implies という data 型を導入する。 -\lstinputlisting[label=implies, caption=implies] {src/implies.agda} -これにより CodeGear が正しく遷移できることを検証する。 -