MISC

2009年5月14日

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

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
  • 伴 潤
  • ,
  • 今井 敬吾
  • ,
  • 結縁 祥治

109
40
開始ページ
49
終了ページ
54
記述言語
日本語
掲載種別
出版者・発行元
一般社団法人電子情報通信学会

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

リンク情報
CiNii Articles
http://ci.nii.ac.jp/naid/110007333738
CiNii Books
http://ci.nii.ac.jp/ncid/AN10013287
URL
http://id.ndl.go.jp/bib/10247086