The spec is out there, Extracting contracts from code

Abstract

A contract is a formal specification of the properties of a method. It has many uses in testing, verification and documentation. Despite all these benefits, developers almost never write contracts for their code due to the large amount of time required to write correct and expressive contracts. The project described in this thesis sets out to evaluate the possibility of extracting contracts from code using syntactic analysis, which is a not yet evaluated technique. Syntactic analysis is done by looking at the operations performed by code, rather than the result of those operations. Contracts were extracted by first parsing target source code into an abstract syntax tree, which was then analyzed to find defined code patterns which signaled the presence of some implicit contract. The information found within these patterns was then extracted and written as an explicit contract. In experiments involving 4 projects over 35 000 methods, our syntactic analysis tool extracted close to 60 000 behaviors, of which one-third were regarded as successful. The results are promising, even though performance of the syntactic analysis was somewhat inconsistent, it could produce contracts on a comparable level to those written by a human.