changeset 15:0ba2de3295b8

*** empty log message ***
author atsuki
date Mon, 18 Feb 2008 01:15:24 +0900
parents 39242aece5fc
children 6bd5455a9335
files paper/chapter1.tex
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/paper/chapter1.tex	Sun Feb 17 14:24:23 2008 +0900
+++ b/paper/chapter1.tex	Mon Feb 18 01:15:24 2008 +0900
@@ -20,9 +20,9 @@
 による実装とその実装に対する検証手法を提案している。
 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
-また、CbCで記述されたプログラムは非決定性状態遷移記述と近い構造になるという性質がある。
+また、CbCで記述されたプログラムは決定性状態遷移記述と近い構造になるという性質がある。
 
-本研究は、CbCが非決定性状態遷移記述と相性の良い言語であることに着目し、
+本研究は、CbCが決定性状態遷移記述と相性の良い言語であることに着目し、
 非決定性状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
 状態を展開する際に、線形時相論理も同時に展開することにより検証を行うことを目的としている。
 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用される。