再帰関数への変換による不変表明の生成
スポンサーリンク
概要
- 論文の詳細を見る
プログラムの正当性の検証に関してループに対する不変表明を生成することを考える。この不変表明の生成に関しては、KatzとManna,Wegbreit,DunlopとBasili,淡等などの方法がある。これらの方法は、フローチャートプログラム上または等価な論理プログラム上で不変表明を生成した。ここで提案する方法は、フローチャートプログラムでの繰り返し部分を等価な再帰関数で置き換えることにより、繰り返しのない単純なフローチャートプログラムに変換する。そしてプログラムの検証を変換した再帰関数に関する帰納法により証明を試みる。通常、この証明はうまくいかないが、以下で述べる条件のもとで証明すべき式として、再帰関数において常に成り立つ関係を導くことができる。この関係を一般化し、再帰関数を使わずに表したものを不変表明の候補とする。再帰関数についての関係式を求めることができるのは、postconditionにある論理式や関数の定義(以下基本定義)とプログラムとの構造が一致している場合である。
- 一般社団法人情報処理学会の論文
- 1991-02-25
著者
関連論文
- 変換履歴の再利用による高レベルのプログラム変換
- ハイパーリングのハイパーキューブへの埋め込み
- AND-EXOR論理式の簡単化並列アルゴリズム
- 拡張前提式を用いたATMSの並列化
- リフレクション原理によるフレームシステムの拡張
- ハイパーキューブ上の安全な情報伝達 (計算モデルとアルゴリズム)
- 情報伝播アルゴリズムによる安全なメッセージ伝達
- Some Modifications of Lockout-Free Mutual Exclusion Algorithms (Algorithms and Theory of Computing)
- ロックアウトフリーな相互排除アルゴリズム
- プログラム変換によるCPSコンパイラの最適化に関する研究
- 状態に依存したプログラムの合成
- 相互排他アルゴリズムのメモリ競合解析
- パーミュテーショナルグラフの独立全域木
- パーミュテーショナルグラフのブロードキャスティング
- 2段MOS論理回路網設計のための論理関数のグラフによる表現
- MOSセルを用いた2段論理回路綱の設計
- 2値画像の一符号化法と演算アルゴリズム
- 可逆論理回路のToffoliゲート数の下界(研究速報)
- AND-EXOR論理式最小化アルゴリズム
- AND-EXOR論理式最小化アルゴリズム
- AND-EXOR論理式最小化アルゴリズム
- 論理関数のあるクラスについて最小性を保証するAND-EXOR論理式の簡単化アルゴリズム
- 故障があるアレンジメントグラフのブロードキャスティング
- 故障があるアレンジメントグラフのブロードキャスティング
- プログラム変換における変換履歴再利用の支援
- 再帰関数への変換による不変表明の生成