Executing Assertions via Synthesized Logic Programs

Abstract. Programming with assertions constitutes an e®ective tool to detect and correct programming errors. The ability of executing for-mal speci¯cations is essential in order to test automatically an imple-mentation against its assertions. However, formal assertions may de-scribe recursive models which are di±cult 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 transforma-tional synthesis can help to execute \expressive " assertions r of the form 8x(r(x), QyR(x; y)) where Q is either an existential or universal quan-ti¯er and R a quanti¯er free formula in the language of a formal theory C we call assertion context. This sort of theories is interesting because it presents a balance between expressiveness for writing assertions and existence of e®ective methods for compiling and executing them. Key words: assertion, automatic testing, correctness, de¯nite logic program, formal speci¯cation, synthesis, transformation.