• 検索結果がありません。

陰関数定義に関する考察

ドキュメント内 九州大学学術情報リポジトリ (ページ 62-65)

第 4 章 仕様と設計を分離する実行可能仕様の設計・構成法の提案 45

4.1.3 陰関数定義に関する考察

52 第 4 章 仕様と設計を分離する実行可能仕様の設計・構成法の提案

以降の各節では, 図4.2と図4.3と図4.4に示した記述スタイルをVDM++を用いて記 述する場合の設計・構成法ついて議論する. まず,図4.3で示した宣言的な記述に対応す る設計・構成法として, 陰関数定義について考察し, 次に, 図4.2で示した操作的な記述 に対応する設計・構成法として, 陽関数定義について考察する. 最後に,本研究において 提案する図4.4の記述スタイルに対応する設計・構成法として,拡張陽関数定義について 考察する. 図4.5は, これらの関数定義と記述スタイルの関係を模式的に表したものであ る. 図は, 最上段に図4.2と図4.3と図4.4に示した記述スタイル名を示した. 次の段に, 各記述スタイルに対応する VDM++ の言語仕様に示された関数定義名を示した. その 下に,仕様アニメーションによる動作検証において, 評価者が入力として用意するテスト データを示した. 次に, その入力データについて, 仕様伝達部と非伝達部におけるデータ の流れを示して, 出力をその次の段に示した. ここでは, 図4.1 と同様に「伝えること」

を目的とした仕様伝達部をグレーで塗りつぶしている. そして次の段に,この出力が正し いことを確認するために, 期待値として用意するテストデータを示した. 最後の行に, 記 述スタイルの考察をまとめた. この図を用いて, 4.1.1節と本節において分析した,「実行 可能性性の影響」の課題と,実行するために必要な評価者の作業工数について, VDM++

の関数定義から議論する.

4.1. 「実行可能性の影響」を解決する仕様記述スタイルの提案と考察 53

図4.5 仕様記述スタイル

件であり, postexpr は関数 f 実行後に成立すべき条件を定義した事後条件である. 事後

条件 postexpr の中で引数a1,...,anと戻り値resを用いて, 関数実行前後の関係を記述す る. 陰関数定義を用いて平方根を求める仕様記述の具体例を次に示す.

public sqrt (x : real) res : real pre x >= 0

post abs (res**2 - x ) <= EPS; -- EPS は許容誤差

sqrt 関数は実数型 (real) のパラメータ (x) を受け取り, 実数型 (real) の結果 (res) を返 す関数として定義している. 事前条件 (pre)では,関数実行前にはパラメータ(x)が 0以 上でなければならないことを記述している. 事後条件 (post) では, 結果 (res) を二乗し たものとパラメータ (x) の差の絶対値 (abs)が,許容誤差 (EPS) 以下でなければならな いことを記述している.

この仕様は VDMToolsのインタープリタ機能を使用して, 仕様アニメーションにより 実行することができる. 実行をするためには, 関数名に「 pre 」を付けて, pre sqrt (x) とすることで sqrt 関数の事前条件式を呼び出す. また, 関数名に「 post 」を付けて,

54 第 4 章 仕様と設計を分離する実行可能仕様の設計・構成法の提案

post sqrt (x,res) とすることで sqrt 関数の事後条件式を呼び出す. VDMTools のイン タープリタ機能を用いて事前条件と事後条件を評価するには, 以下のように行う. パラ メータ(x) を 4 とし, 結果(res) を 2 とした例を次に示す.

> print pre_sqrt(4) true

> print post_sqrt(4, 2) true

「 print 」 は 実行結果の出力を指示する VDMTools のコマンドである. 実行結果は

bool 型であり, 期待値とするテストデータは true である. 実行結果が期待値と異なり

falseであった場合は, 入力のテストデータとして用意したパラメータ (x)の値もしくは

結果 (res)の値が誤っているか,実行したpre sqrt, post sqrt の記述が誤っているかのい ずれかであるため,デバッグを行って誤りを修正する必要がある.

図4.5 (a) に, 4.1.1節において述べた宣言的な記述に対応する模式図を示す. 宣言的な

記述において, 「伝えること」を目的とした仕様伝達部は, 次に示す, 事前条件 (構文例 の preexpr)と事後条件 (構文例の postexpr) である.

pre x >= 0

post abs (res**2 - x ) <= EPS;

評価者が, 仕様アニメーションにおいて入力のテストデータとして用意するものは,入力 データであるパラメータ(x) と出力データである結果 (res) となる. 図4.5(a) の図中の

preexpr と postexpr の実行結果は bool 型である. 期待値とするテストデータは実行結

果のtrue となる.

宣言的な記述を模式的に表した図4.3 において「入力」と「入力時の内部状態」はパ ラメータ(x) に対応し,「出力」と「出力時の内部状態」は結果 (res) に対応する. つま り,テストデータとして「入力」と「入力時の内部状態」,「出力」と「出力時の内部状 態」を用意する必要があることがこの例から分かる. そのため, 4.1.1節において述べた ように, 内部状態が複雑な仕様の場合, 評価者の作業工数が課題となることがある.

九州大学大学院 システム情報科学府 情報工学専攻

4.1. 「実行可能性の影響」を解決する仕様記述スタイルの提案と考察 55

陰関数定義を用いることで,入出力の関係を宣言的に記述することができるため,「解 決すべき問題」である What を記述することができる. したがって, この宣言的な記述 箇所において,操作的な記述を行わなければ,「実行可能性の影響」を回避することがで

きる. さらに, 前述の VDMTools のインタープリタ機能を用いて, 仕様アニメーション

により動作検証を行うことができる. しかし, 評価者は,「入力時の内部状態」と「出力 時の内部状態」をあらかじめ作成しておく必要があるため, 仕様アニメーションにより 動かすときに,評価者の作業工数が課題となる.

ドキュメント内 九州大学学術情報リポジトリ (ページ 62-65)