dc.creator | Galán Morillo, Francisco José | es |
dc.creator | Cañete Valdeón, José Miguel | es |
dc.date.accessioned | 2020-06-18T07:17:22Z | |
dc.date.available | 2020-06-18T07:17:22Z | |
dc.date.issued | 2004 | |
dc.identifier.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. | |
dc.identifier.isbn | 978-3-540-21377-2 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/97969 | |
dc.description.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 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. | es |
dc.format | application/pdf | es |
dc.format.extent | 20 | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | IFM 2004: 4th International Conference on Integrated Formal Methods (2004), p 521-540 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.subject | Assertion | es |
dc.subject | Correctness | es |
dc.subject | Formal specification | es |
dc.subject | Logic program | es |
dc.subject | Program synthesis | es |
dc.subject | Programming with assertions | es |
dc.subject | Meaning-preserving transformation | es |
dc.subject | Testing | es |
dc.title | A Method for Compiling and Executing Expressive Assertions | es |
dc.type | info:eu-repo/semantics/conferenceObject | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/submittedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de Sevilla. Departamento de Lenguajes y Sistemas Informáticos | es |
dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/978-3-540-24756-2_28 | es |
dc.identifier.doi | 10.1007/978-3-540-24756-2_28 | es |
dc.publication.initialPage | 521 | es |
dc.publication.endPage | 540 | es |
dc.eventtitle | IFM 2004: 4th International Conference on Integrated Formal Methods | es |
dc.eventinstitution | Cnaterbury, UK | es |
dc.relation.publicationplace | Berlin | es |