管理メニュー

Model Base

「仕様の推敲を練習する」のPFD

最終更新：

modelbase

- view
管理者のみ編集可

更新日2013-01-31
[ 形式手法の独学 ] / [ 「形式手法の独学」のPFD ]

「仕様の推敲を練習する」のPFD

各プロセスの説明

P201_練習用の仕様情報を作成する

  • 【なぜやるか】
    • 形式化の題材を得るため。
  • 【どのようにやるか】
    • 家電製品の機能、通信プロトコル、○○制度、ゲームのルール、etc...など興味のある題材を探す。
    • 題材を熟知している必要はない。
    • 規模が大きな(登場概念や制約の数が多い)題材は避ける。
    • 題材に登場する概念間の静的関係や、振る舞いなどをUMLなど(自分が把握できる形)でスケッチする。

P201'_仕様を推敲する

  • 【なぜやるか】
    • 対象システムを見直し
      ・概念の過不足
      ・概念間の関係性の見直し
      ・制約条件の過不足
      などの気づきを仕様情報に反映させため。
  • 【どのようにやるか】
    • 自分では十分自明であると思い込んでいる事はないか省みる。
    • 仕様情報に現れる言葉(用語、概念)の解釈を再考してみる。
    • 対象システムを分解し、狭めた範囲の中で再考してみる。

P202_仕様情報を数学的な構造に翻訳する

  • 【なぜやるか】
    • 解析器へ入力できる情報に変換するため。
    • 形式化を行うことで定義の曖昧さを実感するため(形式化の効力を実感するため)。
    • 自然言語や図式表現で説明しようとしている事を数学的表現にする変換する練習をするため。
  • 【どのようにやるか】
    • 仕様情報で説明されるシステム(問題領域)を定義する。
      具体的にはシステムを説明する語彙を洗い出し、それらの語彙を"モノ"(集合の要素)で表すか、"モノ"同士(集合間)の関係で表す。
      Alloyでは"モノ"はシグネチャで表し、関係はフィールドで表す。ただし、Alloyでは集合の集まりを"モノ"として定義できない。
    • 集合と関係で記述したシステムに対して、仕様情報から読み取った制約を与える。
      具体的には集合の要素に関する限量指定や、集合間の関係に関する制約を与える。

P202'_仕様を表す構造を修正する

  • 【なぜやるか】
    • 形式化の翻訳ミスを正すため。
  • 【どのようにやるか】
    • 不適切なインスタンスが出力される場合
      前提条件となる述語が成立しているかや、関係や集合の状況などをEvaluatorを使って丹念に確認してみる。
  • インスタンスが出力されない場合
    確信が持てる述語だけ残してあとは全てコメントアウトする。コメントアウトした述語を順番にアンコメントしながら、どの述語の追加でインスタンスが出力されなくるか特定する。
  • 解析器が応答しない場合
    • 探索スコープを狭めてみる。
    • 置き換え可能なら要素をone sigで宣言する。
    • 集合を限定できるなら、univを使う代わりに具体的な集合の型を使う。

P203_着目する性質を考察する

  • 【なぜやるか】
    • 仕様情報の不備や矛盾に気づくきっかけ作りをするため。
    • 仕様情報が規定する対象システムの責務の理解を深めるため。
  • 【どのようにやるか】
    • 制約条件で成形される問題領域上の境界の内外どちら側にあるかを明確化したいことを探す。
      仕様情報には問題領域の定義を与える情報とその問題領域の境界を適切に成形する制約条件を与える情報が含まれる。制約条件(境界を決める情報)は内包表現で与えられることも多く、関心事が境界の内外どちら側にあるかが一目瞭然でない。
      例えばある法律を考れば、その法律の規定条項が仕様情報の制約条件に対応するのだが、規定条項は禁止すべきあらゆる行為の枚挙ではなく内包表現で書かれている。そこで、いわゆる法の抜け穴(合法だが立法主旨に反する行為)が存在しうるか気になるのである。
      抽象によるソフトウェア設計の4章で掲載されている"自分が自分自身の祖父"は、上記の視点で着目する性質を考察する事例である。
  • 状態ベース仕様で状態遷移に関することを探す。
    対象システムの操作を規定した情報が主たる仕様情報となる場合は、操作の実行により不変条件が維持されることをに着目する。あるいは特定の状態へ到達するための操作パスが存在することに着目する。

P204_着目する性質を述語化する

  • 【なぜやるか】
    • 考案した仕様情報が、要求を実現しているかどうかの検査を実行するため。
  • 【どのようにやるか】
    • 起きてほしい状態や、起きてほしくない状態を述語としてpredで記述する。
    • 常に成立してほしい状態(不変条件)をassertで記述する。
    • システムの初期状態から仕様で定義されている操作を経て、起きてほしい状態へ到達可能であることを記述する。
      これはutil/orderingライブラリを利用して、初期状態から所望の状態へ至る状態の全順序集合が形成できることを言えばよい。

P205_充足例を探索する

  • 【なぜやるか】
    • Alloy語に翻訳した仕様記述が、自分の意図した通りであるかを確認するため。
    • ビジュアライザが作る図式表現を俯瞰することで、今認識している制約条件以外に留意すべき制約があることに気づけるため。
    • 制約条件の過不足や相容れない制約条件を発見するため。
  • 【どのようにやるか】
    • 最も小さなスコープで充足例を探索し、問題がなければさらに大きなスコープで探索する。
    • あえてインスタンスが発見できないと予想されるような制約条件で探索してみる。得てして予想に反してインスタンス現れ、思ってもいなかった課題を発掘できる場合がある。

P205'_反例を探索する

  • 【なぜやるか】
    • Alloy語に翻訳した仕様記述が、自分の意図した通りであるかを確認するため。
    • 着目する性質が満たされるかどうかを実験するため。
  • 【どのようにやるか】
    • 最も小さなスコープで充足例を探索し、問題がなければさらに大きなスコープで探索する。

P206_充足例のインスタンスを観察する

  • 【なぜやるか】
    • 仕様情報に課すべき新たな制約や変更すべき制約を発見するため。
    • 形式化の不備や誤りを発見するため。
  • 【どのようにやるか】
    • 確認すべきポイントがビジュアライザで見やすくなるようにテーマを調整する。
    • ビジュアライザでわかりにくい場合はTree表示で確認する。
    • 述語が成立するかどうかをEvaluatorで確認する。

P206'_反例のインスタンスを観察する

  • 【なぜやるか】
    • 仕様情報に課すべき新たな制約や変更すべき制約を発見するため。
    • 形式化の不備や誤りを発見するため。
  • 【どのようにやるか】
    • 確認すべきポイントがビジュアライザで見やすくなるようにテーマを調整する。
    • ビジュアライザでわかりにくい場合はTree表示で確認する。
    • 述語が成立するかどうかをEvaluatorで確認する。

P299_知見を整理する←繰り返しの練習によって得られた経験を整理する

  • 【なぜやるか】
    • 練習で得られた知見を整理発展させるため。
  • 【どのようにやるか】
    • 数学的な構造で仕様を表すために有用な数学用語をたな卸ししてみる。
    • またそれらの数学用語はどのように形式記述できるか研究してみる。
    • 抽象度の高い形式記述にするため仕様情報の何を捨象したのか振り返ってみる。
    • Alloyでは述語をどのように分割整理すると勝手がよくなるかを研究してみる。

各成果物の説明

D201_仕様情報

  • 【何を得るか、どんな状況になるか】
    • 題材に登場する概念の静的関係図や対象システムの振る舞いのスケッチがある。
    • 概念や振る舞いを既定する制約条件が列挙されている。

D202_仕様を表す構造の定義

  • 【何を得るか、どんな状況になるか】
    システムについての仕様情報が以下の定義へ翻訳される。
    • システムを構成する要素の定義
      • Alloyではsigやenumで定義する。
    • システムを構成する要素の集合の定義
      • Alloyではsigや引数なしのfunで定義する。
    • システムを構成する要素間の関係の定義
      • Alloyではフィールドで定義する。
    • システムに課される制約の定義
      • 具体的には以下の2つの観点についての制約
        ・要素の集合に関する制約
        ・要素と要素の関係に関する制約
      • Alloyではfactやシグネチャfact内の論理式、sigやフィールドを修飾する限量子や多重度、そしてfactやrunに引用されるpred内の論理式で定義する。

D203_着目する性質

  • 【何を得るか、どんな状況になるか】
    • 仕様情報には明記されていないが、自分が認識する対象システムの責務に照らし合わせて考えれば、当然期待されるであろう対象システムの性質や対象システムが与える規定について、見解が得られている。

D204_着目する性質の述語

  • 【何を得るか、どんな状況になるか】
    • 反例がないことを確認するためにcheckコマンドで引用する述語(assert文)。

D205_充足例のインスタンス

  • 【何を得るか、どんな状況になるか】
    • 解析器が出力した充足例を得る(一つも充足例がない場合もある)。
    • いくら待っても解析器から応答がない。

D205'_反例のインスタンス

  • 【何を得るか、どんな状況になるか】
    • 解析器が出力した反例を得る(一つも反例がない場合もある)。
    • いくら待っても解析器から応答がない。

D206_仕様に対する新たな気づき

  • 【何を得るか、どんな状況になるか】
    • 制約条件が不足しているため、期待しないインスタンスが現れることに気づく。
    • 制約条件が厳しすぎるため、期待したインスタンスが現れないことに気づく。~特にありがちなケースとして、制約条件Cについて前提条件Pがある(P=>Cである)ほうがが相応しいことに気づく。
    • 注目する集合サイズの適切な限量に気づく。~特に空集合のケースが考慮されていなかったことに気づく。
    • 単射、全射など概念間の適切な関係性に気づく。
    • 要素の適切な順序関係に気づく。
    • 振る舞いの仕様の場合に非常にありがちなケースとして、不変条件を忘れていることに気づく。
    • 同時に満たすことができない制約条件があることに気づく。
    • 仕様情報の形式化の際の抽象化が手ぬるいため、仕様考察の本質に関与しない概念が構造の定義の中に多く含まれ、その結果解析器が探索する空間が広くなり、いくら待っても解析結果が得られない状況になったことに気づく。
「「仕様の推敲を練習する」のPFD」をウィキ内検索
記事メニュー
人気記事ランキング
  1. 抽象によるソフトウェア設計／付録 A 練習問題 解答例
  2. Alloy Analyzer
  3. A.4.1 状態機械の定義
  4. A.3.1 驚くような三段論法
もっと見る
最近更新されたページ
もっと見る
目安箱バナー