• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

論理型形式的仕様のプロトタイピング・システムの試作・評価

研究課題

研究課題/領域番号 07680373
研究種目

基盤研究(C)

配分区分補助金
応募区分一般
研究分野 計算機科学
研究機関早稲田大学

研究代表者

深澤 良彰  早稲田大学, 理工学部, 教授 (20165252)

研究期間 (年度) 1995 – 1996
研究課題ステータス 完了 (1996年度)
配分額 *注記
2,200千円 (直接経費: 2,200千円)
1996年度: 800千円 (直接経費: 800千円)
1995年度: 1,400千円 (直接経費: 1,400千円)
キーワードプロトタイプ / プロトタイピング / 形式的仕様 / Z / ZF記法 / 集合論 / 述語論理 / 導出規則 / プログラム合成
研究概要

ソフトウェア開発時には、そのソフトウェアに対してどのような性質・機能が要求されているかを厳密に定義する必要がある。一意で明確な定義を与えるために、形式的仕様は重要な役割を果たす。これまで多くの形式的仕様の記述言語が提案されてきた。我々は、記述能力の高さや数学的概念との親和性などから、集合論に基づく形式的仕様記述言語に注目している。このような言語に、ZF(Zermelo-Fraenkel)集合論に基礎を置く仕様記述言語Zがある。しかし、Zでは、集合に対応づけられる仕様中で用いられる部分関数は、一意である必要が置換公理によって求められる。仕様中の情報だけでは、一意であることを証明できない関数を用いて置かれた仕様は、不完全な仕様となる。その部分関数を、一意であることが証明できるように完全に仕様中で定義した時に、設計・実現に関する情報も仕様に書くことになるのであれば、その部分関数を仕様中で完全には定義せずにおくべきである。ただし、その場合、置換公理を満たすために、その部分関数が一意であることを、記述言語が暗黙の裡に保証する必要がある。
そこで、我々は不完全な定義の部分関数を仕様に導入できる言語Z++を定義した。一方、言語Zや、その拡張である言語Z++で書かれた仕様は、仕様を解釈するためのモデルが規定されていないため、一般には直接実行できない。そこで、プロトタイピイングによる利点を享受するために、設計・実現に関する情報を与える記述として実行時仕様と呼ぶ記述を導入した。ソフトウェアの定義を仕様と実行時仕様に分離することで、高いレベルの表現能力での仕様の記述と、実行時仕様に基づく仕様のプロトタイピングの両方が可能になった。本研究では、仕様の解釈としての実行時仕様の与え方とそれに基づく実行の枠組みを対象とした。また、いくつかの問題に本システムを適用した結果に基づいて、その評価を行なった。

報告書

(3件)
  • 1996 実績報告書   研究成果報告書概要
  • 1995 実績報告書
  • 研究成果

    (12件)

すべて その他

すべて 文献書誌 (12件)

  • [文献書誌] H.ARAI and Y.Fukazawa: "A Consistency Verification Method for Design Models in Design Environment" Systems and Computers in Japan. Vol. 27,No. 10. 811-818 (1996)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1996 研究成果報告書概要
  • [文献書誌] J.Baeg and Y.Fukazawa: "A Backward Navigator and its User Model" Proc. 2nt Conf. on Knowledge Based Softwave Eng.Vol. 2. 310-317 (1996)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1996 研究成果報告書概要
  • [文献書誌] 荒崎秀一,深澤良彰: "ドメインモデルを利用したプログラム理解支援について" ソフトウェア開発のためのドメイン分析・モデリングシンポジウム. 123-132 (1996)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1996 研究成果報告書概要
  • [文献書誌] 小野康一,河野誠一,深澤良彰: "述語論理に基づく仕様からの実行可能コードの導出技法" 早稲田大学情報科学研究教育センター紀要. 18. 18-26 (1996)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1996 研究成果報告書概要
  • [文献書誌] 小野康一,深澤良彰: "実行時仕様記述言語ZXの導入による高レベル形式的仕様の実行" レクチャーノート/ソフトウェア系. 15. 121-130 (1996)

    • 説明
      「研究成果報告書概要(和文)」より
    • 関連する報告書
      1996 研究成果報告書概要
  • [文献書誌] H.Arai and Y.Fukazawa: "A Consistency Verification Method for Design Models in Design Environment" Systems and Computers in Japan. Vol.27, No.10. 811-818 (1996)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1996 研究成果報告書概要
  • [文献書誌] J.Baeg and Y.Fukazawa: "A Bockward Navigator and its User Model" Proc.of 2nd.Conf.on Knowledge Based Software Engineering. 310-317 (1996)

    • 説明
      「研究成果報告書概要(欧文)」より
    • 関連する報告書
      1996 研究成果報告書概要
  • [文献書誌] H.Arai and Y.Fukazawa: "A Consistency Verification Method for Design Models in Design Environment" Systems and Computers in Japan. Vol.27,No.10. 811-818 (1996)

    • 関連する報告書
      1996 実績報告書
  • [文献書誌] J.Baeg and Y.Fukazawa: "A Backward Navigator and its User Model" Proc.of 2nd.Joint Conf.on Knawledge Bared Software Eng. Vol.2. 310-317 (1996)

    • 関連する報告書
      1996 実績報告書
  • [文献書誌] 荒崎秀一,深澤良彰: "ドメインモデルを利用したプログラム理解支援について" ソフトウェア開発のためのドメイン分析・モデリング技術シンポジウム. 123-132 (1996)

    • 関連する報告書
      1996 実績報告書
  • [文献書誌] 小野康一,河野誠一,深澤良彰: "述語論理に基づく仕様からの実行可能コードの導出技法" 早稲田大学情報科学研究教育センター紀要. 18. 18-26 (1996)

    • 関連する報告書
      1995 実績報告書
  • [文献書誌] 小野康一,深澤良彰: "実行時仕様記述言語ZXの導入による高レベル形式的仕様の実行" レクチャーノート/ソフトウェア学. 15. 121-130 (1996)

    • 関連する報告書
      1995 実績報告書

URL: 

公開日: 1995-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi