B Maude: A formal executable environment for Abstract Machine Notation Descriptions
Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:NA6KF3B7record.jsonopen to challenge →
classification
cs.SE
cs.LO
keywords
maudeabstractdescriptionsenvironmentexecutablemachinenotationsemantics
read the original abstract
We propose B Maude, a prototype executable environment for the Abstract Machine Notation implemented in the Maude language. B Maude is formally defined and results from the implementation of the semantics of AMN as denotations in the $\pi$ Framework, a realization of Mosses' Component-based Semantics and Plotkin's Interpreting Automata. B Maude endows the B method with execution by rewriting, symbolic search with narrowing and Linear Temporal Logic model checking of AMN descriptions.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.