自然言語の語彙分割による形式的仕様記述
スポンサーリンク
概要
- 論文の詳細を見る
従来, プログラムの仕様は自然言語で書かれていたが, 仕様を入力として, 各種の文書合成や無矛盾性などの検証, さらにはプログラムの自動合成といった意味に関した処理を計算機で行うには, 形式的意味をもつ言語により記述する以外に方法はない. 一方, 自然言語は人間にとってわかりやすいが, 非形式的すぎる. 本論文では, 曖昧性のない擬似的な自然言語(英語)でプログラムの形式的な仕様記述を段階的に行う方法を提案する. われわれの仕様記述言語の意味的基礎は一階の述語論理である. 仕様記述は, 使用される単語の意味を,下位のレベルで定義された単語を用いた英文や論理式, さらには抽象データ型やそのオペレーションを用いて, 定義しながら階層的に行っていく. このため, 最上位レベルの仕様は人にとってわかりやすい英文で記述することができる. 英文で書かれた仕様は, 単語の意味定義から導かれる述語論理の有意式への変換規則に従って, 論理式へと変換される. これにより, 仕様記述内容に厳密な意味が割り当てられ, この論理の公理系のもとで, 計算機による本格的な意味処理が可能になる.
- 一般社団法人情報処理学会の論文
- 1984-03-15
著者
-
米崎 直樹
東京工業大学大学院情報理工学研究科計算工学専攻
-
佐伯 元司
東京工業大学
-
榎本 肇
東京工業大学工学部情報工学科
-
米崎 直樹
東京工業大学大学院情報理工学研究科
-
榎本 肇
東京工業大学:富士通国際情報社会科学研究所
関連論文
- 記号論的暗号解析を用いたOblivious Transferプロトコルの解析(セキュリティ,フォーマルアプローチ論文)
- 記号論及び計算論によるセキュリティ解析の相互関係(数理的技法による情報セキュリティ)
- CAiSE'06参加報告
- CAiSE' 06参加報告
- ゴール指向要求分析のためのドメインオントロジの利用法(ソフトウェア開発とオントロジー,プロジェクト管理とモニタリング,一般)
- 要求分析のためのドメインオントロジ構築支援
- ドメインオントロジを用いた要求獲得支援ツールの実現
- 榎本肇先生を偲んで(追悼抄)
- アスペクト概念を利用したゴール指向要求獲得法
- 要求仕様と再利用可能な実現構造の振る舞いの差分検出に基づく要求分析(オブジェクト指向,言語設計(学生セッション))
- モデル駆動型開発におけるモデルメトリックスの定義手法
- 証明力が拡張された適切さの論理体系ER
- 線形論理CLL_eのモデルを用いた意味論
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- ユースケース記述に対するフレームワーク利用法の導出(アーキテクチャ・フレームワーク(学生セッション))
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法(セッション4-B : ネットワークセキュリティ(1))
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法
- 非同期型のコミュニケーションを用いた共同作業における阻害要因の分析
- 大学における情報化戦略と理工系情報学科の貢献
- 静的解析と動的解析を用いたデザインパターン検出手法
- UMLで記述したモデルの構成管理支援法(要求工学)
- デザインパターンのオブジェクト指向モデル化と支援ツールへの応用(ソフトウェアシステム)
- デザインパターンのオブジェクト指向モデル化と支援ツールへの応用
- フレームワークの要求仕様に対する適合性の評価手法
- グラフ変換を用いたUMLモデルのリファクタリング支援
- デザインパターンのモデル化と適用支援ツール
- ソフトウェアパターンの変換に基づくソフトウェア開発
- フレームワークに基づいた変更支援法について
- ベイジアンネットワークを用いたソフトウェア実装技術の選択支援
- 要求獲得におけるシソーラスの効果・効用について
- シソーラスを用いた要求分析法
- ASE2004参加報告
- 要求分析のためのシソーラス作成支援
- サマーワークショップ・イン・立山 開催報告
- 様相記号列統一化による様相論理定理証明器における自己代入の利用
- 様相記号列統一化による様相論理定理証明器の健全性と完全性
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法(セッション4-B : ネットワークセキュリティ(1))
- 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法
- 仕様記述過程モデル化のための実験と分析
- PAORE : パッケージ指向の要求獲得プロセス
- インタビューによる要求抽出作業を誘導するシステムの実現方法
- インタビューによる要求抽出作業を誘導するシステムの実現方法
- 要求工学における人工知能技術(知能ソフトウェア工学〔第4回〕)
- 6 要求仕様の品質特性(要求工学)
- ゴールグラフからのフィーチャモデル導出(要求,アーキテクチャ(学生セッション))
- 座談会 人間の知能と機械の知能 : 1986年9月6日 於:北海道大学
- CAiSE'06参加報告
- CAiSE'06参加報告
- 分割アルゴリズムに基づく同型グラフの検索について
- リスト構造に対する整合機能の形式化
- 要求工学国際会議(RE'04)の開催を振り返って(要求工学・ドメイン分析)
- 振る舞いモデルを用いたフレームワーク利用支援ツール
- オブジェクト指向は本当に役立っているのか : ソフトウェア工学の立場およびソフトウェア科学の立場から
- オブジェクト指向は本当に役立っているのか : ソフトウェア工学の立場およびソフトウェア科学の立場から
- シソーラスを利用した要求獲得方法(THEOREE)
- 編集操作の分類に基づくソースコード差分の構造化
- コモンクライテリアをドメイン知識としたゴール指向セキュリティ要求獲得法
- 自然言語に基づく静的システムの仕様のプロトタイププログラムへの変換手法
- 形式オントロジーに基づく遺伝子調節のための数値モデル
- 演繹体系による暗号方式の形式化と体系の性質としての暗号方式の安全性
- 演繹体系による暗号方式の形式化と体系の性質としての暗号方式の安全性
- Spi計算の型付けによる公開鍵暗号方式を用いたプロトコルのメッセージ認証の検証
- 初等的でないフレームを持つ様相論理の統一化による証明法
- 導出法による線形論理CLL_eの自動証明戦略
- オブジェクトの項表現を意味論の基礎とする論理体系としてのOntologyとその表現力
- リアクティブシステムの仕様記述言語とその記述操作の特徴付け
- 時相論理を用いた試験等価性の特性化
- 産業界からの理工系情報学科の研究教育内容への期待と大学の取り組み
- 大学における情報化戦略と理工系情報学科の貢献(パネル討論)
- 20周年記念特集号の編集にあたって(20周年記念特集)
- 時間論理によるリアクティブシステム仕様の検証の効率化(セキュアコンピューティング)
- SSLとリレーサーバを用いたPOP before SMTPのセキュアな実現法
- リアクティブシステムの段階的充足可能性とSafety Propertyの関係
- セキュリティプロトコルにおける暗号化メッセージの送信者による認知に関する検証法
- セキュリティプロトコルの一貫性および正常終了一致の同一参加者による複数セッションを考慮した検証法
- セキュリティプロトコルの一貫性および正常終了一致の検証法
- セキュリティプロトコルの一貫性および正常終了一致の検証法
- 自然言語の語彙分割による形式的仕様記述
- 合成可能なタブローによる仕様の差分的無矛盾性判定について (プログラム変換と記号・数式処理)
- 証明力を拡張した適切さの論理$ER$ (プログラム変換と記号・数式処理)
- 適切さと論理RとERの証明力の比較
- 適切さの論理ERの決定可能性
- 証明力を拡張した適切さの論理ER
- 大学における情報科学教育とリテラシー教育
- 欠陥仕様からの修正情報抽出に関する研究
- 合成可能な時間論理タブローの構成法
- 結合子の適切さによる人間の演繹的な推論の形式化 (&特集>「記号論理とAI」)
- 普通のUntil演算子を持つ命題実時間論理について
- 時相論理による段階的仕様記述プロセスに対応した検証法
- 証明の失敗から得られる情報を用いる様相論理定理証明戦略
- 時相論理による仕様記述の無矛盾性判定のための再利用可能なタブローについて
- 紛失通信プロトコルの解析のための可能世界意味論に基づく形式体系
- ソフトウェア発展と検証技術の未来 (特集 ソフトウェア発展)
- オブジェクトの生成,消滅を表現可能な論理体系DOL
- オブジェクトの生成、消滅を表現可能な論理体系DOL
- 様相論理 (<特集>非標準論理とその応用)
- The Temporal Semantics of Logic Programming
- 時相論理によるリアクティブシステム仕様の実現可能性に関する分類 (21世紀のソフトウェア工学)