Language definitions as rewrite theories

详细信息    查看全文

• 作者：Vlad Rusu^a ; Dorel Lucanu^b ; ^{dlucanu@info.uaic.ro" class="auth_mail" title="E-mail the corresponding author} ; Traian-Florin Şerbănuţă^c ; Andrei Arusoaie^b ; ^a ; Andrei Ştefănescu^d ; Grigore Roşu^d ; ^b
• 关键词：Operational semantics ; Rewrite theories ; Symbolic execution ; K Framework ; Maude
• 刊名：Journal of Logical and Algebraic Methods in Programming
• 出版年：2016
• 出版时间：January 2016
• 年：2016
• 卷：85
• 期：1
• 页码：98-120
• 全文大小：738 K

文摘

class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S2352220815000838&_mathId=si1.gif&_user=111111111&_pii=S2352220815000838&_rdoc=1&_issn=23522208&md5=ffb5f4a8576386dd1854f6e9e3d13e92" title="Click to view the MathML source">Kclass="mathContainer hidden">class="mathCode">$\mathbb{K}$ is a formal framework for defining operational semantics of programming languages. The class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S2352220815000838&_mathId=si1.gif&_user=111111111&_pii=S2352220815000838&_rdoc=1&_issn=23522208&md5=ffb5f4a8576386dd1854f6e9e3d13e92" title="Click to view the MathML source">Kclass="mathContainer hidden">class="mathCode">$\mathbb{K}$-Maude compiler translates class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S2352220815000838&_mathId=si1.gif&_user=111111111&_pii=S2352220815000838&_rdoc=1&_issn=23522208&md5=ffb5f4a8576386dd1854f6e9e3d13e92" title="Click to view the MathML source">Kclass="mathContainer hidden">class="mathCode">$\mathbb{K}$ language definitions to Maude rewrite theories. The compiler enables program execution by using the Maude rewrite engine with the compiled definitions, and program analysis by using various Maude analysis tools. class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S2352220815000838&_mathId=si1.gif&_user=111111111&_pii=S2352220815000838&_rdoc=1&_issn=23522208&md5=ffb5f4a8576386dd1854f6e9e3d13e92" title="Click to view the MathML source">Kclass="mathContainer hidden">class="mathCode">$\mathbb{K}$ supports symbolic execution in Maude by means of an automatic transformation of language definitions. The transformed definition is called the symbolic extension   of the original definition. In this paper we investigate the theoretical relationship between class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S2352220815000838&_mathId=si1.gif&_user=111111111&_pii=S2352220815000838&_rdoc=1&_issn=23522208&md5=ffb5f4a8576386dd1854f6e9e3d13e92" title="Click to view the MathML source">Kclass="mathContainer hidden">class="mathCode">$\mathbb{K}$ language definitions and their Maude translations, between symbolic extensions of class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S2352220815000838&_mathId=si1.gif&_user=111111111&_pii=S2352220815000838&_rdoc=1&_issn=23522208&md5=ffb5f4a8576386dd1854f6e9e3d13e92" title="Click to view the MathML source">Kclass="mathContainer hidden">class="mathCode">$\mathbb{K}$ definitions and their Maude translations, and how the relationship between class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S2352220815000838&_mathId=si1.gif&_user=111111111&_pii=S2352220815000838&_rdoc=1&_issn=23522208&md5=ffb5f4a8576386dd1854f6e9e3d13e92" title="Click to view the MathML source">Kclass="mathContainer hidden">class="mathCode">$\mathbb{K}$ definitions and their symbolic extensions is reflected on their respective representations in Maude. In particular, the results show how analysis performed with Maude tools can be formally lifted up to the original language definitions.