代数的手法によるプログラムの検証
スポンサーリンク
概要
- 論文の詳細を見る
This paper makes it clear what is to be proved for the program verification in the framework of algebraic semantics of programming languages. First, we give an algebraic specification method of programming languages which is covenient to considering program verification, where the meaning of a program is considered as a function from inputs to outputs. Next we consider the intended function of a program as an abstract data type and specify it algebraically. Then we give an algebraic definition of the correctness of programs based on these frameworks
- 社団法人人工知能学会の論文
- 1987-09-01
著者
関連論文
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ
- テスト等価性に基づいた視覚的LTSモデル操作によるプロセス代数デバッガ(並列・分散)
- 正則な実時間通信プロセスに対するテスト擬順序の記号的特性化
- 診断テスト生成に基づくラベル付遷移システムのグラフィカル・デバッガ
- 赤外線通信を用いた頑健なモバイルアドホックネットワーク構築手法
- 赤外線通信を用いたモバイルアドホックネットワークの実現とその応用
- モバイルアドホックネットワーク構築のための分散アルゴリズムの提案とその実現
- D-5-4 表層パターンに基づく法律文の構文解析
- 対話同時通訳コーパスの構築とその特徴分析
- 座談会 「人工知能研究の現状と問題点」
- プログラミング言語の新潮流
- ソフトウェア科学会第4回大会
- 座談会 人間の知能と機械の知能 : 1986年9月6日 於:北海道大学
- Information Flow Graphを用いたATMSの解析
- Information Flow Graphを用いたATMSの解析
- Regular Adherenceとその諸性質について (形式言語理論とオートマトン理論)
- 特集「知的プログラミングの基礎」について
- 明日を担う工学教育を
- TD-1-1 オートマトン研究事始め
- 情報新時代に創造的な工学教育を(情報技術の新時代に向けて)
- 21世紀の研究者-研究者の流動性-
- 将来ビジョンの策定と提言を
- 研究会活動と学術分野における国際貢献
- 無線機器間の直観的な接続指示手法
- 項書換え系の拡張された階層的結合における停止性のモジェラー性
- 知識ベースに基づいた図書目録カードの理解
- 知識ベースに基づいた図書目録カードの理解
- 構造記述を用いた書誌項目域の自動分割
- 書誌情報ファイルの処理に対する効率評価
- 書誌情報のファイル格納に関する効率評価
- 英日話し言葉翻訳のための漸新的文生成手法
- 日本語-ウイグル語対訳辞書拡充のための日本語言い換え処理
- 日本語-ウイグル語対訳辞書拡充のための日本語言い換え処理
- 日本語-ウイグル語辞書の自動作成とその収録語の分析
- 音声対訳コーパスからの日本語待遇表現生成規則の自動獲得
- 日本語-ウイグル語機械翻訳のための格助詞の変換処理
- 派生文法に基づく日本語動詞句のウイグル語への翻訳
- 派生文法による日本語形態素解析
- 派生文法に基づく日本語-ウイグル語機械翻訳 : 動詞接尾辞の変換
- 派生文法に基づく日本語-ウイグル語機械翻訳 : 動詞接尾辞の変換
- 派生文法に基づく日本語動詞接尾辞の形態素解析
- モバイルアドホックネットワークにおけるコミュニケーション支援手法
- オブジェクト指向プログラムに対するクラス集合型検査の健全性
- オブジェクト指向プログラムに対するMessage Not Understood フォールト検知のための型検査アルゴリズム
- 項書き換え系のための並列計算機アーキテクチャ
- タビュレーション再帰法と項書換え系の等価変換への応用
- 項書き換えによる関数型プログラミング (関数型プログラミングとその応用)
- 連続動作代数に基づく項書換え系の意味論(計算アルゴリズムと計算量の基礎理論)
- 項書き換えシステムの束論的意味論について(アルゴリズムの数学的基礎理論とその応用)
- D-8-19 選好付き知識に対する統合操作の形式化
- 意味マッチングと単一化に基づくパターン駆動並行リダクションモデル
- 多エージェント系自己認識論理の決定手続き : 命題論理式への変換に基づく方法
- 英日話し言葉翻訳のための漸新的文生成手法
- 拡張性を備えたオープンな電話対話システム開発ツールTEDDI
- 拡張性を備えたオープンな電話対話システム開発ツールTEDDI
- 拡張性を備えたオープンな電話対話システム開発ツールTEDDI
- F-8 拡張性を備えた対話システム開発支援ツールの構築(音声・音声言語情報処理,F.音声・音楽)
- 主辞情報付き文脈自由文法に基づく漸進的な依存構造解析(自然言語処理)
- 確率文脈自由文法に基づく漸進的構文解析
- 多エージェント系自己認識論理の論理プログラムへの変換
- 主辞情報付き文脈自由文法に基づく漸進的な依存構造解析アルゴリズム
- 漸増的に端末を認識するアドホックネットワーク構築手法の評価
- 2000-NL-137-12 / 2000-SLP-31-7 マルチドメイン音声対話システムの構築手法
- 2000-NL-137-12 / 2000-SLP-31-7 マルチドメイン音声対話システムの構築手法
- 漸進的構文解析における構文的曖昧性とその解消
- SD-2-1 実走行環境下における車内音声データベース
- D-5-5 対訳コーパス自動対応づけ手法の定量的評価法
- ハザードのない最簡論理回路の設計
- 2N-4 確率文脈自由文法を用いた漸進的構文解析における出力タイミング決定手法
- 漸進的な構文解析における出力タイミング決定の一手法
- 文法的不適格文に対する漸進的構文解析手法
- 2ZA-1 漸進的処理に基づく音声対話メールツールSync/Mailの評価(マルチモーダル,一般講演,インタフェース)
- 3N-2 文脈自由文法の変換に基づく漸進的な話し言葉翻訳手法
- SCCS動作式に対する unfold 変換によるLTSモデルの効率的な構成法
- SCCS動作式に対するunfold変換によるLTSモデルの効率的な構成法
- 命令を並列に実行するCPUに対するSCCSによるコンパイラの仕様記述
- 二値画像に対する並列形処理と逐次形処理 (形式言語理論とオートマトン理論)
- 車内音声対話システムのための事例に基づく発話意図推定
- 車内音声対話システムのための事例に基づく発話意図推定
- Sync/Mail : 話し言葉の漸進的変換に基づく即時応答インタフェース
- Sync/Mail : 話し言葉の漸進的変換に基づく即時応答インタフェース
- Sync/Mail : 話し言葉の漸進的変換に基づく即時応答インタフェース
- 発話に即時応答可能なメールツールの提案
- 不適格表現を活用する漸進的な英日話し言葉翻訳手法
- 漸進的な英日話し言葉翻訳システムにおけるチャートに基づく変換手法
- 樹状言語の階層構造 (情報科学の数学的理論)
- 片側文脈規定形文法について (情報科学の数学的理論)
- String Controlled Grammar (情報科学の数学的理論)
- 名古屋大学工学部情報処理関係研究室紹介
- 実走行車内音声対話データベース
- 実走行車内音声対話データベース
- 実走行車内音声対話データベース
- 実走行車内音声対話コーパスの設計と特徴
- 実走行車内音声対話コーパスの設計と特徴
- 実走行車内音声対話コーパスの設計と特徴
- プログラムの検証と完備な述語のクラス(計算機構に関する数学的基礎理論とその応用)
- 非決定性プログラムの全面的正当性 (形式言語理論とオートマトン理論)
- 日本語-ウイグル語機械翻訳のための動詞接尾辞に関する一考察
- 日本語-ウイグル語機械翻訳における助動詞のパラメータ化による処理
- 日本語とウイグル語の助詞の対応関係とその機械翻訳への応用