プログラム・デバッグにおける記号的実行の応用

　 M 刪 01 跚 orS ▲o ▲m I期 r：TVTS 　ov 　TaCHHOLOGy 　 　 Vo1　19

，

　No

．

1

，

　1985

プ

ロ

グ ラ

ム ・

デ

バ ッ

グ

に

お

け

る

記 号 的 実

行

の

_{応 用}

深 沢 良

彰

＊

・袖 山

欣 大

＊ ＊

・門 倉 敏 夫

＊ ＊

An

　

Application

　_of　

the

　

Symbolic

　

Execution

　_on 　

Program

　

Debugging

Yoshiaki

　

FuKAzAwA

，　

Yoshihiro

　

SoDEYAMA

　and 　

Toshio

　

KADoKuRA

　 　In　this　paper

，

　we 　describe　the　program 　debugging 　system 　

based

　on　the　symbolic 　execution

．

　 　The 　

basic

　idea　of　the　symbolic 　execution 　

is

　to　allow 　variables 　to　take　on 　symbolic 　vaLues 　as　 well

as　real 　values

．

　

That

　is

，

　each 　symbolic 　execution 　result　may 　

be

　equivalent 　to　a　large　number 　of　usual

test　cases

．

　 But　the　symbolic 　execution 　of　whole 　program 　is　not　generally　practical　because　of　the　vast

cornputational 　power 　and 　the　poor　loop　management

．

　 　In　order 　to　get　over 　two　kinds　of　defects　above 　and 　to　make 　the　symbolic 　execution 　more 　practical

，

our 　 system 　 has　paid　attention 　to　the　following　two 　points

．

　 First

，　this　system 　symbolically 　executes

only 　a　partof　the program 　according 　tothe　user 　specification 　of　necessary variables

．



Namely ，

execu

・

tion　paths　of　no 　interest　are　excluded 　by　means 　of　the　simple 　

data

　

now

　analysis

．

　

Second

，

100p

　Inanage

・

ment 　

is

　

improved

　

by

　the　case　analysis 　of　the　

feature

　oHoops

．

　 Program 　loops　are　classified　into　the

de丘nite 　iteration　loops

，

　the 負nite 　iteration　Ioops　and 　the　indefinite　

iteration

　loops

．



And

　that

，

every 　loops

are　processed 三n　terms　of　this　classification 　respectively

．

　　

The

　target　language 　of　this　system 　is　a　subset 　of　

PLII．

　 Most 　of　this　system 　has　been　implemented

by　

PL

_！

I

　under 　

CMS

　of　

IBM4341

　processor　system

．

　

One

　part　of　this　system

，

　symbolic 　expression 　hand1

・

ing　module

，

　is　processed　by　a　PROLOG 　interpreter

．

　 　 We 　have　obtained 　su 伍 cient 　results 　by　the　application 　 of　this　 system 　 to　some 　 error　cases

．

　 The

results 　are 　compared 　to　those　of　conventional 　debugging 　system 　and 　to　those　of　other 　symbolic 　execu

・

tlon　system

．

1．

は じ め に 　プ ロ グ ラム の 記号 的実行と は， プロ グ ラ ムに入力 する デ

ー

タを

，

ある 固有の値で は な く

，

すべ て の 値を代 表 す るこ との で ぎる記 号の ま まプ 卩 グ ラ ム を実 行 する こ とを 言 う6

・

13） 。 記 号 的 実 行は， プ P グ ラム に入力する デ

ー

タ を人 間の憶 測に よっ て生 成 するもの で はない の で

，

理 論 的に プロ _グラ ムに起こ り得る_総てのパ ス を発見 する こ と がで きる と 言 う特徴を持つ

。

_その た め

，

プロ グラム の テ ス ト， デバ ッ グ時におい て， プロ グ ラム の 制御構造 を 解 析 するツ

ー

ル と して非 常に有 用 なほか

，

テス トさ れ るブ ＊ 情 報工 学 科 　 講 師 　 ＊ ＊ 早 稲田大 学理 工学部　電 気 工 学 科　昭 和

59

年

11

月

27

目受付 ロ グラ ムに与 える テス ト

・

デ

ー

タ の 自動 生 成P）_や ， プ ロ グラ ム がユ

ー

ザの仕 様 どお りに_働くか を 検 証 する

，

プロ グ ラムの正 当 性の_証明5

・

7

・

e ）な どに も応用 さ れて い る。 　記 号 的 実 行に 関 する研 究は

，

1970 年代の 前 半か ら盛 んに な り，

一

_{時はい ろい ろ な研 究 機 関で研 究され}

_，King

に よる PL ！1 サ ブセ ッ ト の記 号 的 実行シ ス テ ム で あ る

EFFIGYI

°） や

，

　

Howden

が_{提 唱}し_た FORTRAN _用の DISSECT1 ）_{な ど が発表されて きて い る} 。 し か し

，

記 号 的実 行が本 質的に持っ て い る と 思わ れる有効性に比ぺ て

，

_{実 用 化}は進んでい ない

。

こ の原 因は

，

まず第 1に記 号 的 実 行シス テム が

，

その原 理故に ， 莫 大な計 算機 資 源 を 浪 費 する割に は

，

_{威 力}を発 揮する プロ _{グ ラ} ムの_種類 が 非 常に限 られて い る こと， 第 2に発表さ れ てい る記 号 的

相 模工業 大 学紀要　 第 19 巻　 第 1 号 実 行シ ス テムの殆 どが， 実際に は存在 し ない ， ま た は使 うに_値しない プ卩 _グラ ミ ン グ言 語 を対象に した り

，

お よ そ実現 が 不 可能な 程の大規 模なシ ス テム を目指すなど， その _{概 念}設計に こだ わ りす ぎて _， 実 用 性を欠い て い るこ とが挙げられる。 しか し

，

我々は記 号 的 実行も

，

そ れを 活か すよ う な工夫 さ え してやれ ば， それ を 応 用 して十 分 実用 的 なシ ス テ ム_{を 作 り得}る と考 えてい _る。 ま た， 最 近 で は

，

記 号 的 実 行の 中 核 を な す 記 号 処 理 を 行 な う環 境が 急 速に整 備さ れ

，

加 えて記 号 的 実 行に お い て人工 知能的 な戦 略を行な う部 分の記述も，

PROLOG

などの言語の

一

_{般 化に よ} っ て非常に容易に なっ て きてい る。 今回試作 し た シ ス テ ム は _， この よ うな環境の もとで前 述の よ う な 記 号 的実 行シス テムの欠点を緩 和する目的で _作成 され た もの である。 　

一

方

，

テ ス ト

，

デバ _ッ グ は依 然とし て

，

プ ロ _グラ ム_作 成 過 程に おい て大 きな割 合 を 占め て い る

。

すで に発 表さ れてい る多くの テス ト技法の中で， プ卩 グ ラム の実行 経 路の_{解 析技 法，} 即 ちあるテ ス ト入 力 デ

ー

タに よっ て どの よう な経路が実 行され， どの ような 出 力 デ

ー

タが得られ るか _， ま た どの よ う な経 路 が 未実行で ある か を調べ _るこ と は， 系統的で， 高い 信 頼 性を持つ 技 法 と して大 変有用 で あること が 分かっ てい る_。 本 シ ス テム で は

，

記 号 的 実 行の適 用 をプ P グラムの デバ ッ グに限定するこ と に よっ て

，

手 軽なデバ _ヅ グ

・

ツ

ー

ル と して_， 記号的 実 行シ ス テ ム を用い る こ とを 試み る。 ま た こ の こ と が， 前 述の 記号 的 実 行シ ス テ ム の短 所の解 消に なると考え られ る。 　 今回 試 作 したシ ス テ ム _は

，ユー

ザ が_， プ ロ グラム ま た は手 続き中の 任 意の ステ

ー

トメ ン トと変 数 を示すこ とに よっ て， プ P グラム または手 続 ぎの最初か ら その ス テ

ー

トメ ン トまで を 記 号的に実 行 し

，

指 定された

一

つ また は 複 数の変 数の 記 号 的 な値

，

お よ びそこに 至 るパ ス をユ

ー

ザに返 す もの である

。

こ の シス テムは

，

プPtグラム の_単 体テス ト の段 階で 主に使用するもの で_， プP グラム の制 御構造の誤 りの発 見や， パ ス の分 岐を決定する複数の変 数の

，

境 界 値 付 近で の_振舞い の分析に_特に_有効で ある。 　また， 本シ ス テム の成果を正確に評価し， 実用 化 する た め に， 本シ ス テ ム に使 用で きる言 語は

，

実在の プロ グ ラ ミン グ_{言 語 （}PL _！1_）に きわめ て 近い もの に設 定し て い る

。

表 1 ダイ ナミ ッ ク

・

デバ ッ ギ ン ク  シ ス テ ム と 記 　 　 　 号的実 行シス テ ム と の比較 ダイ ナ ミ ッ ク ・ デバ ッ ギ ング

。

シス テ ム 記 号 的実 行シス テ ム 　 　 　 ・ _ほ と ん どの プ ロ グラム 　 　 　 　に つ い _{て 実 行が可能} 。 賄

’

鷲 騨

源 を あ ま 喉

・

_{計 算}誤差が ない 。

・

_{境 界 値}の 分 析 力 が高 い _o

・

_実行さ れ ない バ ス _を 発 見 する こ と が で き 　 る

。

2．

本シ ステ 厶 の特 微 短 所

・

_テス ト

。

デ

ー

タ を 人 問 　が推 測 に よ り生 成 す る の で， 特 殊な ケ

ー

ス で 出る バ グ を 発 見 する こ 　とが 難 い。

。

_{莫 大 な計 算 機 資源 を} 消 費 する

。

・

_ル

ー

_{プ 及 び 配列に 関} する解 析 能 力 が 弱 　 く

，

実 行 で きるプ ロ グラ ム _{が 限} ら れ る。

・

結 果が人 間に とっ て 分か りやす い もの に なる とは 限 らな い

。

表

1

に

，

従 来の記 号 的 実 行 を 使っ た プ卩 グラム のデバ ヅ グ ・ シ ス テ ム と， ダ イナ ミッ ク

・

デパ ッ ギン グ

。

シ ス テ ム4｝ との比 較 を 示 す。 　た だ し， ダ イナ ミッ ク

・

デバ ッ ギ ン グ

。

シ ス テ ム と は， プ P グラ ム に具 体 的な値を 入力し， その結 果を追 う ことに よっ てプ 卩 _{グ ラ}ム の ミ スを探 す よ う な もの を 指 す

。

　 本シ ス テ ム で は

，

表 1に示した 記 号 的 実 行シ ス テ ムの

3

つ _{の 欠 点}に対 して

，

次の ような対 策を 用い てい る。 （a） 計 算 機資 源の浪費 　本シ ス テム は， 閉じ た プ ロ グ ラム ま た は手続 き を総て 記号 的実 行する の で は な く

，

その_最初か ら， ユ

ー

ザが 指 定 し たス テ

ー

トメ ン トまで の ， 指 定し た

一

つ ま た は数 個 の変 数に つ い て し か 記 号 的 実 行 を 行 なわない。 し た がっ て_， 指定 さ れ た変 数に直接関 係 し ない パ ス や変 数を

，

予 め簡 単 なデ

ー

タ

・

フ ロ

ー

解_析を_{行 な う}こ とに よっ て排 除 するこ とに よ り

，

計 算 機資源を有効 に利用する こ とが 期 待で _きる。 　ま た

，

記号の ま ま実 行する必 要の 無い変 数につ い て は あ らか じ め その _値を初 期設定す るこ とに よ り， シ ス テム の 負担 を 軽 減 して い る。 （b） ル

ー

プ

，

配列に関する解 析 能 力の弱 さ 　ル

ー

プ は， そ れぞれの 性質につ い て 自動 的に場 合 分 け を行なうの で

，

『ル

ー

プは 必 ず 実行 し ない』シ ス テムや 『指 定回の み 回 る』 シス テム に 比べ て プロ _グラ ム の_{解 析} 能 力が高い。 ま た， 記号的実行に 際して帰納的 な 表 現 を

一 16 一

プロ グ_ラ ム

・

デバ ッ グに お ける記 号 的 実 行の応 用 （深 沢 良 彰

。

袖 山 欣大

・

門倉敏夫 ） 許したこ とも あい まっ て

，

ル

ー

プや配列に対 する解 析 能 力を上 げる効 果を持た せ てい る。 　（C） 結果の見にく さ

　

本シ ス テ ムで は， 記 号 的 実 行を行 なっ た結 果は， 字下 げ を 行 な うなど し て画面上で できるだ け 見 や すい表記方 法を とっ て い る_。 また

，

結 果の記 号の

一

部に数 値や式 を 代入 し て再び簡略化するこ と もで き

，

人間に とっ て分か り や す い 形まで結 果を簡 略化するこ と が 可 能で ある

。

3

． 本

システ厶 の

実行例

　本シ ス テム の 具体的 な実 行例を次に示 す

。

（a） ル

ー

プ が 関与しないプログ ラム

　

図 1の プ P グ ラム _{を 入力 すると}

，

本シ ス テ ム は_， まず プ ロ グ ラ ム _を最_も細か い ス テ

ー

ト メ ン ト の単 位に分 割し 見 や すい よ うに_整理 し た後

，

番 号をつ け て 画面に表 示 す る。 こ こ で

009

のス テ

ー

_{トメ ン} トまで の

K

の_{記 号 的}な値 と009 に た ど りつ くまで のパ ス を求め るこ と を指定する と

，

本シス テム は図 2の ような 出 力 を 行 なう。 この 例に お い て

，

本 シ ス テ ム は

，

記 号的 実行 を 行 な う前に デ

ー

タ フ ロ

ー

解 析を行ない _， ス テ

ー

トメ ソ 5005 _・

006

は 009 に 至 るパ ス に は 無 関係で あること を 察 知し て記号 的実行 を行なわ ない。

　

ま た

，

デ

ー

タ フ ロ

ー

解 析が最も有 効に使わ れた と 思 え OOIOO20030D4 OD50D6

007

00BDO9

010

図 1 SAHPLE1　：

PI

〜OC　　　（

1，

J，

K，

L　）　

．

　DCL　　（1

，

」

，

K

，

L

．

H　）　INTEGER 　

M ・

．

　1十」　； 　

IF

　M

＝1

　THEN 　 　 DO： 　 　 　 　K

＝

1 ＊亅／

2

　； 　 　 　 　

L ＝

・

1 ／

J

； 　 　ENI〕 ； 　 ELSE 　 　IF　M　

＝2

　

THEN

　 　DO ； 　 　 　L

宦3

　1 　 　 　

L ＝

＝

L＋

2

　； 　 　 END　； 　 ELSE 　 　 K

− 2

　1

END

　

SAMPLE1

　： 　 サ ン プ ル

・

プロ グラ ム

1

　 　 KM 　 　 　 condition 　

1

　 　 　 　 ＃i＋ ＃

j ■ 2

　 　 　

RESULT

　

1

　 　 　 　

5

　 　 　 path　

1

　 　 　 　

001−002−003−004−007−008−009

図 2 サ ンプ ル

・

プロ _グラム

1

の 実 行 結 果

ODI

　　　　　　

S

酬

PLE2

　：　

PROC

　（

A

，

1

）　　；

002

　　　　　　DCL　　A　（＊）　　　INTEGER　；

003

　　　　　　　　　DCL　　（1

，

XrJ　）　INTEGER　：

004

　　　　　　1F　I＞

1

　THEN

O

〔｝

5

　　　　　　X

■

　A　（1　）　； 　 　 　 ELSE

oo6

　 　 　 x

＝o

　；

OD

？　　　　　　

DO

　J

冨

1　toI　；

ooe

　 　 　

A

（

J

）

＝

亅　； 　 　 　 END　； 009　 　 　 1

−・

3　； 　 　 　 　

END

　

SAHPLE2

　： 　 　図

3

サ ンプル

。

プ ロ _{グ ラ}ム

2

　 　 X

＝

　 　 　 　 conditjon 　

1

　 　 　 ‡‡i＞

1

　 　 　 　 result 　

1

　 　 　 ＃a　 〔＃ t〕 　 　 　 　 path　

1

　 　 　

0

巳

1−002−003−OO4−

005

−009

　 　 　 　 condition 　

2

　 　 　 ‡‡i く

一1

　 　 　 　 resu ］t　

2

　 　 　

0

　 　 　 　 path　

2

　 　 　

001−002−

003

一

臼〔〕

4−006−

〔｝

09

図 4 サ ン プル

・

プ ロ グラム 2の 実 行 結 果 る 例 の 1つ _を次に示す。 図

3

の プ卩 グラ ム で

，

ス テ

ー

_ト メ ソ ト009 ま での

X

の値を 求め るとすると 結 果は図 4 の よ うに なるが

，

こ こで は記 号 的 実 行に とっ て最 も処 理の 複雑な

007

，

008

の ル

ー

プはX に無関係なの で シス テ ム か らは無視される。

相 模工 業大 学 紀 要　第 19 巻　第

1

号 ◎ 　　DO　I

言1

　to　100： _◎

DO

I

詈JTOKDO

END

_END

3

匚

」

富

置

IJ ◎

躍

XY

凹

▲

四

B

◎

DOK

＝ITOJ

； DO　騨HILE　（自 ＞B ）

END

_{A ＝A}

_十

_C

◎ 　1

− 1

DO騨HILE（

1

　〈

100

_）

1 ＝

・

₁

＋1 END （た だ し

，・

…

　は任 意の ステ

ー

トメ ン ト の集 合 を 表わす） 　 　 　 図 5 決定回 実 行され るル

ー

プ の例 （

b

） ル

ー

プが関与 す る プログラ ム

　

プロ グラム中に， DO や

WHILE

などの ル

ー

プが 現 れ， か つ その ル

ー

プ が必 要 として い る変数に関 与して い る ときに は， ル

ー

プを次の ように場 合わ け し て 処 理 す る。 　i） 決 定回実 行 されるル

ー

_プ

　

これは， ル

ー

プ を実 行する回 数が

，

計 算機に とっ て 明 らか である場 合で _ある。 図 5に例を挙 げる。 　こ の よ うな場 合， 本シ ス テム は 原 則 と して記 号 実 行 を ル

ー

プの 回数だ け 行な う

。

し か し

，

も しル

ー

プ の内部 が 帰納的に表わ せ る よ うな 場合には， 下 記の

ii

）に準 じ

，

◎ 　 　

DO

　

I ＝

JTOK ； 　 　 　 A　（1 ）

＝

1 ＊I 　 　 　END 　 　 　 　 END　； 図

6

有 限 回 実行 さ れ る ル

ー

プの 例 帰 納 的 表 記 を 行なう。 　 ii） 有 限回実 行されるル

ー

プ 　 これ は， 計 算 機に とっ て明 ら かに有 限回 で脱出で きる こ とは分か っ て い て も

，

その具 体 的な実行回数 がわ か ら ない ようなル

ー

プである。 図 6 に例を挙 げる。 　 こ の場合， シ ス テム は

，

まずル

ー

プを

2

回実 行し て み て_， ル

ー

_{プ中の 総ての 変数が} ， 常に

一

定の値 を 示 すか， もしくはル

ー

プ_{変 数}の関数と して表 される場合に は， そ の記 述 を行なっ て ル

ー

プか ら脱 出 する_。 図 7に ， 帰納 的 記述の例を 示す。

　

ま た

，

帰 納的 な 記述が 不可 能な場 合に は_{， 次}の

iii

）に 準ずる。 　iii） 不定回実 行さ れ るル

ー

プ

　

これは， 計 算機に とっ て （人 間に とっ て も）実 行 する 回 数が不 定で ある ようなル

ー

プ で_ある。

一

般に使われる WHILE ル

ー

プ_は こ の 例にあた る。 　シス テ ムが， こ の よ う なル

ー

プ を発見 すると

，

実 行を

一

_{時停止 し て} ， ユ

ー

ザに次の項 目の中か らの選 択を要 求 する。 こ のル

ー

_プで は

，

｛＠i ＞

皀

（変 数J の記 号 的 な 値 ） ＆＠i ＜ 昌 （変 数

K

_{の記 号 的}な_{催 ）} 　 　 　 　

la

〔＠i〕

＝

＠i ＊_＠

i

_｝ が生 成され る。　（＠はシステムが 自動 的に 生 成 し た 仮 変 数であ る。 ） 　 　 　 　図 7 ル

ー

プの 帰納的 表 現の例

一

一

プ ロ グ_ラム

・

デバ ッ グにお ける記号 的 実 行の応 用 （深 沢 良 彰

・

袖山欣 大

・

門倉 敏 夫 ） α ）ル

ー

_{プ を} ユ

ー

ザ が指 定し た回 数 だ け 記 号 実 行 す 　 　る。 β）ル

ー

プを

一

回 ごとに ス テッ プ実 行し， 結 果を画 面 　 　に表 示 する

。

γ）ル

ー

プ 変 数 な ど， ル

ー

プに関係し た値の設 定 を行 　 　ない

，

脱 出 条 件 などの手助け を行 なう。 δ） ル

ー

プ の脱出 条件 を判 断 し て い る 条件 文 を 　 　

TRUE

または

FALSE

に設定する。

4．



_{対 象 言 語}の仕 様 　本 言 語は

，

PLII 言語の サ ブt ッ トであ る が

，

　PL ！

1

で 最 も 良 く使 わ れると思われる言 語 仕 様の大 部分を有して い る。 以 下に ， こ の 言 語の

，

を述べ _る 。

PL

！

1

との主 な 相 違 点のみ 　  　デ

ー

タ の_{種 類} 　 本言語で 扱 う こ と の 可 能 な 基 本デ

ー

タ 型 は

，

INTEGER ，

　REAL _，　

CHARACTER

_，　BOOLEAN _，　PTR の 5 種類である。 この 5 種類の基 本 デ

ー

_{タ型があ れぽ}

_，

一

_{般に使わ れ る プ} ロ グラ ム の 殆 ど は， こ の 制 約に よる大 き な障 害は生 じない と思わ れ る。 ま た

，

こ の制 約は

，

記 号 的実 行では

，

型の変換に よ っ て生 じる誤 差を 記 号的に 検 定するこ _とが非 常に困 難で ある ことに も起因 し て い る

。

　   フ ァ イ ル に対 する操 作は記 述で きない

。

た だ し

，

コ ソ ソ

ー

ル に対 する入 出 力 （PUT 　 LIST ，　 GET 　 LIST 等）は記述可能で ある。 　 配 列 変 数 が 扱え る以 上

，

フ _{ァ イ}ル _{も理 論 的}に は扱え る わ け で は あ る が

，

本シ ス テ ム _{が稼 動 する計算機 環 境} （VM 　CMS _） の制 約の た め， 今回は フ ァ イル操 作は 見送 っ _た。 　   再帰手続 き は 記 述で き ない 。 　再 帰 手 続 き も

，

理 論 的にはサ ポ

ー

ト可 能 だが ， 仮に再 帰手続 きをサ ポ

ー

トし た と して も， その プ ロ グ ラムを 記 号 的に実 行し た結 果は

，

ほとん どの ものが非 常に繁 雑に な り

，

人 間に とっ て デバ ッ グに役 立つ ほ ど有 用なデ

ー

タ を提供で きない と判 断し た

。

　   並 列 実 行に関 する操 作は記 述で き ない。 　本シ ス テ ム の よ う な記号的実 行の ア ブ Pt・

一

チ で は

，

並 列実 行をサ ポ

ー

ト_するこ とは不可能で ある。 　   　ポ インタ は

，NULL

もしくは具 体 的 な 変 数 名 を 指 す もの とする。 従っ て _， ポ イ ソ タ変 数に数値を代入 し た り， ADDR 関数を使 うこ とは許され ない。 　ポ インタ変 数は

，

実 際に は ア ドレ ス が格 納さ れて い る が， 概 念 的には ポ イ ン タ変数は具体的 な 変 数 名 を指すべ きであ り， 上 記の ような制約条件を課し た とこ ろ で， プ ロ グラム に とっ て大 き な 障 害は無い と判 断し た

。

5． 本

シ ス テ ム の

構成

　本シ ス テ ム は，

IBM

の VM 　

CMS

環 境の端末上 で， ユ

ー

ザ_{と対 話 形 式}で実 行されるもの である

。

シ ス テ ムは 図8 に示すよ うに_， 大 きく分けて Pre　Processor

，

　User

Interface

　

Handler，

　

Data

　

Flow

　

Analyzer，

　

Symbolic

Executer ，　

Symbolic

　Evaluater

，

　Editor の

6

つ の部 分

か ら構成 されてい る。 　 以 下にそれ ぞれ の機 能を説 明 する

。

（a_）Pre　Processor 　Pre　Pr  essor は，　 PLfl 言 語の ソ

ー

ス を， 対 象 言 語 の仕 様に_適合 するよ うに 変 更 するもの で ある

。

　 本シ ステ ム の ユ

ー

ザ

・

イン タ フ ェ

ー

ス は ， あ く まで PLII _{を 仮 定 し}て い る

。 一

方

，

処 理の 都 合上

，

本シ ス テ ム は前節で述べ _{た ような 仕 様を持}つ_{言 語}を対 象とするの で こ の 言 語 間の 変 換を行 な うの が Pre　Processor で あ る

。

　Pre　Processor は_{， 大 き}く_分け て_次の 3つ の機 能を持 つ o 　 i） 文 字列の_置換 　 これは

，

主に対 象 言 語の扱 える デ

ー

タ型が

，PL ，

il_に 比較し て_劣っ て い る部分を補う ため _， および短縮形 など を使 うこ とに よ り， 2 種類 以 上の表 記方法を許 すシ ン ボ ル _を

一

_{種 類}に統

一

する た め に使 う。 　 ii） 適 合しない文 法 を含む ソ

ー

ス

・

_ブ卩 グ ラム _の排除 　iii）ソ

ー

ス

・

プ ロ _グラム _{を最 も細}か い単 位の ス テ

ー

ト メ ン ト に分 割し

，

それに番号をつ _けて整 列 化 する機能。

（b）　

User

　

Interface

　Handler

　 User　Interface　Handler をよ_，　 Pre　Processor _{で整 列} 化された プ卩 グラ ム _{に 対し}て _， 求め るス テ

ー

トメ ソ ト や 変数の指示

_，

その他 初 期 設定を 行 な う もの である。 具 体 的に は

，

次の ような もの に対して設 定を行なう。 　 i） 求めるス テ

ー

トメ ン ト の指 示 　 　 　求め るス テ

ー

トメ ン トは，

Pre

　Processor でつ け 　 　 　 られたス テ

ー

トメ ソ ト番号で指定 する。 　 ii） 求め る変数の _指示

相模工 業 大 学紀要



第

19

巻

　

第

1

号 　 　 　 ＝ ＝⇒被テ ス トプログ ラム の流 れ 　 　 　

一

→ デ

ー

_{タ の流}れ 図

8

　システム_図

　　　

これは， 複 数で も構わない。 また

，

配 列 変 数は， 　 　 　ま と め て

一

つ の _変数と して扱 う

。

iii_{） 変 数}の初期 設定

　　　

設 定値は具体 的な値でも

，

記 号 を使っ た式ま たは 　 　 　 条件で も 良い。

iv

） プロ _グラム_中に含まれる他の手続 きの呼び出しの 　 　 　 扱い を決め る

。

　　

ア） プロ グ ラム 中に呼び出 す 手 続 き を挿入 する。

　　

イ ）手 続きの動 作 を 記 号 的に記 述 する。 　 　ウ ）手 続 き 呼び出しに よっ て影 響を受 ける変数を 指 　 　 　 　 定 する

。

（c ＞　

Data

　

Flow

　

Analyzer

　Data

　Flow 　Analyzer _は

，　

Pre

　

Processor

か ら出 力さ

れた プロ _グラ ム と

， User

　

Interface

　

Handler

か らの諸

情報 を も とにデ

ー

タ フ ロ

ー

_{解析を行なっ て記 号 的実行 を} 行 な うべ _きス テ

ー

トメ ソ トと変数 を 探 し て

SymbOlic

Executer

に_渡す 機 能 をもつ

。

　なお， こ こ で行な うデ

ー

タ フ m

一

解 析は ， ス テ

ー

トメ ソ ト間の変数の参照情報を主 な 判 断 材 料に して お り， 比 較的 初 歩 的 な もの で ある。 ま た， 配列 変数は， ま と め て

一

_{つ の変 数 と 判 断して い る} 。 以 下に デ

ー

タ フ 卩

一

解 析の アル ゴ リ ズ ムを 示 す

。

　

Pre

　

Processor

で番 号 付 けされたタ

ー

ゲ ッ ト

・

プ ロ グ ラム の ス テ

ー

ト メン ト番 号を

1

〜 n と し ， プロ グ ラム 中 の ある X テ

ー

トメ ン ト k （1≦k≦n_）で， 定 義される 変 数の集 合 を

DEFV

（

k

）とす る

。

ま た， ス テ

ー

トメ ン ト k で _{， 参}照 さ れ る変 数の_集合お よ び_， そ こか ら前に遡っ て_{最 初}に現 れ た 分 岐ス テ

ー

トメ ン ト （

IF

，　

WHILE

等 ） で参 照 さ れる変 数の 集合を REFV （

k

） とし

，

プ ロ _{グ ラ} ム _中の ス テ

ー

トメ ン _ト

k

_{ま で で} ， 求める 変 数の集合 を

V

とす ると

Data

　

Flow

　

Analyzer

か ら出 力さ れ る， 必要

な ス テ

ー

トメ ソ ト の 集 合

STR

（

k

，　

V

＞は， 次の よ うに 表 わ される。 　STR （O，　

V

）

＝

φ   傷 胆

［

：

_{鰌 飄}

。 、 　 　 　 （if　DEFV _（k_）∩

V

≠φ〉 （d）　SymbOlic 　

Executer

　SymbOlic

　Executer は

，

　

User

　

Interface

　Handler _お

よび

Data

　Flow 　

Analyzer

か らの_情報 を も とに

Pre

プロ _{グ ラ}ム

・

デバ ッ グに お ける記 号 的 実 行の応 用 （深 沢 良 彰

・

袖山欣 大

・

門倉敏夫） Processor か ら出力された プロ グラム の_{記号的 実行}を行 なう

。

ル

ー

プの 実行に関し て会 話 的に実 行 を 行 な う必 要 が生じ た ときは， Editor を呼び出し

，

また

，

式 を 簡 略 化 するため に常 時

Symbolic

　

Evaluater

_{を 呼 び 出 す こと} がで きる

。

　 記号的 実行に際し て， プ ロ グラム中に現れる 変数は 次 の よ うに して処 理する。 　 i） 手 続 き

『

に_渡さ れ る引 数 　 これは ＃記 号に続い て変 数 名の小 文 字で表 わ す

。

た と えば

，

　

AAA

：

PROC

（

ABC ，

　

XYZ

_）；

とい うプ P グラム が_あっ _{た と}す_ると

，

変 数

ABC

の初 期

値は，

User

　

Interiace

　

Handler

で特別な指 定の 無い 限

り

，

＃abc に

，

変 数

XYZ

は _＃xyz にな る

。

　

ii

） 通常の_{変 数} 　これは プロ グ ラム 中の条件に よっ て， 複数の値 を持つ こ とがあるの で _{， 次}の よ うに表 わ さ れる。 　変 数 名

＝

条 件

1

値， 条 件

1

値

，…

， 条件

1

値 た だ し

，

条 件

，

値とも 原則と して i）の引 数か

，

もしく は次の iii）で 述べ _る読み込み 変 数の式で表わ され る。

　iii） GET 　LIST _等でシス テ ム _{に読み こ まれる変 数}

　た とえば，

GET

　

LIST

文がル

ー

プの中にある場合な ど では ， 変 数が 何 回読みこ まれる か不 確定である。 しか し， こ の 変 数 を参照する変 数にとっ て は， 自分の扱っ て い る デ

ー

タが， 何回め に 読み込ま れ た 変数であるか を 把 握 する必 要があるの で_， 入 力 文に よっ て読み込まれた変 数は次の よ うな形 式を とっ てい る

。

　 変 数 名

＝

（読 み 込 まれた回 数 ） 変 数 名の小 文 字 た とえば

，3

回め に読み込 ま れた変 数

ABC

の値は

，

　 （3）abc と な る。 た だ し， 読みこまれた 回数は， 通常 ii） と同 じ く

，

複数の条件 と値の組み合わせ で ある。 　 iv） 動的変 数 　動的変 数 も， プロ グ ラ ムに よっ ては実 際の 変 数 として 記 憶 域に割 付 られる数が変 化 する の で

，

上記の iii） と似 た扱いを する

。

　 変数 名＝ ［_記憶 域_に割 付_{け ら れ た}順番

1

変 数 名_の小文 字 　た だ し

，

こ の ［記 憶 域に割付け られた 順番］も， 原 則 として

ii

） とおな じ形 式 を とっ て い る

。

動 的変数の表記 の具体例を次に _{挙 げ}る。

OOI

　SAトlPLE3

2300nUO

 

0400500E

臼

0700

臼

009UIO

臼

llD12D13

014015

　 　PROC　（TOP　）　；

DCL

　　（TOP

躓

P　）　　　　

PTR

　： DCLl　CハRD　　　　　　BASED

，

　 　 　

2

　NAME　　　　CHARACTER

，

　 　 　

2

　NEXT　　　　PTR　； DCL（

1，

NUMBER）　　　工NTEGER　： DCL　　NULL　　　　　　　BUILTIN　；

GET

LIST

　（

NU

卜｛BER）　；　　　　　　　／＊

IF　NU卜IBER

＝

OTHEN_／＊ 　↑GP ・

・

　NULL_{：　 　 　 　 ／＊} ELSEDO 　

I＝1

　TO　NUMBER カ

ー

ドの枚 数の読み込み　＊／ もし カ

ー

ドが なければ ＊_／

TOP

はNULLIUする　 　 　 ＊／

　　　

ALLOCATE　CARD　SET

　

_（P _{） ；}

　

_／＊



_{構 造 体}CARD_{を割り付 ける}



_＊／

　　　

GET 廴IST （cnRD

．

NAME ） ；



／＊



カ

ー

ドの内 容の護み込み

　

＊_／

　　　

IF　I

＝

1　

THEN　　　　　　　

／＊

　

_{も し}カ

ー

ドが1 枚め だ ？ た ら

　

＊／

　　　

CARD

．

NEXT

＝NULL

；



／ ＊

_CARD．

NEXT _はNULUc _する



＊_／ 　 　 　ELSE

　　　

CARD

．

NEXT

＝

TOP ：



／＊



さ も なくばチ ェ インする

　

＊／

　　 TOP

＝

P ；

　　　　　　　　

／＊

　

TOP をカ

ー

ド の先頭の ポ イン タlt　＊／

　 　

END

　l ENDsnMPLE3：

相模工 業大学紀 要　第

19

巻　第

1

号 　［

i

＜

j

十

11k

十

1，

　

i

＞＝

jH

−

11k

− 1

】abc 　これ ら

i

）

〜iv

）の表 記法を 用い るこ とに よっ て ， 本シ ス テ ム で は， 配 列や ポ イン タ をサ ボ

ー

トして い る。 　たと えば

，

図 9の手 続 きに おい て， 手 続 き終 了 時の ポ イン タ 変 数

TOP

の値を求め るこ と を 考え る

。

こ の手 続 きは， 入力装置か ら， カ

ー

ドを読み込み， そ れ を リス ト に し て先頭の ポ イン タ変数 TOP を返 すもの である。 た だ し， リス トの 末尾は

NULL

になっ て い る。 また ， カ

ー

_{ドの枚数は手続きの最初で読み込み} ， 枚数が

0

の とき に は

TOP

に

NULL

が代入 されるもの と なっ て い る。 　こ の プ ロ グラ ム を記 号 的に実 行 して_， ポイγ タ_{変 数} TOP の_値を求め る過 程を図 10 に示 す。 （e）　Editor 　Editor は， 人 間が理 解で き る形の式と， シ ス テム の   　ステ

ー

トメ ン ト　

002

「

vOO5 _{を実 行}し

，

変 数のテ

ー

ブル _{を 作 る}。   ステ

ー

トメ ン ト

DO6

を 実 行 す る と

，

変数NUMBERは 次のように なる

。

　bRJMBERi

＝

　（1　）　nunt）er

  ステ

ー

トメン ト　

OOT

〜

ooe

を実 行 す_ると

．

ポ_インタ変 数

TOP

は次のよ うにな る。

　

TOP

　

旨

　　　（

1

　）　mumber

＝

＝

O

　

lnull

  　ス テ

ー

トメ ン ト　

OO9

〜

015

はル

ー

プ なの で

，

　

Symbolic

　

Executer

は

，

ル

ー

プの性 質 を

調べ _る

。 そ の結 果， 有 限 回ル

ー

プであ ること が わ か るの で

，

変 数

P

，

CARD

，　

TOP

に対 して

，

次のよ う な 中 闇 結 果 を 作 成 す る

．

　P　

，

　｛＠li　＞

星1

　＆　　＠i　＜

国

　（1　）　number 　

l

　P→ _〔  i_〕card_｝

　TOP

＝

｛＠i ＞ 窗

1

＆　 ＠ i〈 ＝ _（

1

_）number 　

l

　TOP

−

→ _〔＠i_〕card ｝

　cnRD

．

NEXT

＝

｛＠i ＞

旨1

＆　 ＠i 〈

零

（

1

）number ＆　＠i

＝1

　 　 　

1

　〔＠

i

　〕　

CARD．

NEXT

　

−

→

NULL

　　　　　　

1

　 　 　 ＠i ＞

＝

1 ＆　 ＠i〈

豊

（1 ）number 　＆　 ＠1 ≠1 　 　 　

1

〔＠i〕

CARD．

NEXT

→ _〔＠卜

1

_〕

CARD

_｝

c

“

RD．

NA

岡

E 望

｛＠

i

＞

零1

＆　 ＠

i

〈

＝

（

D

　riumber_＆　＠

i 罨1

　 　 　

1

　 〔＠i　〕　CARD

．

NAHE　

＝

　（  i　）　card

．

na用e

　　　　　　　 「

　 　 　 ＠i ＞

＝1

＆　 ＠

i

〈

＝

_（

1

_）number ＆　 ＠

i

≠

1

　 　 　

1

〔＠i〕cnRD

．

NAME

＝

＝

（  i）card

．

name ）

  　よ フ て

，

  と   か ら手 続き終了時のTOP は次の ようになる。 　TOP → 　 　condition 　

1

　 　 　 （

1

　）　numbe 「

＝

工 　 　result 　

l

　 　 NULL 　 　path　

l

　 　 　

OOI−DO2−O

〔

13−O

〔｝

4−005−006−

〔｝

07−OD8

　 　 cendition 　2 　 　 　 （

1

　）　number ≠

1

　 　resu 】t　

1

　 　 　 〔　（

i

）　number 〕　oard 　 　path2 　 　 　001

呻

002

−

003

−

004

−

005

−

006

−

007

−

0臼9

−

OlO

−

011

−

012

−

013

−

Ol4

−

〔｝15 　 　 　 　　 　 　　図 10 ナ ンプ ル ・プ ロ _グラム

3

の 記 号実 行過程

一

一

プ ロ グ_ラム

・

デバ ッ グに お ける記 号 的 実行の応 用 （深 沢 良彰

・

袖山欣大 ・ 門倉敏 夫 ） 内 部 表 現と して の 式の相 互 変 換 を 行 な うもの で ある

。

ま た式 が 画 面の 1 行よ りも長 くな っ た場合に は， 字下 げを 行なっ て式を見 易くする操 作 も行な う

。

（f）　

Symbolic

　

Evaluater

　 Symbolic 　Evaluater _は

，

_{数 式}

，

_論理式の_簡略 化お よ び簡 単 な 定理の 証明 を 行な うものである。 「式 」を簡 略 化 する基 準は

，

用 途に よっ て多 岐にわ た る が

，

こ こ で は 結 果 が 『人 間に とっ て』わ か り やすい ものに帰着させ る こ と を 基 準 とし た

．

　

Symbolic

　

Evaluater

_{の機 能 を 次}に示 す

。

　 i） 単純式の簡 略 化 　 　 ｛列：

3

十a十

b

十a十

1

十a 匸＞　a＊

3

_十

b

_十

4

　 ii）　ド・ モ ル ガ ンの定理 な ど を 用 い た 条件 式の簡略化 　 　 ｛列：一 　（a＞ 3）　⇒　　a≦3 　 　 　 　

−

「 _（a ＞3 ＆ b＜5）匚_{＞ a}≦31b ≧5 　 m ） 知 識ベ

ー

ス を用いた条件 式の簡 略_化 　 　 例： a＞

3

＆ a ＞

5

⇒ a ＞

5

　 　 　 　a

＝

a ⇒ 　　true

　

Symbol

董c　

Evaluater

は， 内部に

PROLOG

イン タプ

リタ を持っ て お り， 上例の iii）などの よ うに ， 公理系か

らの マ

ッ チ ン グに よっ て式の簡略化 を 行 な う際に は

PROLOG の持つ _{推 論 機 能}を利 用 す る こ と が で きる。

　

Symbolic

　

Evaluater

に PROLOG イン タプ リタ_{を 利} 用し た 理 由は次の とお りで ある。

　i

） 論理 や事実を 記 述 する だけで

，

シス テ ム がある_程 度 推 論し， 処 理 して くれる。 し たが っ て ， 手 続 き的プ ロ グ ラ ミ ソ グ は最 小 限度で す む。 　

ii

） PROLOG の プ ロ _グラ ム は デ

ー

タ ・ フ ァ イル に置 か れ た規則の_集合である。 従っ て， 公理系の追加や変更 など

，

細か い仕 様 変 更 が 容易であ る

。

　図 11 に

，

PROLOG の プ ロ グ ラ ム と して _書かれた _， 論理式に_関する公 理の

一

_部を 示 す

。

　こ こで _{， 次}の よ う な式を簡 略 化 する こ と を考える。 　a十b＊

O− 3

＞

−

c ＆ a十c ＞

0

上の式を

Symbolic

　

Evaluater

に かけ る と

，

次の よ う な 手 順で簡 略 化を行 な う eva　

1

（and ，　tr．　X，　X ）

．

eval （andg 

fag



X，



fa

_）

．

eva1 （or

，

_tr

，

》〔，tr）　

．

eval （equal g　

X

，　

X豊

　tr） 「_{真とX 　（X は 式で も何で も良い）のand はX で あ}

₆₁

「_偽とX の and は 偽で あ る」 「_{真とX の or は 真で あ る} 」 「

x

_と

X

_{が等 しけ れ ば}

_，

_真で ある」 eval （ptus

，

　A

，

　O ，　A ）

．

　 「A に

0

を足 し た もの はA で あ る」 eva1 （times

，

A

，

0，0

）

．

　 「

A

_に

O

_{を かけた もの は}

0

_{で あ る1}

eva且　（plus ，　A

，

　ne8 　（B　）　

．

C）　：

−

eval 　　（minus

，

　A

，

B

，

C）　

．

　 　 　 　「A に

一

Bを 足すと 言 うことは

，

A

−

B と 同 じで あ る」

eva1　（and ，　

OP1

騨　Op2　g　Rs　）　：

−

　 　 　 　Op1　

＝．

．

　〔greater

，

P1

，

P2　〕　

，

　 　 　 　OP2　

置．．

　〔greeter，

P1

、

P3

　）　， 　 　 　 　prove 　 （P1

，

Nl　）　

，

　 　 　 　8r　（P2

，

P3

，

1〜　）　

、

　 　 　 　prove　 （R

，

U　）　

，

　 　 　 　Rs

＝．

．

　〔8reater

，

回

1

，し」〕　

．

　 　 　「_もし

，

_{＆演 算 子の両} 側の式が

，

P1

＞

P2

，　

P1

＞

P3

の パ タ

ー

ンな ら

，

結果 は

，

ま ずP1 　 　 　 　の式 を 簡 略 化 し た もの （町 ） と

，

P2

と

P3

の う ち

，

大 きい もの を とっ て

，

さらに そ 　 　 　　れを簡 略 化 し た も の （日）に よフ て

，

Wl＞闇 と 表 わ せ る。 」 図

11PROLOG

プロ グラ ム の 形 で書かれ た 公 理の

一

部 （ただ し， 『 』 内は注釈文である）

相 模工業大学 紀要　第

19

巻　第 1 号   a ＋

b

＊

O− 3

＞

−

c の式を

，

不 等 号 よ り左に 記 号を

，

　 右に数 値を集め， 数 値が演 算 可 能 な と きには， その演 　 算を行な う

。

こ の ことで

，

a＋

b

＊O

−

3＞

−

c は a＋

b

＊ 　 0十 c＞3 に変 形される_。   a＋b＊0_{＋ c の式 を 解 析 し}

，

_「何か IL　

O

_{をか けた もの} 　は

0

で_ある』とい う公 理か ら

b

＊

0

_は 0に な る

。

  a＋0＋c の_式を解 析し，

r

何かに 0を たし たもの は

，

　

その

0

を省くこ とが できる』 とい う公 理に よ り， a＋

0

　 十C は a十C に _なる。   ＆ オペ レ

ー

タ の 両 側が

，

不 等 号 をはさんで

，

同 じ 　 よ うな形を して いるこ と か ら

，

この 2つ の式の簡 略化 　 を試み る

。

  　ど ちら も左 辺が a ＋ c であるこ と か ら， 　 『式

1

＞数 値

1

＆ 式

1

＞数 値

2

は

，

式

1

＞

MAX

（数 　 値

1

， 数値

2

）』とい う 公 理 を適用し て， 3 と0を比 　 較し，

3

の ほ うが

0

よ り大きい の で， a＋e ＞3 ＆ a ＋ c 　＞

0

は， a＋c＞

3

に簡略化で きる。

6

．

本シス テムの評 価 表 2 本シ ス テ ム の _{評 価} D

．

D

．

S　_DISSECT 本シ ス 　 　 　 テ ム 完全 にエ _ラ

ー

_{が 発見で きる} もの 発 見できる場 合が ある もの 発見 できない もの 19_％19_％

28

％ 71_％38_％47_％ 10％　　　　43％　　　　

25

％ （た だ し， DD

．

S

とは， ダイナ ミッ ク

・

デバ ッ ギ ン グ

。

シス テ ム の略で あ る_。｝ 表

3

　エ _ラ

ー

。チ _{ェ ッ ク リ}ス ト に対する本シ ス テ ム 　 　 　の評 価 　 　 　 発 見で　 場 合に　 発見で 件 　 数 　 　 　 　 きる　 　 よる　 　 き ない 　本シ ス テムは

，

従 来の ダ イナ ミヅ ク

・

デバ ッ グ・ シ ス テ ムに_比べ ， 浮 動小数 点演 算に おける誤 差に よるバ グ を 除い て は， 高い エ ラ

ー

発 見能 力を持つ 。 ま た， 従 来の記 号的実 行シ ス テム に 比べ て も， 前 述の 特徴か ら， エ ラ

ー

の発 見 能力は高い。 表

2

に， ダ イ ナ ミッ ク

・

デバ ッ グ

・

シ ス テ ム お よび代 表的な記 号 的実 行シ ス テム の

一

つ であ る DISSECT シ ス テ ム1）との， エ ラ

ー

発見 能 力の 比較を 示 す。 なお， 『プ ロ グ ラム書法 1）_』 ， 第6 章の 『よ くある ま ちがい』 を 評価対象と した。 　表か _{ら も分}か るよ うに_， こ こ で は ダ イナ ミッ ク

・

デバ ッ ギン グ

・

シ ス テム に お い てエ ラ

ー

が発 見できる場 合が ある ものが他に比べ て非常に多 くなっ て い るが， これ は テス ト・ デ

ー

タを作成 する人 間の能 力に依存する部 分が 多 く

，

これ 自体で ダ イナ ミッ ク

・

デバ ッ ギング ・ シ ス テ ム がエ _ラ

ー

_{検 出 能 力に優 れ}てい る と は言 うこと がで _きな い と考えられる。 　ま た， 『プ ロ グラ ム テス トの技 法 3）_』 ， 第

3

章の 『検 査 のため のエ _ラ

ー ・

_{チ ェ} ヅ ク リス ト』に対 する本シ ス テ ム の 評 価 を 表

3

に示 す。 文 献 3）_中で

_，

_{人 手で行なわ な けれ} ぽ な らない と さ れて い る 67 件の チ ェ ッ ク項目に対 し て 本シ ステムで は

，

この うちの約

55

パ

ー

セ ン トを 自動 的 に検 出で きる。 ま た

，

発 見 出 来 ない 12 件の項 目中の 8 件は入 力 ／出 力に関 するものであり， これは 本シス テム デ

ー

タ 参 照 デ

ー

タ 宣 言 計　 　 　算 比　 　 　 較 制 御 流 れ イ ンタフ ェ

ー

ス 入力 ／ 出 力 他の チ

ェ

ヅ ク 16088185 1 　 　

1

　 　 　 　 1 76472902 30406203 10210080 計

67

37 18

12

がサ ポ

ー

トして い ない_{機 能}で ある

。

7．

今

後

の課 題 　 最後に， 本シ ス テ ムの 今後の課題につ い て以 下に述べ る。   現 在

，

本シ ス テ ム は

，

独 立し たデバ _{ッ グ}

・

シ ス テ ム 　 と して イン プ リメン トを行 なっ てお り

，

完 成 時に は， 　 初心者の

PL

／

1

プロ グラ ミ ソ グ実 習に活用で きる程 度 　の成 果 を 目指し ている。 また

，

将 来 的に は本 シ ス テ ム 　を

，

総合 的 な デバ _ッ グ_{環 境}の

一

_部と して位 置づけて既

　

存の デバ ッ グ

・

ツ

ー

ル と結合さ せ， 全体をマ ネ

ー

ジ メ 　ン ト

・

プロ _{グ ラ}ムが管理 し て， 最 も記 号的 実行が効 果 　を発 揮 すると思え る ような 場 合にのみ

，

本シ ス テ ム _を

　

実 行 する ように し

，

本シ ス テ ムの有用 性を高め る こ と 　も考え てい る。   本シ ス テム に おい て_， 従 来の記 号 的 実 行 シ ス テ ムに 　おける方 法 と く らべ て

，

さほ ど改善の跡 が見られ ない 　『不 定 回ル

ー

プ』に関し て， 知 識工学に基づいた 手 法 　に よ り， 解 決で きる部 分 も あるもの と思われる の で

，

　 将 来的に本シ ス テムを拡 張し て行 く方 針で ある。 24

一

プ ロ グラム ・ デバ ッ グにお け る記 号 的 実 行の応 用 （深 沢 良 彰

・

袖山欣 大

・

門 倉 敏 夫） ）

1

） 2 ｝

3

） 4 ） 5 ） 6 参 考 文 献

W ．E ．

　

Howden

_：

“

Symbolic

　Testing　and 　the

DISSECT

　

Symbolic

　

Evaluation

　

Syste

_叫 ，，　IEEE

Trans

．

　 Software 　Eng

．

，

　 SE

−

3

，

　

July

　 1977_，　 p

，

266−278．

B

．

W

．

　Kernighan 　and 　P

．

J．

　Plauger

，

木 村泉訳： 「プ ロ グラム書法」第

2

版， 共 立出版

．

G ．J．

　Myers _著

，

_{長 尾　 真}

， 松 尾正信 訳： 「ソ フ

トウ

ェ

ア

・

テ ス トの 技法」， 近 代 科 学 社， p

．

27−

36．

R

．

M ，

　

Balzer

_： “EXDAMS

−Extendable

　

Debugg −

ing

　and 　

Monitoring

　

System ”，

　 AFIPS 　

Conf．

Pr 

．

_，34_， 1969

，

　

p ．

567

−580．

S．L ．

　

Hantler

　_and 　

J．

　C

．

　King ：　“An　

Introduc・

tion　to　Proving 　the　

Correctness

　of　

Programs

，，

，

CACM ，8，

　

No ．3

_，　Sept

．

1976．

R

．

B

．

　

Dannenberg

　and 　G

．

W

．

　Ernst ： “Formal

Program 　Verification　Using 　SymbOlic 　Execu

−

tion”

，　IEEE 　Trans

．

　

Software

　

Eng ．

，

　SE

−

₈

_，

_No

_．

1

，

1982

．

7

） D

．

LGood ，　R

．

　

L 。

　

London

　and 　

W ．

W ．

　

Bledsoe

：

　　　“

An

　

Interactive

　

Program

　

Veri

_員cation 　

System ”

，

　　　IEEE 　

Trans ．

　

Software

　

Eng ．

，SE

・

1，　No

．

1，1975

．

8_）

A ．

J．

　Blikle：　

“

On 　the　Development 　of　Correct

　　　Specified　Programs

”

，

　IEEE 　Trans

．

　

Software

　　　

Eng ．

，

　

SE −7，

　

No ．5，

1981

，　p

．

519

−

527

．

9） M

．

H

．

　van 　Emden ： “

Programming

　with 　

Veri−

　　　fication　 Conditions

”

，

　 IEEE Trans

，

　

Software

　　　

Eng ．

，

　

SE −

5

，

　

No ．2，1979

_，　p

．

148

−

159

．

10）　

J．

C ．

　

King

：　“

Symbolic

　

Execution

　and 　

Program

　　　

Testing

”

，　CACM

，

19

，

　No

．

7

，

　

July

　

1976，

　p

．

　　 　

385−394．

11_{）　 R}

．

E

．

　

Fairley

：　

“

An 　Experimental 　

Program

　　　

Testing

　

Facility

，

，

，

　IEEE 　Trans

．

　on　

Software

　　　

Eng ．

，

　

SE ・

1，

　

No ．

4_， 1975_，　p

．

350

−

357

．

12）

J．

LWoods ： “

Path

　

Selection

　for　 Symbolic 　　　Execution 　

Systems

”

，

　

UMI

　

RESEARCH

　PRESS

，

　　　

Computer

　

Science

　

System

　Programming

，

　

No ．

　　 　12

．

13＞ 玉井 哲雄， 福永光

一

： 「記 号 実 行 シス テ ム」

，

情 報