関係データベースを用いた在庫管理プログラムの記述とその詳細化の正しさの証明

情報処理学会 HANDLE 被引用文献5件 参考文献12件 オープンアクセス

書誌事項

タイトル別名
  • カンケイ　データベース　ヲ　モチイタ　ザイコ　カンリ　プログラム　ノ　キジュツ　ト　ソノ　ショウサイカ　ノ　タダシサ　ノ　ショウメイ
  • Hierarchical Design oi' Stock Management Program using Relational Algebra and Its Correctness Proof
  • 仕様変換・詳細化

この論文をさがす

抄録

代数的言語・手法の有用性を調べるために、プログラム設計の共通問題である酒屋在庫管理間題に対して、我々の代数的言語を用いて抽象的順序機械型モデルで階層的に設計し、その実現の正しさの証明を一部行った。ある制限されたスタイルで仕様（プログラムの各処理が満たすべき性質）を記述することによって、整数上の論理式の恒真性判定を用 いた簡明な証明手続きにより、詳細化の正しさを半自動で高速に証 明できる場合がある。そのスタイノレ制限のもとでは、例えば、集合を引数とし、その任意の要素がある性質を満たすことを表す述語を用いて、仕様を記述する。本設計例では、そのスタイル制限のもとで自然に記述を行うために、処理の対象となるコンテナ情報などを関係データベースとしてとらえ、また、検証で導入する基本関数の補題をなるべく簡単なものにするため、記述に用いる基本関数を関係データベースの基本的な演算に限った。その記述に対して、上述の証明手続きで詳細化の正しさの証明が比較的容易に行えることを確 かめた。本実験の結果より、従来に比べ証明の実作業時間が大きく 改善できたことが分かり、本論文で採用した記述スタイノレ・証明法が有効であることが確かめられた。

収録刊行物

被引用文献 (5)*注記

もっと見る

参考文献 (12)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ