Abstract
Executing algebraic specifications is done by considering the equations as directed rules from left to right in order to compute normal forms. To improve the expressiveness of algebraic specifications, we not only admit pure equations but conditional ones having the form of positive Horn clauses. Based on a hierarchical approach where conditions have to be evaluated by means of axioms at lower levels, syntactical criteria are provided which guarantee the Church-Rosser property and, therefore, the well-definedness of the operational semantics. Besides, these criteria turn out to be sufficient for the termination of the full substitution strategy as well. Automatic computation of normal forms is possible if each proper subspecification has the finite termination property additionally.
An extended version can be found in Dr 83 where detailed proofs are included.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Goguen, J.A./ Thatcher, J.W./Wagner, E.G.: An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types. Current Trends in Programming Methodology, Vol.IV (R.T. Yeh ed.), Prentice Hall, Englewood Cliffs, 1978
Thatcher, J.W./ Wagner, E.G./ Wright, J.B.: Data Type Specification: Parameterization and the Power of Specification Techniques. ACM Transactions on Programming Languages and Systems, Vol.4, 1982 also: IBM Research Report RC 7757, 1979
Burstall, R.M./ Goguen, J.A.: An Informal Introduction to Specifications Using CLEAR. The Correctness Problem in Computer Science (R. Boyer/J. Moore eds.), Academic Press, New York, 1981
Bergstra, J.A./ Klop, J.W.: Conditional Rewrite Rules: Confluency and Termination. Report No. IW 198/82, Dept. of Computer Science, Mathematisch Centrum Amsterdam, 1982
Drosten,K./ Gogolla,M./ Ehrich,H.-D./ Lipeck,U.: A Hierarchical Approach to an Operational Semantics for Conditional Algebraic Specifications. Forschungsbericht Nr. 144/82, Abt. Informatik, Univ. Dortmund, 1982
Drosten,K.: Towards Executable Specifications Using Conditional Axioms. Bericht Nr. 83-01, Institut fuer Informatik, TU Braunschweig, 1983
Ehrich,H.-D.: On the Theory of Specification, Implementation and Parameterization of Abstract Data Types. Journal ACM, Vol.29, 1982 also: Bericht Nr. 82/79, Abt. Informatik, Univ. Dortmund, 1979
Ehrig,H./ Kreowski,H.-J./ Mahr,B./ Padawitz,P.: Algebraic Implementation of Abstract Data Types. Theoretical Computer Science, Vol.20, 1982 also: Bericht Nr. 80-32, Fachbereich 20, TU Berlin, 1980
Ehrig, H./ Kreowski, H.-J./ Thatcher, J.W./ Wagner, E.G./ Wright, J.B.: Parameter Passing in Algebraic Specification Languages. Proc. Workshop on Program Specification 1981 (J. Staunstrup ed.), LNCS 134, Springer-Verlag, Berlin, 1982
Goguen, J.A./ Tardo, J.J.: An Introduction to OBJ: a Language for Writing and Testing Formal Algebraic Program Specifications. Specification of Reliable Software, IEEE, Cambridge (Mass.), 1979
Guttag, J. V.: The Specification and Application to Programming of Abstract Data Types. Technical Report CSRG-59, Univ. of Toronto, 1975
Huet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal ACM, Vol.27, 1980 also: Proc. 18th IEEE Symposium on Foundations of Computer Science, 1977
Knuth,D.E./ Bendix,P.: Simple Word Problems in Universal Algebras. Computational Problems in Abstract Algebra (J.Leech ed.), Pergamon Press, 1970
Liskov,B./ Zilles,S.: Programming with Abstract Data Types. SIGPLAN Notices, Vol.9, 1974
O'Donnell, M.: Computing in Systems Described by Equations. LNCS 58, Springer-Verlag, Berlin, 1977
Pletat,U./ Engels,G./ Ehrich,H.-D.: Operational Semantics of Algebraic Specifications with Conditional Equations. 7th CAAP, Lille, 1982 also: Forschungsbericht Nr. 118/81, Abt. Informatik, Univ. Dortmund, 1981
Remy, J.L.: Proving Conditional Identities by Equational Case Reasoning, Rewriting and Normalization. Technical Report, C.R.I.N., Nancy, 1982
Rosen,B.K.: Tree Manipulating Systems and Church-Rosser Theorems. Journal ACM, Vol.20, 1973
Sannella, D./ Wirsing, M.: Implementation of Parameterized Specifications. Proc. 9th ICALP (M. Nielsen-E.M. Schmidt eds.), LNCS 140, Springer-Verlag, Berlin, 1982
Wand,M.: Algebraic Theories and Tree Rewriting Systems. Technical Report No.66, Indiana University, Bloomington, 1977
Wirsing, M./ Broy, M.: An Analysis of Semantics Models for Algebraic Specifications. Theoretical Foundations of Program Nethodology (M. Broy/G. Schmidt eds.), Reidel Publ. Co., Dordrecht, 1982
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Drosten, K. (1984). Towards executable specifications using conditional axioms. In: Fontet, M., Mehlhorn, K. (eds) STACS 84. STACS 1984. Lecture Notes in Computer Science, vol 166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12920-0_8
Download citation
DOI: https://doi.org/10.1007/3-540-12920-0_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12920-2
Online ISBN: 978-3-540-38805-0
eBook Packages: Springer Book Archive