ASAP - A Simple Assertion Pre-processor

Abstract

Assertions are widely known as a powerful tool to detect software faults during the debugging of software systems. Despite the maturity of software engineering tools, assertions are seldom used in practice. ASAP is a pre-processor for C programs which implements several concepts defined in the theory of formal specification, such as preconditions, postconditions, assertions related to intermediate states, loop invariants and variants, existential and universal quantifiers. In this paper, the notion of software contract is introduced, and shown how it is applicable with assertions. Finally, a collection of useful examples is given, and ASAP design and implementation is described.