クリーンルーム法の謎解き

− sigfm 第２回月例会 −

当日の報告 | 当日の資料

--------------------------------------------------------------------------

３月３日に発足したSEAフォーマル・メソッド分科会(SIG-FM)のキックオフ・ミー ティングは大盛況でした。

そこで、今月の月例会は、クリーンルーム法についての講演と討論を企画しました。

　この企画は、クリーンルーム法の味噌はなにかの解明をねらったものです。この手 法が良いのは、レビューで仕様と実現を検査することで、開発要員の仕様化とプログ ラム作成能力の向上に寄与することだ愚考します。講師の染谷さんはこの手法を意識 したコンサルタントをしていますので、事例を中心にお話しいただきます。

　その後、多くの開発現場・現状の追認と、現在の形式的方法からみたクリーンルー ム法の批判、あるいは推進方法を議論します。

　なお、今後のsigfm月例会は、原則として毎月第１金曜日に開催することになりま したので、よろしくお願いします。

***************** 開催要領 *****************

1. 日 時： 2000年４月 ７日 (金) 13:30 〜 16:45

2. 場 所： 労働スクエア東京 702会議室 (東京・中央区 新富1-13-14)

3. プログラム：

13:00〜13:30　受付

13:30〜14:30　クリーンルーム法の概略と事例
染谷 誠 (日本ユニシス)

14:30〜15:00　質疑応答
15:00〜15:15　Coffee Break
15:15〜16:30　討論
16:30〜16:45　次回予定

17:30〜 懇親会@与太呂四谷店

---

当日の報告

by 佐原伸 SRA

クリーンルーム手法について（染谷さん）

• 手法に共感を持った

• 開発段階でほとんど無欠陥のソフトを作る
• 品質保証段階で、仕様通りの品質であることを科学的に保証する
  

• 実際に適用してみた

• コマンド行のＮ番目の引数を取ってくる関数について検証した
  • 仕様がほとんど書かれていない
  • コードに誤りがある
    • 仕様が曖昧であることが原因である兆候が見えた
    • プログラミングを行いながら仕様を考えているようだ
      • １重ループで、フラグで分岐
      • コマンド行の構文の規定が無かった
  • 言語はMS社のBasic
  • 顧客が仕様を書けなかったので、染谷さんが書いた
    • 添付資料の仕様を提示した
  • プログラム例
    • 「意図関数に続くコードが意図関数を実現している」ことを検証する
    • プログラム関数（＝条件付き同時割当文）への還元
      • プログラム関数は意図関数と一致する
      • IBMによる講習は例題を提示して教えられた
        • 仕様記述言語がないので、適宜直感を援用する必要がある
          
      • 染谷さんの感想
        • 「テストを当てにしないでちゃんとしたプログラムを書きましょう」というところに本質があるのではないか？
          • 達成可能な努力目標なのだ
        • 必ずしもフォーマルではないが、フォーマルの枠組みに直すことは可能
        • コードのトレースを通して、条件付き代入文にまとめていくという考え方なので、本質的かつ実用的なのではないか？
        • トラブルへの対策でコードレビューするが、問題が発見できない
          • 従来のコードレビューは属人性が高い
          • クリーンルー ム法は属人性が低い

Q&A

• クリーンルー ム法自体への質問
  • 開発方法論か？（澤田）
    • Yes
    • システムがあり、そのシステムへの刺激を状態遷移図からモデル化していく
      • 状態中のブラックボックスの仕様を意図関数で定義して、それをクリアーボックスで段階的に洗練して定義する
      • 実現はプログラミング言語
  • 自分のプロジェクトで採用する場合、どれくらいの労力がかかるか？（澤田）
    • 従来の開発イメージを抱いている人たちに対して、うまく合わない
    • 部分的に採用するのは難しい
    • 出荷後の欠陥が１０分の一になるので、トータルでは採算が合うというIBMの報告がある（伊藤）
  • 「ループ構造が意図関数を実現している」ことの検証方法は？（荒木）
    • WHILE p DO g OD; f ≡f　であることを検証する
  • クリーンルーム法の教育だけでマスターできるのか？（山崎）
    • そもそも意図関数が書けないのではないか？
    • いろいろな知識を投入することは前提となっている
      • Carrol Morganの本を読めといった方が簡単では？（山崎）
  • 同時割当文が互いに干渉しないようにするには、どうしたら？（佐原）
    • はじめにそういうプログラムありきだと、それなりに面倒ね（澤田）

討論

• 現在の形式方法からみたクリーンルー ム法の批判
  特に討論はなし
  
• ＸＰ
  Kent beck, Word Caninghamらが提唱している
  • Smalltalk流手法？
    • ソースプログラムのみ
    • 二人ペアーで開発する
  • クリーンルー ム法と通じるところがある（羽生田）
  • クリーンルー ム法と相反するものである（伊藤）
    
• 多くの開発現場・現状の追認
  • 今の若い人たちは、我々年寄りとやり方が違うのではないか？（澤田）
    我々のころは、ミルズやダイクストラの本を読んでいた
    • デザインパターンのインタープリタ・パターンは，ほとんどの人が分からない（羽生田、佐原）
    • 専門学校の先生にコンパイラー理論の基礎を教えるのに半年かかる（山崎）
  • 介護保険のプログラムの仕様はなぜ無いのか？（佐原）
  • 現場では「仕様を書く」ということは「手続き的仕様を書く」こと（伊藤）
  • 形式手法ではGuarded commandが「プログラム」だが、クリーンルー ム法はそれが「仕様」になっている（荒木）
    
• クリーンルー ム法の推進方法
  
• sigfmで各手法を分類・整理したい
  • いろいろな方が個別にやっているが、sigfmでまとめた方が良いのでは（山崎）

今後

• ５月１２日（金）13:30-16:45
  Catalysis（伊藤）
  
• ６月２日（金）13:30-16:45
  
• ７月７日（金）13:30-16:45
  
• 聞きたい話題と話者
  • 林晋さん（熊谷さん担当）
    • 検証論
    • 自動生成をあきらめた経緯
  • 井田哲夫さん（熊谷さん担当）
    • 関数型言語と形式仕様
  • CafeOBJまわり
    • 1. 振る舞い記述のモデル記述などがおもしろいはず
      • a JAIST森さん
      • b 澤田さんが、場合によっては代打ち
  • π計算
  • リアクティブシステム
    • 結局モダリティとアクション計算か？
  • 染谷さん翻訳出版に絡む話
  • プロセス代数
    • 静岡大の富樫さん
    • 法政の劉さん

当日の資料 (工事中)