はじめに

段階的詳細化

現実のシステムの形式仕様記述は決して容易くはない．現実のシステムに与えられる要求の切り出し方や現実のシステムの仕様記述の方針等と，使用する形式仕様言語が従う形式化の考え方に差異がある．現実の（ソフトウェア）システムの形式仕様を記述する場合，システムを状態機械と見做して記述するのが一般的である．そして，状態機械を形式的に記述する際には，段階的詳細化という，下図に示すような段階的に記述に含まれる情報量を増やしていく方法が採られる．

段階的詳細化では，記述対象となるシステムの単純かつ抽象的な記述（上図の形式仕様0）から出発して，徐々に情報を追加し，最終的に実装と同程度まで詳細に記述する（上図の形式仕様n）．ある段階 i で記述した形式仕様iで充足される性質は，その次の段階 i+1 で記述される形式仕様i+1でも?充足されなければならない．一般に，段階的詳細化には，前向きの模倣(forward simulation)後向きの模倣(backword simulation)の２種類があり，詳細化の種類に応じて形式仕様iと形式仕様i+1の間に検証すべき条件がある．段階的詳細化には，その条件の証明の義務が伴う．

各段階iで記述した形式仕様iに対しては，その妥当性確認(validation)と検証(verification)が行われる．検証とは，使用する形式手法が基く論理の推論体系に基き以下の事柄を論理的に証明することである．

• 対象となるシステムに要求されている性質が形式仕様iで充足されること（但し，形式仕様iで表現できるものに限る）
• 前段階i-1で記述した形式仕様i-1から正しく詳細化されていること

それに対して，妥当性確認とは，形式仕様iが妥当であるか否か，すなわち，形式仕様iが（システムの依頼者の）意図から逸脱していることを確かめることである．

検証と異なり，妥当性確認は，「意図」という人の頭の中にあるものと形式仕様とを照らし合わせて行われる．「意図」が形式的に記述できない以上，論理的な推論では形式仕様の妥当性を確認することはできない．可能であればテストやシミュレーション等を利用しながら，想像される（依頼者の）意図と形式仕様の記述内容から判断するしか?方法はない．

現実のシステムはそれなりの規模と複雑さを持つ．いきなり実装と同程度の詳細度で書き始めてしまうと，?規模や複雑さにおいて実装とさほど変わらない，可読性の低い形式仕様ができてしまう．このような形式仕様の内容を把握することは困難で，その妥当性確認は難しい．

また，性質の記述と検証には，それに相応しい抽象度がある．段階的詳細化を経ないと，記述される性質や形式仕様の抽象度は，記述や検証に相応しい抽象度よりも低くなる．その場合，性質や仕様は過度に詳細に記述され，本来検証には必要のない情報が形式仕様に入り込むことになり，その結果，検証にかかる手間は増大する．

一方，システムに要求される振舞いには「似て非なる」ものが多数含まれる．適切な段階的詳細化の下では，?「似て非なる」振舞いの「似ている」部分と「非なる」部分を適切に切り分けて構造化することが可能になる． しかし，段階的詳細化が適切に行われないと，「似て非なる」振舞いを適切に構造化して纏め上げることが難しくなり，形式仕様の中に同じ表現がそこかしこに現れ，仕様の保守性を低下させてしまう可能性が高くなる．

さらに，開発の途中におけるシステムに対する要求の変更や追加は珍しくない．この場合，変更・追加された要求を満たすよう，形式仕様を改修することになるが，内容の把握が困難で，適切に構造化されていない形式仕様を改修すると，その場凌ぎの記述がそこかしこに追加され，記述の重複が増え，文書の構造はますます乱れることになる．?その結果，形式仕様の可読性や保守性は一段と低くなり，形式仕様の妥当性確認や検証はますます困難になる．

段階的詳細化は，形式仕様の可読性や保守性の低下を防ぎ，妥当性確認や検証の簡便化の助けとなる．

段階的詳細化における代数仕様言語の問題点

システムは状態機械と見なされることが多い． 例えば，CafeOBJでは，「基本的には」抽象データ型と同じようにして状態機械を記述する．

状態機械の状態のソートをSとし，遷移に与えられる入力のソートをA1,…,Anとすると，状態遷移を引き起こす操作Fは，次のような演算として宣言される．?

#!cafeobj

    F : A1 ... An S -> S

また，状態を構成する属性Gも，遷移Fと同様に演算として宣言される．

#!cafeobj

    G : S -> V

ここで，Vは属性Gの値のソートを表す．

遷移の振舞いは，状態機械の属性の値が遷移によりどのように変化するかで定められる．?ソートS,A1,…,Anの項を各々s,a1,…,anとすると、Fの作用の前後の属性Gの値である、G(s)とG(F(a1,…,an,s))の間の関係で遷移Fの振舞いが定められる．

状態機械の記述に段階的詳細化を適用する場合，その状態機械にとって本質的である，単純で抽象的な状態と自明な不変条件を持つ状態機械の記述から始める．そして，以下のようにして状態機械の情報を追加して、徐々に実装に近づけていく．

• 状態を構成する属性の数を増やす
• 属性の値の構造を豊かにする
• 状態機械の状態がどのように遷移しても成り立つ不変条件を強める

ここで気をつけなければならないのは，状態の詳細化に伴い，状態遷移を引き起こす操作も併せて詳細化されることである．それは，以下のような形で現れる．

• 操作に与えられる入力/出力引数の数が増える
• 操作に与えられる入力/出力引数の型が豊かになる
• 操作の事前・事後条件が強化される

ZやEvent-Bのように、入力引数の並び順を陽に規定せず、スキーマ包含やイベントの詳細化という詳細化前の記述をそのまま引き継げる，すなわち，入力/出力引数の数を増やしたり，その型を豊かにしたり，?事前・事後条件を強化したりできる手段を持つような言語や記法では，何の工夫することなく，詳細化に従って状態機械の記述を進めていくことができる．

しかし，代数仕様言語のように入力引数の並び順を陽に規定して演算を宣言する言語では、状態機械の遷移を演算で表現してしまうと、詳細化に従って状態機械の記述を進めることは煩雑になる．

例えば、状態機械の状態の属性を追加し、それに伴い，遷移Fに入力引数が追加される場合を考えよう．この場合，F は次のように詳細化される．

#!cafeobj

    F' : A1 ... Am S -> S (m > n)

詳細化前の状態の属性GのF'の作用による値の変化は，Fの作用による変化と変わらないものとしよう，このような場合，ZやEvent-Bでは、F'の作用による属性Gの値の変化を新たに記述する必要はない．しかし，代数仕様言語では，F' の作用による属性Gの値の変化とFの作用による属性Gの値の変化が等しいことを改めて宣言しなければならない．?

#!cafeobj

    G(F'(a1,...,am,s)) = G(F(a1,...,an,s))

現実のシステムの状態が持つ属性の数を考えると，これは非常に煩わしい．代数仕様言語で段階的詳細化に従い状態機械の記述を進めるには何らかの工夫が必要になる．

本文書では，代数仕様言語の１つであるCafeOBJで，段階的詳細化に従い状態機械の記述を進める工夫として，ある枠組を提示する．そして，その枠組に従って，OSEK/VDX仕様を書き進めていく．