システムの概要

MENDELS ZONE上の開発は、オブジェクトを生成する“代数仕様フェーズ”と
オブジェクトを結合する“ペトリネットフェーズ”に分けられる。

図１に代数仕様フェーズの画面イメージを示す。




図 1 



ユーザは、オブジェクトの機能(メソッド)を代数的仕様記述で与える。正
しい仕様を記述するために、MENDELS ZONEは、仕様の文法チェック、項書
換えとしての直接実行、潜在帰納法による検証などの支援を行なう。ユーザは、
より仕様の満たすべき検証項目を入力すると、MENDELS ZONEは仕様がその
検証項目を満たしているかどうかを自動検証し、で検証手続きの進行状況が
確認できる。正しさが確認されたら、MENDELオブジェクトヘ自動変換を行な
う。
図2にペトリネットフェーズの画面イメージを示す。
自動変換で生成されたオブジェクトは、の部品ライブラリに登録される。オ
ブジェクトの結合は高レベルペトリネットで表現することができ、その記述は
のペトリネットエディタでマウス操作のみで行なえる。


					- 99 -