Process for Contract Extraction

Design by Contract is an approach to designing and developing software; it contains a set of methodological principles that help to produce correct and robust software. Contract specifications have never become a mainstream since it is a demanding task for programmers. This paper introduces a process for extracting formal contract specifications combining formal methods and human analysis. It is illustrated with two case study. We conclude that contract extraction is in some cases achievable, although the limitations of this process are that it requires human analysis and deep knowledge of the problem domain, and cannot be fully automated.