RAISE FREQUENTLY ASKED QUESTIONS

Version: 1.16, Date and time: 95/02/15 08:47:56
Maintained by: tcszyh@aie.lreg.co.uk
Translated by: ugai@fujitsu.com

目次

1. RAISE って何?
2. RAISE 手法って何?
3. RSL って何?
4. RSL を使ってどんなシステムが記述できるの?
5. RSL ではどんなシステムは記述できないの?
6. どんな支援ツールがあるの?
7. RSL はどんな記述スタイルを支援してくれるの?
8. RSL はどんなモジュラリティを持っているの?
9. RSL のクラス拡張というのはあるの?
10. RSL はオブジェクト指向はサポートしているの?
11. RAISE は並列も扱うことができるの?
12. RSL は実行可能なの?
13. RSL はどんな意味論を持っているの?
14. RAISE の実装って何?
15. theory extension て何?
16. なにが証明できるの?
17. RAISE を使うとテストにどんな影響があるの?
18. RSL は Z と比較するとどうなの?
19. RSL は VDM と比較するとどうなの?
20. RAISE とリファインメント計算との関係はどうなっているの?
21. だれが RAISE と RSL を使っているの?
22. ほかには RAISE を使っている人はどこかにいるの?
23. RAISE に関する文書はあるの?
24. RAISE を勉強するにはなにからはじめればいいの?
25. RAISE についてもっと知りたい時はどうすればいいの?
26. Contact information
27. この FAQ に足りないものがあったら誰にいえばいいの?
28. 参考文献

RAISE って何?

• より信頼性の高いソフトウェア
• よりエラーの少ないソフトウェア
• よく文書の整備されたソフトウェア
• より容易に保守が可能なソフトウェア

• 強力な仕様記述と設計のための言語である RAISE Specification Language (RSL)
• 統合的な開発方法

RAISE 言語とツールはソフトウェア開発過程における仕様記述, 設計, 実装 の各場面を支援することに焦点を合わせています.

RAISE の目的は工業的なやりかたで計画され実行される規則を支援することに よってソフトウェア開発プロセスをより良くすることです. とくに RAISE は 最終的にコンパイル可能なコードを作るまでずっと開発を支援します. RAISE を使うと仕様から実装までのすべての開発において形式的に記録が残され, こ のことが最適な保守作業の前提条件になっているのです.

RAISE は `spepwise refinement' のパラダイム([Dij76],[Wir71],[Jon86])を 使ったシステマティックなソフトウェア開発の20年の研究と経験の結果できた ものです. RAISE についてもっと明確に言うと, European Commission - RAISE (ESPRIT I 315, 1985 - 1990) と LACOS (ESPRIT II 5383, 1990 - 1995, LArge scale COrrect Systems using formal methods) がスポンサーに なっている 2 つのプロジェクトがあり 200 人年以上の人がかかわっている.

RAISE メソッドって何?

RAISE ではこの検証に関するツールによる支援があります. このような形式的 検証が正しく行なわれることによって 得られる正しいソフトウェアに関する 健全な基礎が得られることになります. しかしながら, 形式的証明はひとつ の可能性に過ぎないのです. 実際の工業的なアプリケーションに関しては, 実際的な, あるいは経済的制約により検証はそれほど形式的には (それほど厳 しくは) 行なわれません.

RAISE メソッドは, 規定でもクッキングブックのようなものでもなくソフトウ ェア開発プロセスに関する枠組とガイドラインを与えるものです. このメソ ッドの柔軟さによってそれぞれのプロジェクトに実際的な問題を管理するため の厳しさのレベルを決めたり技術を選択したりすることができるのです. RAISE メソッドではユーザはそれぞれの環境やプロジェクトの標準などに応じ てどれ位形式的かというレベルを選択することができるのです.

RSL って何?

RSL の仕様はソフトウェアシステムの数学的なモデルであると考えることがで きます. 開発の中で異なるレベルの仕様の違いは, 抽象度のレベルの違いとな ります.

RSL を使ってどんなシステムが記述できるの?

4 世代ツール (巨大なユーザインターフェイスの設計を含むようなある種の管 理上のアプリケーション)によって簡単にできるようなソフトウェアの開発で はRAISE から同じように恩恵を受けることはできないでしょう.

• ネットワーク設計ツールセット
• 無人運転列車の保護システム
• 船のエンジンのモニタリングシステム
• 画像処理
• 出荷管理
• 人工衛星による位置の確認システム
• 人工衛星のペイロード管理に関する器具管理ユニットを開発するための 統合ツールセットの一部
• セキュリティアーキテクチャの記述 (Bell-La Padula & Bull's Sesame)
• 列車のモニタリングと再スケジューリングのためのシステム

RAISE ではどんなシステムは記述できないの?

しかしながら, RSL でモデル上の時間を扱うことは可能で, このような やりかたにしている理由は実時間性についてのみです.

どんな支援ツールがあるの?

言語と方法論を支援する十分利用に耐えるツールのセットがあります. RAISE のツールは完全に形式的な仕事のやりかたを証明の追跡と validationなどを 使って支援し, もっと緩やかなやりかたと同じように仕事を行なうことができ ます.

RAISE のツールは, 開発中のさまざまなもの (モジュール, モジュール間の関 係,理論, 正当性, ヒント)のエディット, 操作をするためのツールの集まりに なっています. RAISE のツールで提供される環境はソフトウェアシステムの開 発全体を追跡し, 文書化する機能を提供しています. この環境はそのソフト ウェアのライフタイムすべてに渡って保守, 発展を支援します. 現在この環境 は Unix と X を用いて Sun ワークステーション上で動作します.

• エディット
• 正当性の評価の実行
• 手続き型言語への変換
• 文書化の支援

正当性エディタは会話的に論理的正当性を開発するために使われ,後向き推論 にも前向き推論に使われます. 正当性エディタは,重要な機能を持っています.

• 簡素化機能. この機能は証明の規則を自動的に適用することによってより簡 潔な条件に縮小するために使われます. (一番いいのは真にすること)
• 実装条件拡張機能. この機能は 2 つのモジュール間の実装の関係が成り立 つ時に詳細な条件をつくり出す時に使われます.

文書整形器は, RAISE の実体を適当な形で抜き出し, 非形式的なテキストと RAISE の実体を含むような紙による文書をつくり出すために使われます現在 LaTeX の整形システムのみがサポートされています. しかしながら, 正当性 以外の実体は ASCII で手に入れることもでき,特殊文字は ASCII の列に変換 されます.

RSL はどんな記述スタイルを支援してくれるの?

• Z や VDM で使われるようなモデル指向の仕様. このスタイルを使うと仕様 の中で使われるデータは `モデル化' されたものになります. 例えばスタック は値の列としてモデル化されます. データに関する操作はデータのモデルにど のように働くかが記述されます. スタックの例では値をプッシュすることは列 の最初に値を加えることで, ポップすることは列の最初の値を取り除くことと 等価になります.
• Larch や OBJ で使われるような代数仕様. これはモデル指向よりももっと 抽象度が高い. このスタイルではデータはデータについての性質を表す公理を 用いて記述されます. スタックの例ではスタック s と要素 x に対して pop(sushi(x,s)) = s を定義します. このスタイルでは, 多くのモデルで公 理を充足します. RAISE メソッドでは代数仕様は一般にもっと具体的なデータ 構造が設計されるようにモデル指向で開発されます.
• Lisp, Miranda, Haskell のような applicative なプログラミング言語で用 いられるスタイルのような applicative 仕様. 大域的実行履歴や状態のよう なものはなく, 変数もありません. パラメタに関数を適用した結果が関数に 対するパラメタの機能なのです. 手続きのようなものもありません. したが って同じパラメタに対する関数を適用した結果は常に同じ結果になります.
• C, Modula-2, Pascal などの手続き型プログラミング言語で用いられるよう な手続き的仕様. このスタイルの顕著な特徴は, 実行履歴, 大域状態である. 変数が定義でき, 変更できる. したがって手続きの適用の順番が結果に重要な 影響をもたらす.
• CSP で使うような並行の仕様. 並行プロセスは同期チャンネルを通して互い に通信を行なうように定義されます.
• pre- post- 条件を用いたインプリシットな定義
• エクスプリシットな定義

RSL はどんなモジュラリティを持っているの?

RSL のモジュールは, 基本的なブロックと抽象的なユニットで構成されてい て, RAISE による開発は, これらを組み上げていくことである. モジュール 内部では RSL のエンティティすなわち, タイプ, 値, 変数, チャンネル,オブ ジェクトとほかのモジュールが定義される. RSL モジュールは プログラミン グ言語で言われる `モジュール', `パッケージ', `クラス' などに相当しま す. モジュールが自分のエンティティを定義している他のモジュールのエン ティティを参照できるので, RSL による仕様は, 階層的に構成されます. モ ジュールはパラメタ化され, generalised 仕様をサポートしています. これ は再利用可能なモジュールを作るために重要な機構です. モジュールは, そ のエンティティの名前を替えたり隠したりすることによって与えられた環境に 適合させることができます.

RSL のクラス拡張というのはあるの?

クラスの拡張は他のクラスの拡張によってパラメタ化されることがあります. そのようにして作られた仮引数は, 実引数から必要な性質を定義します. こ れらの性質は, パラメタ化されたクラスの拡張で利用可能となるものです.

RSL はオブジェクト指向はサポートしているの?

多相

RSL はサブタイプ多相 (あるタイプのサブタイプにある値の型を定義して関 数を適用できるようにすること)をサポートしていますが, 動的バインディン グはサポートしていません.

RSL は (例えば ML にあるような) パラメータの多相はサポートしていませ ん. しかしながら, 関数 `テンプレート' はあるタイプで実体化されるよう に定義することができます. 例えば, タイプ ELEM 上にいくつかの関数を定義 したモジュールは, タイプ ELEM を定義しているモジュールをパラメータとし て持つことができます.

   scheme LIST_FUNS(E : class type Elem end) =
     class
       value 
         reverse : E.Elem-list - > E.Elem-list
         reverse(seq) is ...
         ...
     end

いまこの関数は任意の型で定義されていて ELEM で実体化して使われます. パラメタ化の機能を使うと, パラメタの多相よりもより一般的なことができま す. 例えば, パラメタは公理による仕様を含むことができるので, Elem が全 順序の形になることができます.

RSL では関数の上書きをすることができるので, どの関数も上書きが静的に解 決できるのであれば何回でも宣言することができます. すなわち異なる関数の 定義は, それぞれのタイプ と/または 数のパラメタに対して適用しなければ なりません.

継承

継承は RSL の `拡張' 機能を使って行ないます. 他を拡張したモジュールは その定義と状態を継承します. しかしながら, 複数からの継承を行なった時に 継 承の不一致が起こった時の解決をする方法はありません. その不一致は静的 なチェックを行なっている時にエラーとして報告されます. 複数からの継承 は, 共有されるものを明示的なやりかた(パラメタ化によって)で仕様化されな ければなりません.

隠蔽

隠蔽は RSL の `hide' 機能を使って行ないます. この機能によってモジュー ルの中で定義されるエンティティが隠され, モジュールの外から参照できなく なります

RAISE は並行も扱うことができるの?

RSL のプロセスは, 入力, 出力, 選択, 並列合成を含む式を使って明示的に 仕様化され, 公理的な仕様が作られます. 並行動作を公理的に仕様化するために, RSL は特殊な `interlock' 演算を持っています.

RSL は実行可能なの?

RSL はどんな意味論を持っているの?

RAISE の実装ってなに?

• Property Preservation: A0 について証明されるすべての性質が A0 に関しても証明される. (一般的には,なりたたない)
• Substitutivity: 仕様の中で A0 のインスタンスが A1 のインスタンスで 置き換え可能であり, 新しくできた仕様がまえの仕様の実装になっている.

theory extension て何?

• 理論 T2 が 理論 T1 よりより多くの実体 と/または 性質を持つ時に T2 は T1 を拡張する.
• 理論 T1 で定義される実体を使って表現される理論 T2 のすべての性質が T1 の性質であるとき T2 は T1 を保守的に拡張する. 言い替えれば, T2 は T1 からの実体に対して何も新しい性質を加えない. 保守的でない拡張は `非保守的' と言う.

なにが証明できるの?

RAISE を使って作成されて正当化される条件には次の 2 種類があります.

• formal condition (RAISE の理論で明記される述語と開発関係). これらは 手で作らなければならない.
• confidence confition (RSL の部品では最終的とはならなく,予想できない 意味がある信頼性を増すための述語). これらは自動的に生成される.

RAISE を使うとテストにどんな影響があるの?

RSL は Z と比較するとどうなの?

RSL は 低レベルの仕様や並列性の機能に関して Z よりも優れています. し たがって, Z の仕様を RSL の仕様に変換することは, その逆よりは容易です.

Z と RSL の仕様記述のスタイルはしばしば全く異なるものになります. Z の 仕様は モデルベース, 主として applicative のスタイルで書かれます. 一 方 RSL は applicative と imperative のスタイルから一方を選択することが できます. あるいは代数仕様とモデルベース仕様から選択することができま す. 抽象レベルの違うものを仕様化することができるようになっていること によって, RSL はあるレベルから別のレベルへの開発を可能にしているので す.

仕様の部品(Z ではスキーム, RSL ではモジュール) を組み合わせることは RSL よりも Z の方が容易です. (文法上のオーバヘッドが少ない) しかしなが らおそらく大きなソフトウェアに関しては再利用性は低いでしょう. RSL の構 造化の仕組みはある種の ML の拡張のようなものです. 例えば, モジュール は他のモジュール上でパラメタ化することができ, RSL は パラメータとして 提供されるモジュールからの識別子を使うことができます. ただし, パラメタ の名前でそれを前置しなければなりません.

Z も RSL もある関数が適用された時に変更が無いような状態の細かな多くの 無意味の述語を入れるよりもより小さな状態に分けることが良いとしていま す. Z は一般的にそれぞれの小さな状態 (しばしば, ある特定の状態にそれぞ れの関数が適用可能になるのですが)をそれぞれ別のスキーマで扱います. 一 方 RSL は小さな状態を一つ以上のモジュールで関数を組み合わせます. これ は一般的に Z の仕様には多くの小さなスキーマが出現し, それとは対照的に, RSL の仕様ではより少ない大きなモジュールで構成されることになります.

RSL は VDM と比較するとどうなの?

VDM を使った相当数のケーススタディが発表されている. VDM を使った時の 形式的な側面のシステマティックな重要性とともにソフトウェアのモデリン グ, 仕様化, 開発のための相当量の技術や戦略が発表されていて,それらは RSL でも容易に利用することができる.

RAISE とリファインメント計算との関係はどうなっているの?

だれが RAISE と RSL を使っているの?

ほかには RAISE を使っている人はどこかにいるの?

ツールと一般的な情報に関しては Jan Storbank Pedersen <jsp@csd.cri.dk> コースと一般的な情報に関しては Maurice Naftalin <tcsmpn@aie.lreg.co.uk> と連絡を取ってみて下さい

RAISE に関する文書はあるの?

RAISE Overview

この文書には RAISE の考え方とその成立ちが書いてあり, 導入的な レベルで典型的な小さな例題を使って説明がされています. CRI から入手可能です. (つぎの章を見て下さい)

The RAISE Specification Language

この本は RSL のチュートリアルと RSL のリファレンスから構成されています. チュートリアルには RAISE Specification Language (RSL) の詳細な 導入が含まれています. トレーニングコースの基礎と同じようなことを 自分で勉強することを考えています. リファレンスの部分では, RAISE Specification Language (RSL) が詳細に定義されています.

この本は入手可能です.
The RAISE Specification Language
The RAISE Language Group
Prentice Hall
ISBN: 0-13-752833-7

The RAISE Development Method

この本は RAISE を使って 仕様化, 開発, verification, validation, 変換をどのように行なうかを, 勉強, トレーニング, 参考に利用されることを 考えています.

これはまた RSL の仕様の性質を正当化したいと思っている人のための ハンドブックにもなると考えています. この本には RAISE の正当性に関する 文法が記述されていて, 正当性の証明で利用される形式的証明規則が 載っています.

この本は 1995 年の春に出版される予定です.
The RAISE Development Method
The RAISE Method Group
Prentice Hall
ISBN: 0-13-752700-4

RAISE を勉強するには, なにからはじめればいいの?

• Introduction to RAISE
• Software Development using RAISE

• RAISE Tutorial (1 day)
• RSL and Method Course (3 days)
• RSL Course (5 days)
• RAISE Method Course (5 days)
• RAISE Justification Course (4 days)

CRI, CAP Programator と Lloyd's Register は顧問の仕事も行なっています.

RAISE についてもっと知りたい時はどうすればいいの?

RAISE を良く使っている人か,

Maurice Naftalin at Lloyd's Register <tcsmpn@aie.lreg.co.uk>
Jan Storbank Pedersen at CRI <jsp@csd.cri.dk>

Contact information

Maurice Naftalin
Lloyd's Register
Lloyd's Register House
29, Wellesley Road,
Croydon CR0 2AJ	
UK

Tel: +44 81 681 4040
Fax: +44 81 681 4839
email: tcsmpn@aie.lreg.co.uk


Jan Storbank Pedersen
Computer Resources International A/S 
P.O.Box 173
Bregner{\o}dvej 144
DK-3460 Birker{\o}d
Denmark

Tel: +45 45 822100
Fax: +45 45 821711
email: jsp@csd.cri.dk

Eld Zierau
CAP Programator
Produktionsvej 2
2600 Glostrup
Denmark

Tel: +45 44 94 44 44
Fax: +45 44 94 62 42
email: ez@sypro.dk

この FAQ に足りないものがあったら誰にいえばいいの?

この FAQ に関する示唆や訂正は, Zoe Hellinger at Lloyd's Register にして下さい.

Zoe Hellinger,
Lloyd's Register
Lloyd's Register House,
29, Wellesley Road,
Croydon CR0 2AJ
UK

参考文献

[BD92a] D. Bolignano and M. Debabi. On the Foundations of the RAISE Specification Language. LACOS Report Bull/DB/27, Bull Corporate Research Center, June 1992.

[BD92b] D. Bolignano and M. Debabi. Higher Order Communicating Processes with Value-passing, Assignment and Return of Results. In Proceedings of the ISAAC'92 Conference. December 1992.

[Dij76] E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976

[RLG92] The RAISE Language Group. THE RAISE Specification Language. The BCS Practioner Series. Prentice Hall, 1992 ISBN 0-13-752833-7

[RMG95] The RAISE Method Group.. The RAISE Development Method. BCS Practitioner Series. Prentice Hall, 1995 ISBN 0-13-752700 (To appear Spring 1995)

[Hoa85] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall series in Computer Science. Prentice-Hall International, 1985

[Jon86] C.B. Jones. Systematic Software Development using VDM. Prentice-Hall Series in Computer Science. Prentice-Hall International, 1986

[Mil90a] R. Milne. The proof theory for the RAISE specification language. RAISE Report REM/12, STC Technology Ltd, 1990.

[Mil90b] R. Milne. The semantic foundations of the RAISE specification language. RAISE Report REM/11, STC Technology Ltd, 1990.

[Wir71] N. Wirth. Program Development by Stepwise Refinement. Communications of the ACM, (14):221 - 227, 1971

Simon Hughes
Imperial College
Email: sph@doc.ic.ac.uk