Advanced Specification Formalisms

The people of this group mainly involved in this area are E.Astesiano and M.Cerioli (Contact person)

A very natural way of describing the data structures used by (any paradigm of) programming languages is using algebraic approaches.
Indeed, data structures consist of collections of data type elements and functions handling them, that should be their interface with the users, corresponding to the rigorous mathematical concept of algebra. Moreover using logical formulas the relevant properties of a data type can be captured, so that reasoning on its axiomatization allows to abstract from any implementative detail.
Although standard many-sorted algebras are a powerful tool to describe many simple data types, some features of very common data types are not easily and immediately represented by them, so that more sophisticated approaches have, and currently are, been investigated.
This group is mainly concerned with the following issues.

Partiality

Although each partial function can be represented as a total function on enriched domains, where a special element (bottom) has been added to represent the undefined, this coding usually does not respect the categorical structure of model classes and is not axiomatizable (in the general case).
Therefore, as many computable functions are inherently partial, in the late seventies the paradigm of partial algebras, that are simply algebras where operation symbols are interpreted by partial (= non necessarily total) functions, has been introduced. In the seminal papers on partiality, the form of logical formulas used to describe data types were restricted to the so called positive conditional axioms, because such formulas correspond to a natural coding of recursive definitions and guarantee the same properties used in total many-sorted approaches. But positive conditional axioms are too restrictive, for instance, to code extensionality. Hence if the data type to be axiomatized includes higher-order types, as it is the case for imperative languages with the usual model environment-store approach, where both environments and stores are functions and appear as argument in expression and code evaluation functions, such formulas are too poor.
A complete analyses of a richer logic for partial data types, called conditional, that is the minimal extension of the standard positive conditional approach able to express extensionality-like properties, has recently appeared in Free Objects and Equational Deduction for Partial Conditional Specifications.
Using the theory of partial conditional axioms, partial higher-order data types are fully investigated in Partial Higher-Order Specifications .
This group is currently involved in writing a chapter on partiality for the book Algebraic Foundation of Information Systems Specification (Hans-Joerg Kreowski, Bernd Krieg-Brueckner and Egidio Astesiano Editors), that will be the theoretical foundation for the semantics of the language proposed by the CoFI (Common Framework Initiative).

Non-strictness

A function from a domain A is called non-strict if it can yields a result on an input non belonging to A. There are basically two cases of non-strictness common in programming languages:


Please send suggestions and comments to: Last Updated:
Maura Cerioli cerioli@disi.unige.it
29 April, 1996