A Method for Compiling and Executing Expressive Assertions
|Author/s||Galán Morillo, Francisco José
Cañete Valdeón, José Miguel
|Department||Universidad de Sevilla. Departamento de Lenguajes y Sistemas Informáticos|
|Abstract||Programming with assertions constitutes an effective tool
to detect and correct programming errors. The ability of executing formal
specifications is essential in order to test automatically a program
with respect to ...
Programming with assertions constitutes an effective tool to detect and correct programming errors. The ability of executing formal specifications is essential in order to test automatically a program with respect to its assertions. However, formal specifications may describe recursive models which are difficult to identify so current assertion checkers limit, in a considerable way, the expressivity of the assertion language. In this paper, we are interested in showing how transformational synthesis can help to execute “expressive” assertions of the form ∀x(r(x) ⇔ QyR(x, y)) where x is a set of variables to be instantiated at execution time, Q is an existential or universal quantifier and R a quantifier free formula in the language of a particular first-order theory A we call assertion context. The class of assertion contexts is interesting because it presents a balance between expressiveness for writing assertions and existence of effective methods for executing them by means of synthesized (definite) logic programs.
|Citation||Galán Morillo, F.J. y Cañete Valdeón, J.M. (2004). A Method for Compiling and Executing Expressive Assertions. En IFM 2004: 4th International Conference on Integrated Formal Methods (521-540), Cnaterbury, UK: Springer.|
|A Method for Compiling.pdf||328.3Kb||[PDF]||View/|