代数的仕様記述言語CafeOBJ
スポンサーリンク
概要
- 論文の詳細を見る
形式仕様記述法はシステムの仕様を整った構造を持たせて厳密に記述することが出来る為、仕様の分析定義といったソフトウェアの開発工程を支援する方法として期待されている。代数仕様は形式仕様の手法の一つであり、抽象データ型を厳密に記述することが出来ることからシステムの仕様記述に最も適した方法の一つであるといえる。また代数的仕様記述法による仕様は項書換え系と呼ばれる機構によって実行が可能であり、仕様レベルでの無矛盾性の証への計算機支援を可能にしている。OBJは代数仕様の基く高い記述能力を持った言語である。CafeOBJはOBJの特徴を継承しつつオブジェクト指向プログラミングの様な動的な側面を陽に記述に取入れた言語として、現在、情報処理振興事業協会において開発中である。本稿では記述例を用いてCafeOBJの概要を説明する。
- 一般社団法人情報処理学会の論文
- 1993-09-27
著者
関連論文
- 項書換え系に基づく定理証明支援環境の構築
- 代数仕様言語CafeOBJのパラメータ化機構
- 実行可能な形式仕様言語CafeOBJ(4) : CafeOBJによるZ仕様のアニメーションの枠組み
- 実行可能な形式仕様言語cafeOBJ(3) : CafeOBJによるオブジェクト指向システムの仕様記述ライブラリの記述
- 実行可能な形式仕様言語CafeOBJ(2) : Cafeシステムの核アーキテクチャ
- 実行可能な形式仕様言語CafeOBJ(1) : CafeOBJの宣言的意味論
- CafeOBJによるプロセス記述ライブラリの作成
- 等式論理系における制約解消による証明支援環境構築の試み
- 等式論理系における制約解消による証明記述の枠組み
- 実行可能な形式仕様言語Cafe OBJの開発
- 代数的仕様記述言語CafeOBJ