Inferring Visual Contracts from Java Applications

Visual contracts model the operations of components or services by pre- and post-conditions formalised as graph transformation rules. They provide a precise intuitive notation to support testing, understanding and analysis of software. However, creating a detailed model of a system in any language is error-prone. Visual contracts are no exception, and their specification of object states and transformations requires a deeper understanding of a system than models of externally visible behaviour. This limits their applicability in testing, verification and program understanding, thus inventing an effective technique for extracting visual contracts automatically would enable their wider use in general. In this thesis we study a reverse engineering approach to address such problems by extracting visual contracts dynamically from existing systems. We propose an inference solution and implement a prototype tool in Java with empirical evaluations of the performance, completeness, correctness and utilisations. The resulting contracts give an accurate description of the observed object transformations, their effects and preconditions in terms of object structures, parameter and attribute values, and allow generalisation by universally quantified (multi) objects. They support program understanding in general, and the analysis of tests based on a concise, visual and comprehensive representation of operations' behaviour in particular.