Abstract machine and database schema

Recently, in the formal languages community, there has been much interestin a new method for the construction of programs. The approach consists in constructing a consistent and complete formal specification from informal requirements and then applying provably correct transformation steps until a target program is derived. This report illustrates the current state of an activity aimed at developing a database methodology which adopts this software engineering approach. In particular, it discusses the reasons for which the formal engineering method, B-Method, has been considered a good basis for our work. The report also introduces a new database model, the Schema Specification Model, and an associated formal notation, the Schema Specification Notation for the incremental specification of database schemas.