Snapshots generation via constructive logic

A software information system S allows users to store, retrieve and process information about the external world, typically in the form of a data base. We can differentiate two separate aspects in the data elaborated by S: the first concerns data types, while the second is related to the information on the external “real world” carried by the data. More precisely, a data type is a set of data together with the associated manipulations where the focus is on operations. In contrast, the other information carried by the data stored in S is strongly related to their meaning in the real world. The need for properly treating data according to their meaning is becoming increasingly important, due to the wide quantity of information exchanged on the Internet [5]. In this context, we are developing COOML [4] (Constructive Object Oriented Modeling Language), an OO specification language where the focus is on the information carried by data. The main features of COOML are: – a data model based on a predicative extension of the constructive intermediate logic E [3], following the Brower-Heyting-Kolmogorov interpretation of logical connectives; – a multi-layered structure, starting with the COOML logic layer, on top of which lies the problem domain logic, and finally the computation layer; – a data model based on the notion of ”pieces of information” i : P, where i is a structured information (”information value”) giving constructive evidence for the truth of a specification P. We believe that COOML may have a role as an OO specification framework, and we are developing different prototypical tools. This work is in progress and more details are available at the COOML web page http://homepages.inf.ed.ac.uk/amomigl1/cooml. In this abstract, we focus on automatic snapshots generation [1]: in modeling languages (we concentrate on the UML [2] as the de-fact standard) a snapshot represents a system state (object diagram) and snapshots generation in the presence of OCL constraints has proved to be useful both for understanding a specification and verifying its consistency in the problem domain. In our approach, snapshots are represented by the pieces of information and our snapshots generation algorithm is driven by the constructive content of COOML specifications.