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).