Abstract
The behavioural semantics of specifications with higher-order formulae as axioms is analyzed. A characterization of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, due to Reichel and recently generalized to the case of first-order logic by Bidoit et al, is further generalized to this case. The fact that higher-order logic is powerful enough to express the indistinguishability relation is used to characterize behavioural satisfaction in terms of ordinary satisfaction, and to develop new methods for reasoning about specifications under behavioural semantics.
This is a condensed version of [HS95].
Supported by a Human Capital and Mobility fellowship, contract number ERBCHBICT930420.
Supported by an EPSRC Advanced Fellowship and EPSRC grants GR/H73103 and GR/J07303.
Chapter PDF
Similar content being viewed by others
References
M. Bidoit and R. Hennicker. Proving behavioural theorems with standard first-order logic. Proc. 4th Intl. Conf. on Algebraic and Logic Programming, Madrid. Springer LNCS 850 (1994).
M. Bidoit and R. Hennicker. Behavioural theories. Selected Papers from the 10th Workshop on Specification of Abstract Data Types, Santa Margherita Ligure. Springer LNCS, to appear (1995).
M. Bidoit, R. Hennicker and M. Wirsing. Behavioural and abstractor specifications. Report LIENS-94-10, Ecole Normale Supérieure (1994). To appear in Science of Computer Programming. A short version appeared as: Characterizing behavioural semantics and abstractor semantics. Proc. 5th European Symp. on Programming, Edinburgh. Springer LNCS 788, 105–119 (1994).
J. Farrés-Casals. Verification in ASL and Related Specification Languages. Ph.D. thesis, Report CSR-92-92, Univ. of Edinburgh (1992).
J. Goguen and J. Meseguer. Universal realization, persistent interconnection and implementation of abstract modules. Proc. 9th Intl. Colloq. on Automata, Languages and Programming, Aarhus. Springer LNCS 140, 265–281 (1982).
M. Hofmann and D. Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. Report ECS-LFCS-95-318, Univ. of Edinburgh (1995). Available on WWW in http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/95/ECS-LFCS-95-318.
S. Kahrs, D. Sannella and A. Tarlecki. The semantics of Extended ML: a gentle introduction. Proc. Intl. Workshop on Semantics of Specification Languages, Utrecht, 1993. Springer Workshops in Computing, 186–215 (1994).
J. Meseguer and J. Goguen. Initiality, induction and computability. In: Algebraic Methods in Semantics (M. Nivat and J. Reynolds, eds.). Cambridge Univ. Press, 459–540 (1985).
T. Nipkow. Observing nondeterministic data types. Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane. Springer LNCS 332, 170–183 (1988).
P. Nivela and F. Orejas. Initial behaviour semantics for algebraic specifications. Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane. Springer LNCS 332, 184–207 (1988).
H. Reichel. Behavioural validity of conditional equations in abstract data types. Proc. of the Vienna Conf. on Contributions to General Algebra, 1984. Teubner-Verlag, 301–324 (1985).
D. Sannella and A. Tarlecki. On observational equivalence and algebraic specification. Journal of Computer and System Sciences 34:150–178 (1987).
D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. Proc. 1983 Intl. Conf. on Foundations of Computation Theory, Borgholm. Springer LNCS 158, 413–427 (1983).
O. Schoett. Two impossibility theorems on behavioural specification of abstract data types. Acta Informatica 29:595–621 (1992).
P.-Y. Schobbens. Second-order proof systems for algebraic specification languages. Selected Papers from the 9th Workshop on Specification of Abstract Data Types, Caldes de Malavella. Springer LNCS 785, 321–336 (1994).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hofmann, M., Sannella, D. (1995). On behavioural abstraction and behavioural satisfaction in higher-order logic. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds) TAPSOFT '95: Theory and Practice of Software Development. CAAP 1995. Lecture Notes in Computer Science, vol 915. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59293-8_199
Download citation
DOI: https://doi.org/10.1007/3-540-59293-8_199
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59293-8
Online ISBN: 978-3-540-49233-7
eBook Packages: Springer Book Archive