Mercurial > hg > Papers > 2018 > ryokka-thesis

comparison final_main/chapter1.tex @ 7:28f900230c26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final_pre
author ryokka
date Mon, 19 Feb 2018 23:32:24 +0900
parents 2155c6ff589f
children 50a27cc71ca7
comparison
equal deleted inserted replaced
6:d927f6b3d2b3 7:28f900230c26
1 \chapter{はじめに} 1 \chapter{A}
2 \label{chap:introduction} 2 \label{chap:introduction}
3 \pagenumbering{arabic} 3 \pagenumbering{arabic}
4 4
5 % 序論の目安としては1枚半ぐらい． 5 % 序論の目安としては1枚半ぐらい．
6 % 英語発表者は，最終予稿の「はじめに」の英訳などを載せてもいいかも． 6 % 英語発表者は，最終予稿の「はじめに」の英訳などを載せてもいいかも．
8 %% 想定外の挙動をしてほしくない 8 %% 想定外の挙動をしてほしくない
9 9
10 10
11 動作するプログラム(ソフトウェア)は高い信頼性を持つことが望ましい。 11 動作するプログラム(ソフトウェア)は高い信頼性を持つことが望ましい。
12 12
13 % しかし、既存の言語で関数より細かい単位に分割することは難しい。そのために当研究 13 プログラムの信頼性を保証するにはプログラムが期待される仕様を満たすことを検証する手法と、その仕様を直接証明する手法が存在している。
14 % 室ではコードの単位を CodeGear ~
15 プログラムの信頼性を保証するにはプログラムが期待される仕様を満たすことを検証する手法と、その仕様を直接証明する手法が存在している。
16
17
18 % しかし、期待される仕様を満たすかを検証する際、仕様が大きくなるに連れ指数関数的に検証する項が増えてしまう。そのため、ここでは仕様を直接証明する手法を用いている。
19 14
20 そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している。 15 そのために当研究室では検証しやすい単位として CodeGear、DataGearという単位を用いてプログラムを記述する手法を提案している。
21
22 %% コードセグメントは通常の言語での関数を細かくしたものとしてよい？
23 16
24 17
25 本研究では CbC を用いて Tree、 Stack を実装し、等価な Agda の実装を使ってその仕 18 本研究では CbC を用いて Tree、 Stack を実装し、等価な Agda の実装を使ってその仕
26 様の一部を証明した。 19 様の一部を証明した。
27 20