## FORMULA (Formal Modeling Using Logic Analysis)FORMULA (Formal Modeling Using Logic Analysis) is a unified framework for specifying domain-specific languages (DSLs) and model transformations. FORMULA allows modeling artifacts to be specified using logic programming (LP) extended with structuring and composition operators. This approach provides a formal foundation for the structural semantics of DSLs, which are non-operational, and the operational semantics of graph-like rewriting procedures, which arise in model transformations. FORMULA provides formal analysis of these model artifacts by means of a model finding procedure implemented on top of the SMT solver Z3. The tool also generates code for executing model transformations and testing if a model conforms to the structural semantics of a DSL. |
||