被覆集合帰納法と代数的仕様の検証の機械的支援に関する考察
スポンサーリンク
概要
- 論文の詳細を見る
等式を用いて代数的に記述された抽象データ型の仕様が目的とする性質を満たすことの検証は,仕様に基づいて作成される,あるいは,自動生成されるソフトウェアの信頼性の向上のために重要である.代数的仕様の検証は,典型的には,等式で表現される性質がその仕様の意味する代数の上で成立することを証明することである.仕様の意味する代数が仕様を満たす代数のクラスの始代数であるときは,この検証は,仕様を等式理論とみなし,性質を表す等式がその理論の帰納的定理であることを証明することに対応する.代数的仕様の帰納的定理の機械的証明方法としては,Induction-less Inductionと呼ばれる手法が研究されてきている.この方法の問題点のひとつは,等式が帰納的定理ではないことが証明されたとき,仕様のどの部分にその原因があるのかが実行結果から分りづらいことである.このことは,証明の過程が直観的には理解しづらいためであり,仕様が満たすべき性質を満たすように,仕様を変更するための指針が得にくいことを意味している.このため,伝統的な帰納法の証明法も見直されてきており,構造帰納法の拡張である被覆集合帰納法が提案されている.本論文では,文献で提案した被覆集合帰納法に基づく証明例を挙げ,その機械的支援に関する考察を行なう.
- 一般社団法人情報処理学会の論文
- 1991-02-25
著者
関連論文
- 基本対称関数に基づく節をもつCNF論理式の充足可能性判定(計算論,計算モデル)
- ビットエラー通信路におけるスケーラブルCANの動作解析
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について (ソフトウェアサイエンス)
- シャローな依存対から構成される項書換え系の停止性の決定可能性
- 基本対称関数を付加したCNF論理式の充足可能性判定
- 制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序
- プレスブルガー文付き項書換え系における書換え帰納法について
- 例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム(ディペンダブルコンピューティング)
- 等式を規則化する変換の停止条件
- 動的型言語への柔らかい型付けによるエラー検出
- 対話型埋込みによる数独問題の設計ツール
- プログラム生成系GeneSysにおける等式仕様への否定の導入
- 導出木からのループ検出による論理プログラムの非停止性証明法
- 振舞等価性の証明のための等式付き書換えに基づく潜在帰納法
- 左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン
- 二階の書換え系における引数切り落とし法
- 通信プロセスに対する文脈変換手法を用いたモデル検査
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ(並列・分散)
- 診断テスト生成に基づくラベル付遷移システムのグラフィカル・デバッガ
- 制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み
- 高階書換え系における引数切り落とし法と実効規則
- 難解言語Malbolgeのチューリング完全性について
- 名古屋大学情報セキュリティ対策推進室の活動
- 右線形右シャローな項書換え系における文脈依存停止性の決定可能性について
- 条件付き等式の変換に基づくプログラム生成
- 制約付き項書換え系における書換え帰納法
- プレスブルガー文付き項書換え系における書換え帰納法について
- 非完全な仕様における振舞等価性の自動証明法
- 暗号プロトコル記述からカラーペトリネットへの変換による機密性検証
- 関数プログラムの停止性証明のための辞書式経路順序
- 単純型項書換え系における定理自動証明系HOPSYS
- 項書換え系の拡張された階層的結合における停止性のモジェラー性
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- 例外処理付きオブジェクト指向言語における情報流の安全性解析
- 形式的手法に基づくJavaScriptプログラムの型検査系の実現
- 等式理論を法とするDPLL遷移系について
- モデル生成法に基づくJavaScriptプログラム型検査の機械実行(ソフトウェア,フォーマルアプローチ論文)
- モデル生成に基づくJavaScriptプログラムの型検査系
- モデル生成に基づくJavaScriptプログラム型検査のためのフロントエンド
- オブジェクト指向プログラムに対するMessage Not Understood フォールト検知のための型検査アルゴリズム
- 項書き換え系のための並列計算機アーキテクチャ
- 項正規表現に基づくSpi計算の機密性検証
- 等式付き書換え系の等式数を削減する変換
- ナローイング計算の停止性証明のための依存グラフ法
- 意味マッチングと単一化に基づくパターン駆動並行リダクションモデル
- 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け(基礎理論,フォーマルアプローチ論文)
- 単純型項書換え系上の依存対法における実効規則と直積型項へのラベル付け
- LA-001 関数プログラムの再帰構造解析と強計算性に基づく十分完全性の証明法(A分野:モデル・アルゴリズム・プログラミング)
- 強計算性に基づいた単純型項書換え系の停止性証明法
- 静的依存対法による高階書換え系の停止性証明
- 強計算依存対法による高階書換え系の停止性証明
- GeneSysによるプログラム生成例とIntroduction規則の追加
- GeneSysによるプログラム生成例とIntroduction規則の追加
- 優先順序付き項書換え系の頭必須戦略の決定可能性
- SCCS動作式に対する unfold 変換によるLTSモデルの効率的な構成法
- SCCS動作式に対するunfold変換によるLTSモデルの効率的な構成法
- 命令を並列に実行するCPUに対するSCCSによるコンパイラの仕様記述
- 配列を扱う非線形先頭再帰プログラムからの再帰除去 (計算機科学基礎理論とその応用)
- 左線形シャローなどの項書換え系の停止性の決定性
- 準構成子項書換え系における停止性の決定問題
- 重なりを持つTRSにおける最外戦略の完全性について
- 順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について
- 制約付き木オートマトンとその閉包性
- データグラフの近似 (オートマトン理論および言語理論の新展開)
- 代数的仕様の階層的記述が可能なUltraC
- II_n型条件付き書換え系の合流性について
- メタ項書換え計算における規則中に規則を含む直交メタ項の合流性
- 有限なロケーションを持つ並行プロセス
- 有限なロケーションを持つ並行プロセス
- 代数的仕様における振舞等価性証明のための線形文脈帰納法について (計算モデルとアルゴリズム)
- 代数的仕様の実現検証のための線形文脈帰納法について
- 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み
- 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み
- SimpleObjectに対する型検査 : 型制約言語と推論アルゴリズム
- SimpleObjectにおけるクラス定義単位の型制約導出と型検査
- 左辺が一致するオーバレイ性を持つ左線形TRSの正規化戦略 (計算機科学基礎理論の新展開)
- 潜在帰納法による弱完全振舞仕様に対する振舞等価性の自動証明
- 被覆集合帰納法と代数的仕様の検証の機械的支援に関する考察
- プログラミング言語PL/0の代数的仕様記述(計算機科学の基礎理論とその応用)
- 依存対に基づく高階項書換え系の停止性証明
- 多ソート部分的代数に対する等式推論規則 (形式言語理論とオートマトン理論)
- 不完全指定形抽象データタイプの仕様記述と実現 (計算の複雑性に関する研究)
- 実時間通信プロセスの述語的仕様記述に対する検証法(並列・分散)
- 実時間通信プロセスの述語的仕様記述に対する検証法(並列・分散)
- 抽象データ型の代数的仕様の直接実現系Cdimple (関数型プログラミング)
- 順序ソートの自動推論とラベル付けに基づく合流性判定への応用 (計算モデルとアルゴリズム)
- DTRCに基づくTRS等価性の証明法の健全性
- 再帰型をもつオブジェクト指向計算モデルにおける例外処理の型付 (計算機科学基礎理論の新展開)
- オブジェクト指向計算モデルにおける例外処理機能の型付
- 分散JoinJAVAプログラムの通信エラーに対する型判定システム
- 2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ
- 弱最内戦略を完全にする項書換え系の等価変換 (計算機科学基礎理論とその応用)
- 難読プログラミング言語Malbolgeにおけるプログラム構成手法
- 変換と部分評価に基づく非左辺正規なメタ項の停止性証明 (計算機科学基礎理論とその応用)
- 項到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係 (計算機科学基礎理論とその応用)
- 融合変換を模倣するプログラム生成変換の戦略
- 限量子付き等式理論の変換に基づく仕様からのプログラム生成
- オブジェクト指向言語におけるクラス代入と型に関する考察