文献

J-GLOBAL ID：200902222586477409   整理番号：09A0650158

Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築

An SOS interpreter with negative premises and an equivalence checker by Maude

著者 (3件)： 伴潤 (名古屋大 大学院情報科学研究科) ,  今井敬吾 (名古屋大 大学院情報科学研究科) ,  結縁祥治 (名古屋大 大学院情報科学研究科)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 109  号： 41(KBSE2009 1-11)  ページ： 49-54  発行年： 2009年05月14日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本稿では,プロセス計算の操作意味を定義するときに一般的に用いられる構造操作意味定義(SOS)によって定義されるラベル付き遷移系を実現するインタプリタを書換え論理の処理系であるMaudeによって実装する。SOS規則の前件に否定を含む場合の充足性検査として,Maudeのメタレベルの探索機能を用いることで,一般的なSOSを解釈するインタプリタを構築する。さらに,SOSから導出されるラベル付き遷移系上での項に対する強双模倣等価性検証器をMaudeによって実装し,SOSによって定義される動作仕様上での等価性判定を行うツールを構築し,否定を含むSOSによって定義されるプロセス計算の例として,HennessyのTPLにおける等価性判定を示す。(著者抄録)

シソーラス用語： *インタプリタ ,  制御用計算機 ,  等価性 ,  *言語設計 ,  関数型言語 ,  操作的意味論 ,  遷移状態
準シソーラス用語： プロセス計算機 ,  操作意味論

分類 (1件)： 言語プロセッサ  (JD03040F)

タイトルに関連する用語 (8件)： Maude ,  否定 ,  意味 ,  定義 ,  インタプリタ ,  等価性 ,  検証 ,  構築