Object-oriented frameworks are a popular means for efficiently producing quality software. We conjecture that formal proofs of a framework's properties help to prove properties of applications developed using the framework. Here, we describe a case study that was carried out in order to test this hypothesis on a chosen framework, Salespoint, and an application software, Mafiasoft, developed using this framework. In the first part of the paper, a central portion of the framework, its referential integrity property, and an important Mafiasoft function, mergeCustomers, are formalized. Since formalization, like any human activity, tends to be error-prone, we have chosen an iterative approach where we heavily rely on feedback from the Alloy model-checking tool. In the second part of the paper, the specification thus developed is recast in the Object-Z language, which in our opinion is easier to read and also more amenable to formal proofs. The results developed and model-checked in the first part are formally proven in the second. The referential integrity property established for the framework considerably simplifies the proof of the mergeCustomers operation. This finally supports our conjecture.    «

Object-oriented frameworks are a popular means for efficiently producing quality software. We conjecture that formal proofs of a framework's properties help to prove properties of applications developed using the framework. Here, we describe a case study that was carried out in order to test this hypothesis on a chosen framework, Salespoint, and an application software, Mafiasoft, developed using this framework. In the first part of the paper, a central portion of the framework, its referen...    »