Mercurial > hg > Papers > 2018 > ryokka-thesis
changeset 0:46d543c569d2
add MindMap
| author | ryokka |
|---|---|
| date | Thu, 25 Jan 2018 17:00:42 +0900 |
| parents | |
| children | 0035f6d4826f |
| files | final_main/Makefile final_main/bibliography.tex final_main/chapter1.tex final_main/chapter2.tex final_main/chapter3.tex final_main/chapter4.tex final_main/chapter5.tex final_main/chapter6.tex final_main/fig/ryukyu.pdf final_main/main.tex final_main/mythesis.sty final_main/thanks.tex thesis.mm |
| diffstat | 13 files changed, 539 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/Makefile Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,90 @@ +# target and root file name +TARGET = main + +# class files +CLASS_FILE = + +# figure pass +FIG_DIR = ./fig + +# ebb or extractbb +EBB = extractbb + +# dependent document files +TEX_FILES = \ + bibliography.tex \ + chapter*.tex \ + thanks.tex \ + +# dependent image files +SVG_FILES = + +# use bibtex or not (yes|no) +BIBTEX_ENABLED = no + +# commands to compile document +LATEX = platex +BIBTEX = pbibtex +DVIPDF = dvipdfmx +DVIPS = dvips + +# generated files +DVI_FILE = $(TARGET).dvi +PDF_FILE = $(TARGET).pdf +PS_FILE = $(TARGET).ps +TEX_FILES += $(TARGET).tex +EPS_FILES = $(SVG_FILES:%.svg=%.eps) +AUX_FILES = $(TEX_FILES:%.tex=%.aux) +GENERATED_FILE = \ + $(EPS_FILES) \ + $(DVI_FILE) \ + $(PDF_FILE) \ + $(AUX_FILES) \ + $(TARGET).log \ + $(TARGET).toc \ + $(TARGET).bbl \ + $(TARGET).blg \ + $(TARGET).lof \ + $(TARGET).lol \ + texput.log + +.DEFAULT_GOAL = pdf + +.PHONY : pdf +pdf : $(PDF_FILE) + open $(TARGET).pdf +$(PDF_FILE) : $(DVI_FILE) $(TEX_FILES) $(EPS_FILES) $(CLASS_FILE) + $(DVIPDF) $(TARGET) + +.PHONY : ps +ps : $(PS_FILE) +$(PS_FILE) : $(DVI_FILE) $(TEX_FILES) $(EPS_FILES) $(CLASS_FILE) + $(DVIPS) $(TARGET) + +.PHONY : dvi +dvi : $(DVI_FILE) +$(DVI_FILE) : $(TEX_FILES) $(EPS_FILES) $(CLASS_FILE) + $(LATEX) -halt-on-error $(TARGET) +ifeq ($(BIBTEX_ENABLED),yes) + $(BIBTEX) $(TARGET) +endif + $(LATEX) -halt-on-error $(TARGET) + $(LATEX) -halt-on-error $(TARGET) + +%.eps : %.svg + inkscape --export-area-drawing --without-gui --file="$<" --export-eps="$@" + +.PHONY : clean +clean: + rm -f $(GENERATED_FILE) + +.PHONY : help +help: + @echo "make dvi" + @echo " Make DVI file from tex documents." + @echo "make pdf" + @echo " Make PDF file from DVI file." + @echo "make ps" + @echo " Make PS file from DVI file." + @echo "make clean" + @echo " Remove all generated files."
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/bibliography.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,25 @@ +% 参考文献 +\def\line{−\hspace*{-.7zw}−} + +\begin{thebibliography}{99} +%\bibitem{*}内の * は各自わかりやすい名前などをつけて、 +%論文中には \cite{*} のように使用する。 +%これをベースに書き換えた方が楽かも。 +%書籍、論文、URLによって若干書き方が異なる。 +%URLを載せる人は参考にした年月日を最後に記入すること。 + +\bibitem{比嘉健太} +{比嘉健太, 河野真治}: メタ計算を用いた Continuation based C の検証手法 +, 琉球大学工学部情報工学科平成 29 年度学位論文(修士) (2016). + +% \bibitem{gears} +% {伊波立樹, 東恩納琢偉, 河野真治}: Code Gear、Data Gear に基づく OS のプロトタイプ +% , 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS) (2016). + +% \bibitem{llvm} +% The LLVM Compiler Infrastructure. \\\verb|http://llvm.org| + +% \bibitem{llvm_ir} +% LLVM Language Reference Manual. \\\verb|http://llvm.org/docs/LangRef.html| + +\end{thebibliography}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/chapter1.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,42 @@ +\chapter{(タイトル)} +\label{chap:introduction} +\pagenumbering{arabic} + +% 序論の目安としては1枚半ぐらい． +% 英語発表者は，最終予稿の「はじめに」の英訳などを載せてもいいかも． + +%% 想定外の挙動をしてほしくない + + + 動作するプログラム(ソフトウェア)は高い信頼性を持つことが望ましい。 + プログラムの信頼性を保証するにはプログラムが期待される仕様を満たすことを検証する手法と、その仕様を直接証明する手法が存在している。 + しかし、期待される仕様を満たすかを検証する際、仕様が大きくなるに連れ指数関数的に検証する項が増えてしまう。そのため、ここでは仕様を直接証明する手法を利用している。 + 証明では + +そのために当研究室ではコードセグメント、データセグメントという単位を用いてプログラムを記述する手法を提案している。 +%% コードセグメントは通常の言語での関数を細かくしたものとしてよい？ + +本研究では CbC を用いて UnblanceTree を実装し、等価な Agda でその一部を証明する。 +%% 動作するプログラムの信頼性を保証したい + +%% そのために当研究室ではコードセグメント、データセグメントという単位を用いてプログラムを記述する手法を提案する + +%% 処理の単位であるコードセグメントはメタ計算によって接続される + +%% メタ計算を切り替えることでコードセグメントを変更することなくプログラムの性質を検証することができる + +%% 証明を使い、プログラムの信頼性を保証できるようにしたい + +%%% +% やってること、やりたいことはAgdaとCbC言語で等価なプログラムを書き、証明すること +% Agdaではunblancedなbinary tree を作るとこまできた +% CbC側ではBalancedなredBlackTreeを作るところまではきている +%%% + +% なんでAgda で証明するの ? Agda である理由は ? +% 他論文でも実装と異なる言語で証明している例は多い。 +% もともとの言語が証明支援ではない。関数型言語(証明支援系言語)でのプログラミングは手続き型のプログラミングと異なる + +%\section{論文の構成} + +%\section{Introduction}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/chapter2.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,27 @@ +\chapter{Continuation based C} +%% CbCとはなにか？どのようなものか？どのようにしてなりたっているか？ + + +Continuation based C (以下CbC)は当研究室で開発しているプログラミング言語である。 +CbC は殆どC言語と同じ構文を持っているが、C言語よりアセンブラに近い記述をすることで細 +かい動作を +CodeSegment、 DataSegment という単位を使いプログラムを記述する。 + +\section{CodeSegmentとDataSegment} +%% CodeSegmentとはなにか？どのようなものか？くらいかけばよしかな +CodeSegmentは処理の単位である。入力を受け取り、処理を行い出力を行う。 + + + +% \section{DataSegment} +%% DataSegmentとはなにか？どのようなものか +DataSegmentはCodeSegmentで扱うデータの単位であり、処理に必要なデータがすべて入っている。 + +\section{CbC上でのCodeSegment、DataSegmentの表現} %% 例題 +%% CbCの具体的なコード類。どういう風に書くのか〜くらい +%% Metaな話は今書いてもどうせ使わないので検証に使える〜くらいで置いておく。Meta +%% 部分は生成でき、そこで検証用の動作をする感じでは？hora理論使ったりするといい +%% かんじにできるんじゃないかな + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/chapter3.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,7 @@ +\chapter{Agda} + +CbCの章では CodeSegment 、 DataSegment が部分型で定義 + +\section{Agda} + +型システムを用いて証明を行うことができる言語として Agda が存在する。
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/chapter4.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,5 @@ +\chapter{CbCとAgda} + +\section{} +実装部分。 +Agdaでの実装とかAgdaでの証明とかその解説とか?
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/chapter5.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,13 @@ +\chapter{Agdaでの証明} + +前章ではノーマルレベルでのAgdaが正しく動くことを示した。 + +本章では + +\section{自然演繹} + +\section{Agdaでの証明} + + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/chapter6.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,2 @@ +\chapter{まとめ} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/main.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,92 @@ +\documentclass[a4j,12pt]{jreport} +\usepackage[dvipdfmx]{graphicx} +\usepackage{mythesis} +\usepackage{multirow} +\usepackage{here} +\usepackage{listings} +\lstset{ + language={C}, + basicstyle={\footnotesize\ttfamily}, + identifierstyle={\footnotesize}, + commentstyle={\footnotesize\itshape}, + keywordstyle={\footnotesize\bfseries}, + ndkeywordstyle={\footnotesize}, + stringstyle={\footnotesize\ttfamily}, + frame={tb}, + breaklines=true, + columns=[l]{fullflexible}, + numbers=left, + xrightmargin=0zw, + xleftmargin=3zw, + numberstyle={\scriptsize}, + stepnumber=1, + numbersep=1zw, + lineskip=-0.5ex +} +\def\lstlistingname{リスト} +\def\lstlistlistingname{リスト目次} +\setlength{\itemsep}{-1zh} +\title{CbC 言語とプログラムの証明} +\icon{ + \includegraphics[width=80mm,bb=0 0 595 642]{fig/ryukyu.pdf} %%元は 642じゃなくて842 +} +\year{平成30年度 卒業論文} +\belongto{琉球大学工学部情報工学科} +\author{145750B 外間 \\ 指導教員 {河野 真治} } +%% +%% プリアンブルに記述 +%% Figure 環境中で Table 環境の見出しを表示・カウンタの操作に必要 +%% +\makeatletter +\newcommand{\figcaption}[1]{\def\@captype{figure}\caption{#1}} +\newcommand{\tblcaption}[1]{\def\@captype{table}\caption{#1}} +\makeatother +\setlength\abovecaptionskip{0pt} + +\begin{document} + +% タイトル +\maketitle +\baselineskip 17pt plus 1pt minus 1pt + +\pagenumbering{roman} +\setcounter{page}{0} + +\tableofcontents % 目次 +\listoffigures % 図目次 +%\listoftables % 表目次 +\lstlistoflistings + +%以下のように、章ごとに個別の tex ファイルを作成して、 +% main.tex をコンパイルして確認する。 +%章分けは個人で違うので下のフォーマットを参考にして下さい。 + +% はじめに +\input{chapter1.tex} + +% 基礎概念 +\input{chapter2.tex} + +% 実験 +\input{chapter3.tex} + +% 実装 +\input{chapter4.tex} + +% 評価 +\input{chapter5.tex} + +% 結論 +\input{chapter6.tex} + +% 参考文献 +\input{bibliography.tex} + +% 謝辞 +\input{thanks.tex} + +\appendix +% 付録 +%\input{appendix.tex} + +\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/mythesis.sty Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,156 @@ +% +% 卒業論文スタイルファイル(mythesis.sty) +% version 1.0e +% +% ver 1.0e 02/07/2000 since +% usage: + +%\documentclass[a4j]{jreport} +%\usepackage{master_paper} +% +% +%\title{卒論タイトル \\ 長い} +%\etitle{\pLaTeX2e style test file for Teri's thesis } +%\year{平成11年度} +%\belongto{琉球大学大学工学部\\ 情報工学科} +%\author{豊平 絵梨} +% +%\begin{document} +% +%\maketitle +% +%%要旨 +%\input{abstract.tex} +% +%%目次 +%\tableofcontents +% +%%図目次 +%\listoffigures +% +%%表目次 +%\listoftables +% +%%第一章 +%\input{chapter1.tex} +%%chapter1.texの\chapter{}の後ろに次のコマンドを追加してください。 +%%ページカウントがリセットされ、ページ数がアラビア文字になります。 +%% \pagenumbering{arabic} +%%第二章 +%\input{chapter2.tex} +%%第三章 +%\input{chapter3.tex} +% +%%付録 +%\input{appendix.tex} +% +%%謝辞 +%%\input{thanx.tex} +% +%%参考文献 +%\input{biblography.tex} +% +%\end{document} + + +%長さ設定 +%\setlength{\topmargin}{-30mm} +%\addtolength{\oddsidemargin}{-15mm} +%\addtolength{\textwidth}{60mm} + +\topmargin -1in \addtolength{\topmargin}{35mm} +\headheight 0mm +\headsep 0mm +\oddsidemargin -1in \addtolength{\oddsidemargin}{30mm} +%\evensidemargin -1in \addtolength{\evensidemargin}{8mm} +\textwidth 160mm +\textheight 230mm +%\footheight 0mm +%\footskip 0mm +%\pagestyle{empty} + + +%年度 +\def\@year{} +\def\year#1{\gdef\@year{#1}} +%英文タイトル +\def\@etitle{} +\def\etitle#1{\gdef\@etitle{#1}} +%アイコン +\def\@icon{} +\def\icon#1{\gdef\@icon{#1}} +%所属 +\def\@belongto{} +\def\belongto#1{\gdef\@belongto{#1}} + +%表紙 +\renewcommand{\maketitle}{% +\newpage\null +\thispagestyle{empty} +\vskip 0cm% +\begin{center}% +\let\footnote\thanks + {\huge \@year \par}% + \vskip 3em% + {\Huge \@title \par}% + \vskip 1em% + {\huge \@etitle \par}% + \vskip 8em% + {\huge \@icon \par}% + \vskip 0.5em% + {\huge \@belongto \par}% + \vskip 1.0em% + {\huge \@author \par}% + +\end{center}% +\par\vskip 1.5em +} + + +%abstract +\renewenvironment{abstract}{% + \titlepage + \thispagestyle{empty} + \null\vfil + \@beginparpenalty\@lowpenalty + {\Huge \bfseries \abstractname}% + \begin{center}% + \@endparpenalty\@M + \end{center} +}% + + +%目次 +\renewcommand{\tableofcontents}{% + \pagestyle{plain} + \if@twocolumn\@restonecoltrue\onecolumn + \else\@restonecolfalse\fi + \chapter*{\contentsname + \@mkboth{\contentsname}{\contentsname}% + } \pagenumbering{roman}\@starttoc{toc}% + \if@restonecol\twocolumn\fi +} + +%章 +\renewcommand{\chapter}{% + \pagestyle{plain} + \if@openright\cleardoublepage\else\clearpage\fi + \thispagestyle{jpl@in}% + \global\@topnum\z@ + \@afterindentfalse + \secdef\@chapter\@schapter} + + +\renewcommand{\prepartname}{} %\renewcommand{\prepartname}{第} +\renewcommand{\postpartname}{部} +\renewcommand{\prechaptername}{第}%\renewcommand{\prechaptername}{第} +\renewcommand{\postchaptername}{章} +\renewcommand{\contentsname}{目 次} +\renewcommand{\listfigurename}{図 目 次} +\renewcommand{\listtablename}{表 目 次} +\renewcommand{\bibname}{参考文献} +\renewcommand{\indexname}{索 引} +\renewcommand{\figurename}{図} +\renewcommand{\tablename}{表} +\renewcommand{\appendixname}{付 録} +\renewcommand{\abstractname}{要 旨}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/thanks.tex Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,17 @@ +\chapter*{謝辞} +\thispagestyle{empty} + +%基本的な内容は以下の通り．参考にしてみて下さい． +%厳密な決まりは無いので，個々人の文体でも構わない． +%GISゼミや英語ゼミに参加した人はその分も入れておく． +%順番は重要なので気を付けるように．(提出前に周りの人に確認してもらう．) + +\hspace{1zw} + +謝辞だよ。 + +%% \begin{flushright} +%% % 2018年 3月 \\ 外間政尊 +%% \end{flushright} + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thesis.mm Thu Jan 25 17:00:42 2018 +0900 @@ -0,0 +1,63 @@ +<map version="1.1.0"> +<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> +<node CREATED="1516447600591" ID="ID_1323189017" MODIFIED="1516447624027" TEXT="thesis"> +<node CREATED="1516447625087" ID="ID_1724518003" MODIFIED="1516447637346" POSITION="left" TEXT="はじめに"> +<node CREATED="1516448006125" ID="ID_801881892" MODIFIED="1516448107906" TEXT="動作するプログラムの信頼性を保証したい"/> +<node CREATED="1516448247561" ID="ID_951851740" MODIFIED="1516448282443" TEXT="CodeSegment,DataSegmentという単位でプログラムを書く手法を提案している"/> +<node CREATED="1516448220906" ID="ID_182832086" MODIFIED="1516448412313" TEXT="CbC(Continuation based C )ではこのようにプログラムを記述することでメタ計算として検証をすることができた（あっとんさんの論文）"/> +<node CREATED="1516448414254" ID="ID_1047962267" MODIFIED="1516448573215" TEXT="CbCでは自身で証明をすることができない為、（何らかの理由で）Agdaを使って証明する"/> +<node CREATED="1516448574477" ID="ID_1442131681" MODIFIED="1516453035591" TEXT="本研究ではAgdaでCodeSegment、DataSegmentという単位を使ってCbCで記述したものと等価なUnbarrancedTreeを作り、ノードを入れる際ノードがなくならないこと、などを証明をする"/> +</node> +<node CREATED="1516447638226" ID="ID_1889545574" MODIFIED="1516448672959" POSITION="left" TEXT="基礎概念"> +<node CREATED="1516448673422" ID="ID_1274177968" MODIFIED="1516448683325" TEXT="CbC"> +<node CREATED="1516448708973" ID="ID_815925469" MODIFIED="1516454414422" TEXT="CodeSegmentとは"> +<node CREATED="1516454422237" ID="ID_661052887" MODIFIED="1516454424583" TEXT="例題"/> +</node> +<node CREATED="1516448719701" ID="ID_1017753652" MODIFIED="1516454421110" TEXT="DataSegmentとは"> +<node CREATED="1516454425392" ID="ID_221829180" MODIFIED="1516454427407" TEXT="例題"/> +</node> +</node> +<node CREATED="1516448688109" ID="ID_594761054" MODIFIED="1516448692742" TEXT="証明"> +<node CREATED="1516454132267" ID="ID_1490526606" MODIFIED="1516693045587" TEXT="自然証明"> +<node CREATED="1516454431900" ID="ID_1113949900" MODIFIED="1516454434111" TEXT="例題"/> +</node> +<node CREATED="1516454140637" ID="ID_1834687592" MODIFIED="1516455188550" TEXT="カリーハワード同型対応"/> +</node> +<node CREATED="1516448684110" ID="ID_1770419109" MODIFIED="1516448687493" TEXT="Agda"> +<node CREATED="1516454190133" ID="ID_445682748" MODIFIED="1516454207271" TEXT="その他の証明支援系"/> +<node CREATED="1516454167956" ID="ID_1326840818" MODIFIED="1516454171204" TEXT="記述方法"/> +<node CREATED="1516454171715" ID="ID_1880237124" MODIFIED="1516454184781" TEXT="例題"/> +</node> +<node CREATED="1516448778576" ID="ID_1454457815" MODIFIED="1516453085568" TEXT="Tree,RedBlackTree"/> +</node> +<node CREATED="1516448781436" ID="ID_732614714" MODIFIED="1516448784603" POSITION="left" TEXT="実験"> +<node CREATED="1516448792793" ID="ID_590034820" MODIFIED="1516448919993" TEXT="Treeの作成方針"/> +<node CREATED="1516448843266" ID="ID_1177321611" MODIFIED="1516454291651" TEXT="証明方針の検討,実装時の改善"/> +</node> +<node CREATED="1516448766134" ID="ID_712304841" MODIFIED="1516448768937" POSITION="left" TEXT="実装"> +<node CREATED="1516448769994" ID="ID_1122278060" MODIFIED="1516453267632" TEXT="CbCでの実装"/> +<node CREATED="1516453268445" ID="ID_1239636691" MODIFIED="1516453272713" TEXT="Agdaでの実装"/> +<node CREATED="1516453273168" ID="ID_1420286449" MODIFIED="1516454130460" TEXT="Agdaでの証明,解説"/> +</node> +<node CREATED="1516455668900" ID="ID_155403381" MODIFIED="1516455671387" POSITION="left" TEXT="評価"> +<node CREATED="1516455671828" ID="ID_1828774278" MODIFIED="1516455677370" TEXT="?"/> +</node> +<node CREATED="1516448787093" ID="ID_1477806830" MODIFIED="1516448789500" POSITION="left" TEXT="結論"> +<node CREATED="1516453116787" ID="ID_1750859738" MODIFIED="1516453146188" TEXT="TreeをCodeSegment,DataSegmentを用いて二つの言語で記述した"/> +<node CREATED="1516453146841" ID="ID_495843685" MODIFIED="1516695852072" TEXT="等価なコードができた?"/> +<node CREATED="1516453179338" ID="ID_710713278" MODIFIED="1516695815136" TEXT="証明支援器を使ってunBalanceなTreeができることを証明した?"/> +<node CREATED="1516693502350" ID="ID_1803347987" MODIFIED="1516695887153" TEXT="その他、今後の話"> +<node CREATED="1516693505485" ID="ID_727445874" MODIFIED="1516693962403" TEXT="CbCのコンパイル時にTypeCheckingもできるかもしれないねみたいなはなし"/> +</node> +</node> +<node CREATED="1516695662563" ID="ID_1054440656" MODIFIED="1516695667362" POSITION="right" TEXT="章構成"> +<node CREATED="1516695644106" ID="ID_736329900" MODIFIED="1516695909066" TEXT="研究背景"/> +<node CREATED="1516695675644" ID="ID_922716453" MODIFIED="1516695971900" TEXT="CbC"/> +<node CREATED="1516695693068" ID="ID_1567452235" MODIFIED="1516695739269" TEXT="証明とプログラミング"/> +<node CREATED="1516695699548" ID="ID_1160729877" MODIFIED="1516695701947" TEXT="Agda"/> +<node CREATED="1516695711821" ID="ID_886806884" MODIFIED="1516695769605" TEXT="CbCとAgda"/> +<node CREATED="1516695770479" ID="ID_289839920" MODIFIED="1516695935530" TEXT="Agdaでの証明"/> +<node CREATED="1516695962331" ID="ID_1727743322" MODIFIED="1516695964397" TEXT="まとめ"/> +</node> +</node> +</map>