Abstract
This paper presents a permissive subsorted partial logic used in the CoFI Algebraic Specification Language. In contrast to other ordersorted 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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Arbib and Manes. Arrows, Structures, and Functors — The categorical Imperative. Academic Press Inc, 1975.
P. Burmeister. Partial algebras — survey of a unifying approach towards a two-valued model theory for partial algebras. Algebra Universalis, 15:306–358, 1982.
M. Cerioli and J. Meseguer. May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173:311–347, 1997.
M. Cerioli, T. Mossakowski, and H. Reichel. From total equational to partial first order. In E. Astesiano, H.-J. Kreowski, and B. Krieg-Brückner, editors, Algebraic Foundations of Systems Specifications. 1997. To appear 9.
Joseph Goguen and RĂzvan Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4(3):363–392, September 1994.
J. Goguen and J. Meseguer. Eqlog: Equality, types, and generic modules for logic programming. In Douglas DeGroot and Gary Lindstrom, editors, Functional and Logic Programming, pages 295–363. 1986.
J. A. Goguen and J. Meseguer. Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105:217–273, 1992.
A.E. Haxthausen. Order-sorted algebraic specifications with higher-order functions. Theoretical Computer Science, 183, 1997. To appear.
A.E. Haxthausen and F. Nickl. Pushouts of order-sorted algebraic specifications. In Proceedings of AMAST'96, volume 1101 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
B. Wolff Kolyang, T. Santen. A structure preserving encoding of Z in Isabelle/HOL. In Proc. 1996 International Conference on Theorem Proving in Higher Order Logic (Turku), volume 1125 of Lecture Notes in Computer Science. 1996.
T. Mossakowski. Representations, hierarchies and graphs of institutions. PhD thesis, Bremen University, 1996.
Peter D. Mosses. CoFI: The common framework initiative for algebraic specification and development. Invited paper for TAPSOFT'97, 1997.
H. Reichel. Initial Computability, Algebraic Specifications and Partial Algebras. Oxford Science Publications, 1987.
D. S. Scott. Identity and existence in intuitionistic logic. In M.P. Fourman, C.J. Mulvey, and D.S. Scott, editors, Application of Sheaves, volume 753 of Lecture Notes in Mathematics, pages 660–696. Springer-Verlag, 1979.
CoFI: The Common Framework Initiative for Algebraic Specification. CASL — the COFI Algebraic Common Language Tentative Design: Language Summary10, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cerioli, M., Haxthausen, A., Krieg-Brückner, B., Mossakowski, T. (1997). Permissive subsorted partial logic in CASL. In: Johnson, M. (eds) Algebraic Methodology and Software Technology. AMAST 1997. Lecture Notes in Computer Science, vol 1349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000465
Download citation
DOI: https://doi.org/10.1007/BFb0000465
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63888-9
Online ISBN: 978-3-540-69661-2
eBook Packages: Springer Book Archive