Industrial-scale software is commonly very large and complex, making it difficult and time-consuming to develop. In order to manage complexity in software, developers break systems into smaller components which can be developed independently. Software contracts were first proposed several decades ago; they are used to explicitly specify the interfaces between software components to ensure that they work together correctly. Software contracts specify both the responsibility of a client using a service and of the component providing the service. The advantage of contracts is that they formalise what constitutes correct interactions between software components. In addition, they serve as documentation, as well as a basis for test cases, and help clarify correct use of inheritance. However, despite their usefulness, software contracts are still not widely used in mainstream software engineering. In this work, we aim to develop a new software contract tool which we hope will help increase the use of software contracts. We start our work by evaluating existing software contract technologies and uncover a range of inconsistencies and shortcomings. We find that there are disagreements surrounding even some of the most basic aspects of software contracts. Using the lessons learned from our analysis of existing tools, we design a new contract tool, PACT. We describe in detail the formal semantics and typing of PACT and develop a first implementation of our tool. Finally, we discuss the advantages of PACT over existing tools, including its rigorous separation of interfaces and implementations, its rich inheritance semantics, and its support for flexible and expressive definition of contracts.

Regression testing of an evolving software system may involve significant challenges. While, there would be a requirement of maximising the probability of finding out if the latest changes to the system has broken some existing feature, it needs to be done as economically as possible. A particularly important class of software systems are API libraries. Such libraries would typically constitute a very important component of many software systems. High quality requirements make it imperative to continually optimise the internal implementation of such libraries without affecting the external interface. Therefore, it is preferred to guide the regression testing by some kind of formal specification of the library. The testing problem comprises of three parts: computation of test data, execution of test, and analysis of test results. Current research mostly focuses on the first part. The objective of test data computation is to maximise the probability of uncovering bugs, and to do it with as few test cases as possible. The problem of test data computation for regression testing is to select a subset of the original test suite running which would suffice to test for bugs probably inserted in the modifications done after the last round of testing. A variant of this problem is that of regression testing of API libraries. The regression testing of an API is usually done by making function calls in such a way that the sequence of function calls thus made suffices a test specification. The test specification in turn embodies some concept of completeness. In this thesis, we focus on the problem of test sequence computation for the regression testing of API libraries. At the heart of this method lies the creation of a state space model of the API library by reverse engineering it by executing the system, with guidance from an formal API specification. Once the state space graph is obtained, it is used to compute test sequences for satisfying some test specification. We analyse the theoretical complexity of the problem of test sequence computation and provide various heuristic algorithms for the same. State space explosion is a classical problem encountered whenever there is an attempt of creating a finite state model of a program. Our method also faces this limitation. We explore a simple and intuitive method of ameliorating this problem – by simply reducing the size of the state vector. We develop the theoretical insights into this method. Also, we present experimental results indicating the practical effectiveness of this method. Finally, we bring all this together into the design and implementation of a tool called Modest.