# HG changeset patch # User ryokka # Date 1516867242 -32400 # Node ID 46d543c569d2bdaa8dd548f182e9931d139f1f04 add MindMap diff -r 000000000000 -r 46d543c569d2 final_main/Makefile --- /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." diff -r 000000000000 -r 46d543c569d2 final_main/bibliography.tex --- /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} diff -r 000000000000 -r 46d543c569d2 final_main/chapter1.tex --- /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} diff -r 000000000000 -r 46d543c569d2 final_main/chapter2.tex --- /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理論使ったりするといい +%% かんじにできるんじゃないかな + + + diff -r 000000000000 -r 46d543c569d2 final_main/chapter3.tex --- /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 が存在する。 diff -r 000000000000 -r 46d543c569d2 final_main/chapter4.tex --- /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での証明とかその解説とか? diff -r 000000000000 -r 46d543c569d2 final_main/chapter5.tex --- /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での証明} + + + + diff -r 000000000000 -r 46d543c569d2 final_main/chapter6.tex --- /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{まとめ} + diff -r 000000000000 -r 46d543c569d2 final_main/fig/ryukyu.pdf Binary file final_main/fig/ryukyu.pdf has changed diff -r 000000000000 -r 46d543c569d2 final_main/main.tex --- /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} diff -r 000000000000 -r 46d543c569d2 final_main/mythesis.sty --- /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}{要 旨} diff -r 000000000000 -r 46d543c569d2 final_main/thanks.tex --- /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} + + diff -r 000000000000 -r 46d543c569d2 thesis.mm --- /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 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +