Mercurial > hg > Papers > 2020 > ryokka-master
changeset 0:41a936510fd0
Initialize
| author | ryokka |
|---|---|
| date | Thu, 02 Jan 2020 21:25:52 +0900 |
| parents | |
| children | ee44dbda6bd3 |
| files | paper/Makefile paper/abstract.tex paper/agda.tex paper/cbc.tex paper/cbc_agda.tex paper/conclusion.tex paper/history.bib paper/history.tex paper/hoare.tex paper/introduction.tex paper/master_paper.pdf paper/master_paper.tex paper/reference.bib paper/summary.tex paper/thanks.tex paper/tree.tex ryokka-master.mm |
| diffstat | 17 files changed, 661 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/Makefile Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,44 @@ +# Settings +TARGET=master_paper +BIBTEX=pbibtex +BB=extractbb + +vpath pdf fig +FIGURES=$(wildcard fig/*.pdf) +FIGURES_FOR_TEX=$(subst .pdf,.xbb,$(FIGURES)) + +vpath agda src +SOURCES=$(wildcard src/*agda) +SOURCES_FOR_TEX=$(subst .agda,.agda.replaced,$(SOURCES)) + +# dependencies +$(TARGET).pdf : $(TARGET).dvi + dvipdfmx $< + +$(TARGET).dvi : $(wildcard *.tex) $(FIGURES_FOR_TEX) $(SOURCES_FOR_TEX) + platex $(TARGET).tex + $(BIBTEX) $(TARGET) + platex $(TARGET).tex + platex $(TARGET).tex + +%.xbb: %.pdf + $(BB) $< + +%.agda.replaced: %.agda + ruby escape_agda.rb $< + + +# commands +.PHONY : clean all open remake + +clean: + rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*.replaced + +all: $(TARGET).pdf + +open: $(TARGET).pdf + open $(TARGET).pdf + +remake: + make clean + make all
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/abstract.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,26 @@ +\chapter*{要旨} +OS やアプリケーションの信頼性は重要である。 +信頼性を上げるにはプログラムが仕様を満たしていることを検証する必要がある。 +プログラムの検証手法として、Floyd–Hoare logic (以下 Hoare Logic)が存在している。 +HoareLogic は事前条件が成り立っているときにある +関数を実行して、それが停止する際に事後条件を満た +すことを確認することで、検証を行う。 +HoareLogic はシンプルなアプローチであるが通常のプログラミング言語で使用することができず、 +広まっているとはいえない。 + +当研究室では信頼性の高い OS として GearsOS を開発している。 +現在 GearsOS ではCodeGear、DataGearという単位を用いてプログラムを記述する手法を用いており、 +仕様の確認には定理証明系である Agda を用いている。 + +CodeGearは Agda 上では継続渡しの記述を用いた関数として +記述する。 +また、継続にある関数を実行するための事前条件や +事後条件などをもたせることが可能である。 + +そのため Hoare Logic と CodeGear、DataGear という単位を用いたプログラミング手法 +記述とは相性が良く、既存の言語とは異なり HoareLogic を使ったプログラミングが容易に行えると考えている。 + +本研究では Agda 上での HoareLogic の記述を使い、簡単な while Loop のプログラムの作成、証明を行った。 +また、GearsOS の仕様確認のために CodeGear、DataGear という単位を用いた記述で Hoare Logic をベースと +したwhile Loop プログラムを記述、その証明を行なった。 +\chapter*{Abstract}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/agda.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,14 @@ +\chapter{Agda} +Agda についての説明 + +\section{Agda の Data Type} +data とか record とか + +\section{Agda の関数} +関数定義だったり型とかの話 + +\section{Agda での検証} +検証の話 + +\section{定理証明とプログラミング検証} +たぶん Curry-Howard isomorphism の話
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/cbc.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,13 @@ +% だいたい sigss のやつ + +\chapter{Continuation based C} +CbC について + +\section{Code GearとData Gear} +概念 + +\section{メタ計算} +メタ計算の話 + +\section{Meta Gear} +Meta Gears の概念
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/cbc_agda.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,14 @@ +\chapter{Continuation based C と Agda} +対応のお話 + +\section{DataGear の対応} +agda での datagear + +\section{CodeGear} +agda での codegear + +\section{Meta部分の話} +あんまりでなさそうだけどとりあえず + +\section{CbC 上での HoareLogic の実現} +研究の主な部分
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/conclusion.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,5 @@ +\chapter{結論} +まだ終わってないので最後に + +\section{今後の課題} +いつかくる後輩の修論や卒論に備えて
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/history.bib Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,8 @@ +@techreport{weko_189373_1, + author = "外間,政尊 and 河野,真治", + title = "GearsOSのAgdaによる記述と検証", + year = "2018", + institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科", + number = "5", + month = "may" +} \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/history.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,15 @@ +\newpage +\vspace*{\stretch{1}} +{\Huge \textbf{研究関連業績}}% +\\ +\\ +\begin{enumerate} + \item 外間政尊, 河野真治. GearsOSのAgdaによる記述と検証. 研究報告システムソフトウェアとオペレーティング・システム（OS), May, 2018 + \item 外間政尊, 河野真治. GearsOSのHoare Logicをベースにした検証手法. 電子情報通信学会 ソフトウェアサイエンス研究会 (SIGSS) 1月, Jan, 2019 + + %% \item 宮城光希, 河野真治. Code Gear と Data Gear を持つ Gears OS の設計. 第59回プログラミング・シンポジウム, Jan, 2018 +\end{enumerate} + + + +\vspace*{\stretch{2}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/hoare.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,17 @@ +\chapter{Floyd-Hoare Logic} +HoareLogic の話 + +\section{Hoare Triple} +HoareLogic の概念 + +\section{Agda での Hoare Logic} +人のコード解説になりそう + + +\section{Hoare Logic の Soundness} +Soundness 周り + +\section{Hoare Logic での証明} +whileTestPrim.agda の解説 + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/introduction.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,24 @@ +% sigos のやつ +\chapter{プログラミング言語の検証} +現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。 +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} などが存在しているが、これらの言語自体は実行速度が期待できるものではない。 + +そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{cbc} という言語を開発している。 +Continuation based C(CbC) では、処理の単位を CodeGear、 データの単位を DataGear としている。 +CodeGear は値を入力として受け取り出力を行う処理の単位であり、 CodeGear の出力を 次の GodeGear に接続してプログラミングを行う。 CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。 +このメタ計算部分で assertion などの検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。 +現段階では CbC 自体に証明を行うためのシステムが存在しないため、証明支援系言語である Agda を用いて等価な実装の検証を行っている。 + + +%現代の OS では拡張性と信頼性を両立させることが要求されている。 +%時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。 +%しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。 +%これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。 +% 証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。 +% 型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610} +% 従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。 +% また SPIN などのモデル検査を OS の検証に用いた例もである。 +% 本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/master_paper.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,116 @@ +% Todo +\documentclass[a4j,12pt]{jreport} +\usepackage{master_paper} +\usepackage{ascmac} +\usepackage[dvipdfmx]{graphicx} +\usepackage{here} +\usepackage{listings} +\usepackage{comment} +\usepackage{url} +\usepackage[deluxe, multi]{otf} + +%\input{dummy.tex} %% font + +\jtitle{GearsOS での HoareLogic を用いた実装と検証} +\etitle{} % 英文例題まだ +\year{2020年 3月} +\eyear{March 2020} +\author{外間 政尊} +\eauthor{Masataka HOKAMA} +\chife{指導教員：教授 玉城 史朗} % 多分このままでもあってる後で確認 +\echife{Supervisor: Prof. Shirou TAMAKI} + +\marklefthead{% 左上に挿入 + \begin{minipage}[b]{.4\textwidth} + 琉球大学大学院学位論文(修士) +\end{minipage}} + +%\markleftfoot{% 左下に挿入 +% \begin{minipage}{.8\textwidth} +% Gears OS の並列処理 +%\end{minipage}} + +\newcommand\figref[1]{図 \ref{fig:#1}} +\newcommand\tabref[1]{表 \ref{tab:#1}} +\newcommand\coderef[1]{ソースコード \ref{code:#1}} + +\lstset{ + frame=single, + keepspaces=true, + stringstyle={\ttfamily}, + commentstyle={\ttfamily}, + identifierstyle={\ttfamily}, + keywordstyle={\ttfamily}, + basicstyle={\ttfamily}, + breaklines=true, + xleftmargin=0zw, + xrightmargin=0zw, + framerule=.2pt, + columns=[l]{fullflexible}, + numbers=left, + stepnumber=1, + numberstyle={\scriptsize}, + numbersep=1em, + language={}, + tabsize=4, + lineskip=-0.5zw, + escapechar={@}, +} +\def\lstlistingname{ソースコード} +\def\lstlistlistingname{ソースコード目次} + +%%% 索引のために以下の2行を追加 +\usepackage{makeidx,multicol} +\makeindex +\begin{document} +%rome +\maketitle + +\pagenumbering{roman} +\setcounter{page}{0} +\makecommission + +\newpage + +%要旨 +\input{abstract.tex} + +%発表履歴 +\addcontentsline{toc}{chapter}{研究関連論文業績} +\input{history.tex} + +\mainmatter +%目次 +\tableofcontents + +%図目次 +\listoffigures + +%表目次 +\listoftables + +%リスト目次 +\lstlistoflistings + +%chapters +\input{introduction.tex} +\input{cbc.tex} +\input{agda.tex} +\input{hoare.tex} +\input{cbc_agda.tex} +\input{tree.tex} +\input{conclusion.tex} + +%謝辞 +\addcontentsline{toc}{chapter}{謝辞} +\input{thanks.tex} + +%参考文献 +\nocite{*} +\bibliographystyle{junsrt} +\bibliography{reference} + +%付録 +\addcontentsline{toc}{chapter}{付録} +\appendix +\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/reference.bib Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,233 @@ +@inproceedings{queue, + author = {Michael, Maged M. and Scott, Michael L.}, title = {Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algorithms}, + booktitle = {Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing}, + series = {PODC '96}, + year = {1996}, + isbn = {0-89791-800-2}, + location = {Philadelphia, Pennsylvania, USA}, + pages = {267--275}, + numpages = {9}, + url = {http://doi.acm.org/10.1145/248052.248106}, + doi = {10.1145/248052.248106}, + acmid = {248106}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {compare_and_swap, concurrent queue, lock-free, multiprogramming, non-blocking}, +} + +@inproceedings{agda, + author = {Norell, Ulf}, + title = {Dependently Typed Programming in Agda}, + booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation}, + series = {TLDI '09}, + year = {2009}, + isbn = {978-1-60558-420-1}, + location = {Savannah, GA, USA}, + pages = {1--2}, + numpages = {2}, + url = {http://doi.acm.org/10.1145/1481861.1481862}, + doi = {10.1145/1481861.1481862}, + acmid = {1481862}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {dependent types, programming}, +} + +@inproceedings{Chen:2015:UCH:2815400.2815402, + author = {Chen, Haogang and Ziegler, Daniel and Chajed, Tej and Chlipala, Adam and Kaashoek, M. Frans and Zeldovich, Nickolai}, + title = {Using Crash Hoare Logic for Certifying the FSCQ File System}, + booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles}, + series = {SOSP '15}, + year = {2015}, + isbn = {978-1-4503-3834-9}, + location = {Monterey, California}, + pages = {18--37}, + numpages = {20}, + url = {http://doi.acm.org/10.1145/2815400.2815402}, + doi = {10.1145/2815400.2815402}, + acmid = {2815402}, + publisher = {ACM}, + address = {New York, NY, USA}, +} + +@inproceedings{Klein:2009:SFV:1629575.1629596, + author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon}, + title = {seL4: Formal Verification of an OS Kernel}, + booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles}, + series = {SOSP '09}, + year = {2009}, + isbn = {978-1-60558-752-3}, + location = {Big Sky, Montana, USA}, + pages = {207--220}, + numpages = {14}, + url = {http://doi.acm.org/10.1145/1629575.1629596}, + doi = {10.1145/1629575.1629596}, + acmid = {1629596}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {isabelle/hol, l4, microkernel, sel4}, +} + + +@inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879, + author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi}, + title = {Push-button Verification of File Systems via Crash Refinement}, + booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation}, + series = {OSDI'16}, + year = {2016}, + isbn = {978-1-931971-33-1}, + location = {Savannah, GA, USA}, + pages = {1--16}, + numpages = {16}, + url = {http://dl.acm.org/citation.cfm?id=3026877.3026879}, + acmid = {3026879}, + publisher = {USENIX Association}, + address = {Berkeley, CA, USA}, +} + +@inproceedings{Yang:2010:SLI:1806596.1806610, + author = {Yang, Jean and Hawblitzel, Chris}, + title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System}, + booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation}, + series = {PLDI '10}, + year = {2010}, + isbn = {978-1-4503-0019-3}, + location = {Toronto, Ontario, Canada}, + pages = {99--110}, + numpages = {12}, + url = {http://doi.acm.org/10.1145/1806596.1806610}, + doi = {10.1145/1806596.1806610}, + acmid = {1806610}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {operating system, run-time system, type safety, verification}, +} + +@article{atton-ipsj, +author="比嘉 健太 and 河野 真治", +title="Verification Method of Programs Using Continuation based C", +journal="情報処理学会論文誌プログラミング（PRO）", +ISSN="1882-7802", +publisher="", +year="2017", +month="feb", +volume="10", +number="2", +pages="5-5", +URL="https://ci.nii.ac.jp/naid/170000148438/en/", +DOI="", +} + +@article{go, +author={J. Meyerson}, +journal={IEEE Software}, +title={The Go Programming Language}, +year={2014}, +volume={31}, +number={5}, +pages={104-104}, +keywords={Andrew Gerrand;C;Go;Google;arrays;build times;compilers;garbage collection;golang;imports;interfaces;open source;readability;scalability;slices;standard library;syntax}, +doi={10.1109/MS.2014.127}, +ISSN={0740-7459}, +month={Sept},} + +@article{moggi-monad, + author = {Moggi, Eugenio}, + title = {Notions of Computation and Monads}, + journal = {Inf. Comput.}, + issue_date = {July 1991}, + volume = {93}, + number = {1}, + month = jul, + year = {1991}, + issn = {0890-5401}, + pages = {55--92}, + numpages = {38}, + url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4}, + doi = {10.1016/0890-5401(91)90052-4}, + acmid = {116984}, + publisher = {Academic Press, Inc.}, + address = {Duluth, MN, USA}, +} + +@inproceedings{nobu-prosym, + author = "大城信康 and 河野真治", + title = "Continuation based C の GCC4.6 上の実装について", + booktitle = "第53回プログラミング・シンポジウム予稿集", + year = "2012", + volume = "2012", + pages = "69--78", + month = "jan" +} + +@inproceedings{mitsuki-prosym, + author = "宮城光希 and 河野真治", + title = "Code Gear と Data Gear を持つ Gears OS の設計", + booktitle = "第59回プログラミング・シンポジウム予稿集", + year = "2018", + volume = "2018", + pages = "197--206", + month = "jan" +} + + +@InProceedings{llvm, +author = {Chris Lattner and Vikram Adve}, +title = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}", +booktitle = "{Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04)}", +address = {Palo Alto, California}, +month = {Mar}, +year = {2004} +} + +@article{kaito-lola, + author = "Kaito, Tokumori and Shinji, Kono", + title = "Implementing Continuation based language in LLVM and Clang", + journal = "LOLA 2015, Kyoto", + month = "July", + year = 2015 + +} + +@article{kkb-sigos, + author = "小久保翔平 and 伊波立樹 and 河野真治", + title = "Monad に基づくメタ計算を基本とする Gears OS の設計", + journal = "第133回情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)", + month = "May", + year = 2015 +} + +@article{ikkun-sigos, + author = "東恩納琢偉 and 伊波立樹 and 河野真治", + title = "Gears OS における並列処理", + journal = "第140回 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)", + month = "May", + year = 2017 +} + +@misc{openmp, + title = "OpenMP: Simple, portable, scalable SMP programming", + howpublished = {\url{http://www.openmp.org,}}, + note = {Accessed: 2018/02/05(Mon)} +} + +@misc{cuda, + title = {CUDA Zone | NVIDIA Developer}, + howpublished = {\url{https://developer.nvidia.com/cuda-zone}}, + note = {Accessed: 2018/02/05(Mon)} +} + +@mastersthesis{utah-master, + author = "徳森海斗", + title = "LLVM Clang 上の Continuation based C コンパイラ の改良", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2016" +} + +@mastersthesis{kkb-master, + author = "小久保 翔平", + title = "Code Segment と Data Segment を持つ Gears OS の 設計", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2016" +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/summary.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,34 @@ +\chapter{まとめ} +本論文ではメタ計算を用いた Continuation based C プログラムの検証手法を二つ提案した。 + +一つはモデル検査的なアプローチであり、メタ計算ライブラリ akasha を用いて GearsOS の非破壊赤黒木の仕様を保証した。 +CbC における仕様の定義は assert に渡す論理式として定義され、状態の数え上げは軽量継続 \verb/meta/ を切り替えることで実現できた。 +CbC で記述された非破壊赤黒木のプログラムを検証用に変更することなく、CbC 自身で検証した。 +検証できた範囲は有限の要素数のみであるが、有限モデルチェッカ CBMC よりも大きな範囲を検証した。 + +二つめは定理証明的なアプローチである。 +akasha を用いた検証では挿入回数は有限の数に限定されていた。 +プログラムを直接証明することにより、任意の回数の操作においても性質を保証する。 +部分型を利用して CbC の型システムの定義を行ない、依存型を持つ言語 Agda 上で記述することで CbC の形式的な定義とした。 +Agda 上で記述された CbC プログラムの性質を証明することで、 CbC が部分型できちんと型付けできること、依存型をCbCコンパイラに組み込むことでCbC 自身を証明できることが分かった。 + +また、型システムは証明以外にも実用的に利用できることが分かった。 +akasha を用いて検証を行なう際、全ての CodeSegment に対して stub をユーザが定義する必要があった。 +CbC の型を定義することにより、stub の自動生成と型チェックが行なえることが分かった。 + +\section{今後の課題} +今後の課題として、型システムの詳細な性質の解析がある。 +本論文では部分型の定義を CbC に適用した。 +CodeSegment は関数呼び出しを末尾でしか許さない制限があるので、関数型の計算規則をより制限できるはずである。 +その制約の元に生まれた計算体系の持つ性質や表現能力に興味がある。 + +また、提案した型システムを CbC コンパイラの内部に組み込み、CodeSegment と DataSegment の型チェックを行なえるようにしたい。 +加えて部分型を組み込むことにより、stub の自動生成ができる。 +さらに依存型を加えれば CbC で CbC 自身を証明できるようになる。 +他にも SingleLinkedStack の証明を元にした赤黒木の証明などが考えられる。 + +モデル検査的アプローチの展望としては、依存型を CbC コンパイラに実装し、型情報を用いた記号実行や状態の列挙を行なうシステムの構築などがある。 + +また、型システムの拡張としては総称型などを CbC に適用することも挙げられる。 +多相型は \verb/Java/ におけるジェネリクスや \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。 +他にも、CbC の型推論や推論器の実装などが挙げられる。
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/thanks.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,9 @@ +\chapter*{謝辞} + +本研究の遂行、本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に心より感謝致します。 +そして、 共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します。 +最後に、 有意義な時間を共に過ごした理工学研究科情報工学専攻の学友、並びに物心両面で支えてくれた家族に深く感謝致します。 + +\begin{flushright} + 2018年 3月 \\ 伊波立樹 +\end{flushright}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/tree.tex Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,14 @@ +\chapter{BinaryTree} +CbC-Agda 上での Binary Tree + +\section{BinaryTree} +BinaryTree 概要 + +\section{BinaryTree の実現} +BinaryTree の記述等 + +\section{BinaryTree の検証時の問題点と改善} +つまってたとこ(条件付きとかそのあたり) + +\section{BinaryTree 検証の HoareLogic を用いた解決} +できたらいいなの話(1/2 時点)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ryokka-master.mm Thu Jan 02 21:25:52 2020 +0900 @@ -0,0 +1,75 @@ +<map version="1.1.0"> +<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> +<node CREATED="1577179229340" ID="ID_1981253136" MODIFIED="1577182620460" TEXT="GearsOS での HoareLogic を用いた実装と検証"> +<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179287926" ID="ID_1165984884" MODIFIED="1577182620459" POSITION="right" TEXT="はじめに"> +<font NAME="SansSerif" SIZE="19"/> +</node> +<node CREATED="1577179299434" ID="ID_372153190" MODIFIED="1577182620459" POSITION="right" TEXT="Continuation based C"> +<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179793073" ID="ID_1307352612" MODIFIED="1577182620458" TEXT="CodeGear"> +<font NAME="SansSerif" SIZE="19"/> +</node> +<node CREATED="1577179805065" ID="ID_1214581036" MODIFIED="1577182620458" TEXT="DataGear"> +<font NAME="SansSerif" SIZE="19"/> +</node> +<node CREATED="1577179939889" ID="ID_1188251116" MODIFIED="1577182620458" TEXT="Meta CodeGear,DataGear"> +<font NAME="SansSerif" SIZE="19"/> +</node> +</node> +<node CREATED="1577179329845" ID="ID_1008088180" MODIFIED="1577182644207" POSITION="right" TEXT="Agda"> +<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577182682220" ID="ID_1522532015" MODIFIED="1577182690635" TEXT="入門"> +<font NAME="SansSerif" SIZE="18"/> +</node> +</node> +<node CREATED="1577179349458" ID="ID_739318439" MODIFIED="1577182637067" POSITION="right" TEXT="Hoare Logic"> +<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179370109" ID="ID_809388614" MODIFIED="1577182664147" TEXT="whileTest (Hoare Logic の例)"> +<font NAME="SansSerif" SIZE="19"/> +</node> +<node CREATED="1577179360283" ID="ID_501247037" MODIFIED="1577182670343" TEXT="Agda と Hoare Logic"> +<font NAME="SansSerif" SIZE="20"/> +<node CREATED="1577179441565" ID="ID_1388092541" MODIFIED="1577182620455" TEXT="記述"> +<font NAME="SansSerif" SIZE="19"/> +</node> +<node CREATED="1577179468054" ID="ID_545191696" MODIFIED="1577182620454" TEXT="Soundness 関連"> +<font NAME="SansSerif" SIZE="19"/> +</node> +</node> +</node> +<node CREATED="1577179318540" ID="ID_402362033" MODIFIED="1577182658769" POSITION="right" TEXT="Continuation based C と Agda"> +<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577182741707" ID="ID_1751180005" MODIFIED="1577182751755" TEXT="HoareLogic"> +<font NAME="SansSerif" SIZE="16"/> +</node> +</node> +<node CREATED="1577182694546" ID="ID_764943519" MODIFIED="1577182712199" POSITION="right" TEXT="BinaryTree と RedBlack Tree(Agda)"> +<font NAME="SansSerif" SIZE="15"/> +<node CREATED="1577182754406" ID="ID_1200857877" MODIFIED="1577182760901" TEXT="HoareLogic"> +<font NAME="SansSerif" SIZE="17"/> +</node> +<node CREATED="1577182712718" ID="ID_283296995" MODIFIED="1577182732895" TEXT="BinaryTree の 条件つきのやつの話"> +<font NAME="SansSerif" SIZE="16"/> +</node> +<node CREATED="1577182765996" ID="ID_740598781" MODIFIED="1577182773370" TEXT="RedBlackTree"> +<font NAME="SansSerif" SIZE="16"/> +</node> +</node> +<node CREATED="1577179295267" ID="ID_747054126" MODIFIED="1577182620450" POSITION="right" TEXT="まとめ"> +<font NAME="SansSerif" SIZE="19"/> +</node> +<node CREATED="1577179315283" ID="ID_1375073128" MODIFIED="1577182620457" POSITION="left" TEXT="Gears OS"> +<font NAME="SansSerif" SIZE="19"/> +<node CREATED="1577179820187" ID="ID_519165935" MODIFIED="1577182654290" TEXT="-interface"> +<font NAME="SansSerif" SIZE="19"/> +</node> +<node CREATED="1577179862592" ID="ID_1991286966" MODIFIED="1577182620456" TEXT="Gears OS の検証"> +<font NAME="SansSerif" SIZE="19"/> +</node> +</node> +<node CREATED="1577179492520" ID="ID_1327764636" MODIFIED="1577182620454" POSITION="left" TEXT="できたらいいな(Binary-Tree)"> +<font NAME="SansSerif" SIZE="19"/> +</node> +</node> +</map>