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

1997 年度 研究成果報告書概要

代数的手法に基づくソフトウェアの検証の基礎的研究

研究課題

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

基盤研究(C)

配分区分補助金
応募区分一般
研究分野 計算機科学
研究機関名古屋大学 (1997)
北陸先端科学技術大学院大学 (1995-1996)

研究代表者

酒井 正彦  名古屋大学, 工学研究科, 助教授 (50215597)

研究分担者 外山 芳人  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00251968)
山本 晋一郎  名古屋大学, 工学研究科, 講師 (40240098)
研究期間 (年度) 1995 – 1997
キーワード項書換え系 / 合流条件 / 停止条件 / E単一化 / 完備化
研究概要

本研究は等式論理における検証法の確立し,さらに,一般のソフトウェアを代数的手法を用いて等式論理に自動的に変換することにより,これらの検証への応用を図るものである.本研究により、以下の結果が得られた。
(1)停止順序を満たす等式を通常の項書換え規則とみなし,これを満たさない等式は集合としての書換え規則とみなす項集合書換え系の形式的定義を与えた.
(2)項集合書換え系においては,通常の項書換え系におけるE合同上の書換えよりも若干緩い条件で停止性を持つ。
(3)停止的かつ左線形な項集合書換え系はその危険対が合流するならば合流性を持つ。
(4)項集合書換え系における完備化のための推論規則を与えた。
(5)項集合書換え系を試作し、効率的な実現について検討した。
(6)結合律と交換律による商の上の書換え系の停止性について検討した。
(7)優先順位付き項書換え系の定義を行ない,その等式論理に基づく意味論を与えた.これにより,関数型プログラムを等式論理に変換して検証するための基礎が得られた.

  • 研究成果

    (8件)

すべて その他

すべて 文献書誌 (8件)

  • [文献書誌] 高橋、酒井、外山: "条件付き項書換え系の合流性について" 電子情報通信学会論文誌. J79-D-I. 897-902 (1996)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] 粕谷, 酒井, 山本, 阿草: "項集合書換え系とその合流性" 電子情報通信学会論文誌. J80-D-I. 325-334 (1997)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans. on Information and System. E80-D. 1176-1182 (1997)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] M.Sakai, Y.Toyama: "Semantics and Strong Sequentiality of Priority Term Rewriting Systems" Theoretical Computer Science. (to appear). (1998)

    • 説明
      「研究成果報告書概要(和文)」より
  • [文献書誌] Y.Takahashi, M.Sakai, Y.Toyama: "On the confluence property of conditional term rewriting systems" Transactions of IEICE. J79-D-I (in Japanese). 897-902 (1996)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] H.Kasuya, M.Sakai, S.Yamamoto, K.Agusa: "Term Set Rewriting Systems and their Confluent Property" Transactions of IEICE. J80-D-I (in Japanese). 325-334 (1997)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans.on Information and System. E80-D. 1176-1182 (1997)

    • 説明
      「研究成果報告書概要(欧文)」より
  • [文献書誌] M.Sakai, Y.Toyama: "Semantics and Strong Sequentiality of Priority Term Rewriting Systems" Theoretical Computer Science. (to appear). (1998)

    • 説明
      「研究成果報告書概要(欧文)」より

URL: 

公開日: 1999-03-16  

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

Powered by NII kakenhi