Mercurial > hg > Papers > 2015 > atton-thesis
changeset 4:cc74def322a8
Add introduction
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 06 Feb 2015 15:41:43 +0900 |
parents | 4cac648eb36e |
children | bafd7d4af924 |
files | introduction.tex main.tex |
diffstat | 2 files changed, 28 insertions(+), 43 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/introduction.tex Fri Feb 06 15:41:43 2015 +0900 @@ -0,0 +1,11 @@ +\chapter{研究目的} +本研究ではプログラムの信頼性の向上を目標とする。 + +プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。 +例えば仕様が未定義の挙動によってプログラムが停止することや、プログラムに記述した誤った条件式よる異なる計算結果、実行環境やパラメタの変化に対応できずに正しくない動作が引き起されることなどがある。 +信頼性を低下させる原因が増えるタイミングの多くはプログラムを変更した時であると考えた。 + +本研究ではプログラムの変更を Monad を用いて形式化する。 +プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。 +信頼性を保ちながら開発するための手法や、変更を形式的に行なうことによって可能となる信頼性の解析などを提案する。 +また、形式化した論理の観点からプログラムの変更が持つ性質などを解析し、ソフトウェア開発手法の指針を提案する。
--- a/main.tex Tue Feb 03 17:55:53 2015 +0900 +++ b/main.tex Fri Feb 06 15:41:43 2015 +0900 @@ -4,13 +4,15 @@ \usepackage{multirow} \usepackage{here} \setlength{\itemsep}{-1zh} -\title{} +\title{圏によるプログラムの変更の形式化} \icon{ - \includegraphics[width=80mm,bb=0 0 595 842]{fig/ryukyu.pdf} - } -\year{平成Y年度 卒業論文} + \includegraphics[width=80mm,bb=0 0 595 842]{fig/ryukyu.pdf} +} +\year{平成26年度 卒業論文} \belongto{琉球大学工学部情報工学科} -\author{0957 \\ 指導教員 {} } +\author{115763K 比嘉健太 \\ 指導教員 {河野真治} } + + %% %% プリアンブルに記述 %% Figure 環境中で Table 環境の見出しを表示・カウンタの操作に必要 @@ -30,22 +32,16 @@ \pagenumbering{roman} \setcounter{page}{0} -\tableofcontents % 目次 -\listoffigures % 図目次 -\listoftables % 表目次 +\tableofcontents % 目次 +\listoffigures % 図目次 +\listoftables % 表目次 -%以下のように、章ごとに個別の tex ファイルを作成して、 -% main.tex をコンパイルして確認する。 -%章分けは個人で違うので下のフォーマットを参考にして下さい。 - -% FIXME: Temporary table of contents -\chapter{研究背景と目的} +\input{introduction} \chapter{プログラムの変更を表現する Delta Monad} -\section{Delta の データ定義} -\section{Delta の Functor 定義} -\section{Delta の Monad 定義} -\section{Delta を用いたプログラムの変更} +\section{Delta の定義} +\section{Haskell における Delta Monad の実装例} +\section{Delta を用いたプログラムの変更の記述} \chapter{Categorical Definitions of Monad} \section{Category} @@ -54,21 +50,11 @@ \section{Monad} \section{Monads in Functional Programming} -\chapter{Disposition of Category?} -\section{Product} -\section{CoProduct} -\section{Limit} -\section{CoLimit} -\section{Equalizer ?} -\section{Indexed Category} -\section{Delta との対応} - \chapter{Agda による証明手法} \section{Natural Deduction} \section{Curry-Howard Isomorphism} \section{Agda による証明} \section{Reasoning} -\section{Example?} \chapter{Delta が Monad である証明} \section{Agda における Functor 則} @@ -81,21 +67,9 @@ \section{DeltaM が Monad 則を満たす証明} \chapter{結論} -% -% % はじめに -% \input{chapter1.tex} -% -% % 基礎概念 -% \input{chapter2.tex} -% -% % 実験 -% \input{chapter3.tex} -% -% % 他の論文との比較 -% %\input{chapter4.tex} -% -% % 今後の課題 -% \input{future.tex} + +% 今後の課題 +\input{future.tex} % 参考文献 \input{bibliography.tex}