DISI Dipartimento di Informatica e Scienze dell'Informazione

Permissive Subsorted Partial Logic in CASL

M. Cerioli , Anne Haxthausen, Bernd Krieg-Brückner, and Till Mossakowski.
To appear in Algebraic Methodology and Software Technology (AMAST'97), Lecture Notes in Computer Science. Springer Verlag, 1997.
This paper presents a permissive subsorted partial logic used in the CoFI Algebraic Specification Language. In contrast to other order-sorted logics, subsorting is not modeled by set inclusions, but by injective embeddings allowing for more general models in which subtypes can have different data type representations.
Furthermore, there are no restrictions like monotonicity, regularity or local filtration on signatures at all. Instead, the use of overloaded functions and predicates in formulae is required to be sufficiently disambiguated, such that all parses have the same semantics. An overload resolution algorithm is sketched.

The compressed postscript version of this paper is available through anonymous ftp at ftp.disi.unige.it, in /person/CerioliM/AMAST97.ps.gz (95468 Kb).