Discovery of likely program constraints via static and dynamic analysis

This work is concerned with the task of automatically inferring constraints on the behavior of correct target programs via program analysis. The ultimate goal of this task is to recover a program specification from the program itself that closely approximates its essential behavior. Such a specification is called an essential specification for a program. This work focuses on an essential specification which is stated in terms of higher-level constraints that are intended to be used by a human developer for the purpose of understanding the target program.;In an effort to discover more program-specific constraints, several approaches are explored. The first approach facilitates the introduction of polymorphic constraints into the language of dynamic constraint inference. Such polymorphic constraints reveal the specification of the runtime behavior of the systems.;The second technique involves preliminary lightweight analysis of the source code of the target program. The static information is then used to formulate constraint hypotheses that are checked dynamically. This approach allows for the inference of program-specific disjunctive constraints and constraints on the behavior of collections.;Having introduced new constraints into the language of constraint inference, this work also proposes a quantitative evaluation methodology for constraint inference techniques. The proposed methodology can be applied to measure both how closely a particular tool approximates the desirable specification of a program, as well as the percentage of useful constraints in its output. The measures are produced within the context of the essential specification of a program.;Finally, this work proposes comprehensibility as a unifying application-oriented criterion for evaluating the quality of structural design in the form of the Comprehensibility Thesis.