×

Behavioral abstraction is hiding information. (English) Zbl 1105.68076

Summary: We show that for any behavioral \(\Sigma\)-specification \(\mathbb{B}\) there is an ordinary algebraic specification \(\widetilde\mathbb{B}\) over a larger signature, such that a model behaviorally satisfies \(\mathbb{B}\) iff it satisfies, in the ordinary sense, the \(\Sigma\)-theorems of \(\widetilde\mathbb{B}\). The idea is to add machinery for contexts and experiments (sorts, operations and equations), use it, and then hide it. We develop a procedure, called unhiding, which takes a finite \(\mathbb{B}\) and produces a finite \(\widetilde\mathbb{B}\). The practical aspect of this procedure is that one can use any standard equational inductive theorem prover to derive behavioral theorems, even if neither equational reasoning nor induction is sound for behavioral satisfaction.

MSC:

68Q65 Abstract data types; algebraic specification

Software:

CafeOBJ; Maude; OBJ3; CCSL; CoCasl
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bergstra, J.; Heering, J.; Klint, P., Module algebra, J. Assoc. Comput. Mach., 37, 2, 335-372 (1990) · Zbl 0696.68040
[2] Bergstra, J.; Tucker, J. V., Equational specifications, complete rewriting systems, and computable and semicomputable algebras, J. Assoc. Comput. Mach., 42, 6, 1194-1230 (1995) · Zbl 0885.68092
[3] Bernot, G.; Bidoit, M.; Knapik, T., Observational specifications and the indistinguishability assumption, Theoret. Comput. Sci., 139, 1-2, 275-314 (1995) · Zbl 0874.68194
[4] N. Berregeb, A. Bouhoula, M. Rusinowitch, Observational proofs with critical contexts, in: Proc. FASE’98, Lecture Notes in Computer Science, Vol. 1382, Springer, Berlin, 1998.; N. Berregeb, A. Bouhoula, M. Rusinowitch, Observational proofs with critical contexts, in: Proc. FASE’98, Lecture Notes in Computer Science, Vol. 1382, Springer, Berlin, 1998.
[5] M. Bidoit, R. Hennicker, Proving behavioural theorems with standard first-order logic, in: Algebraic and Logic Programming (ALP’94), Lecture Notes in Computer Science, Vol. 850, 1994, pp. 41-58.; M. Bidoit, R. Hennicker, Proving behavioural theorems with standard first-order logic, in: Algebraic and Logic Programming (ALP’94), Lecture Notes in Computer Science, Vol. 850, 1994, pp. 41-58. · Zbl 0988.03525
[6] Bidoit, M.; Hennicker, R., Behavioral theories and the proof of behavioral properties, Theoret. Comput. Sci., 165, 1, 3-55 (1996) · Zbl 0872.68167
[7] Bidoit, M.; Hennicker, R., Modular correctness proofs of behavioural implementations, Acta Inform., 35, 11, 951-1005 (1998) · Zbl 0910.68145
[8] M. Bidoit, R. Hennicker, Observer complete definitions are behaviourally coherent, in: OBJ/CafeOBJ/Maude at Formal Methods’99, Theta, 1999, pp. 83-94.; M. Bidoit, R. Hennicker, Observer complete definitions are behaviourally coherent, in: OBJ/CafeOBJ/Maude at Formal Methods’99, Theta, 1999, pp. 83-94.
[9] Burstall, R.; Diaconescu, R., Hiding and behaviouran institutional approach, (Roscoe, W., A Classical Mind: Essays in Honour of C.A.R. Hoare (1994), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 75-92
[10] S. Buss, G. Roşu, Incompleteness of behavioral logics, in: Proc. CMCS’00, Elective Notes in Theoretical Computer Science, Vol. 33, Elsevier, Amsterdam, 2000, pp. 61-79.; S. Buss, G. Roşu, Incompleteness of behavioral logics, in: Proc. CMCS’00, Elective Notes in Theoretical Computer Science, Vol. 33, Elsevier, Amsterdam, 2000, pp. 61-79.
[11] C. Cîrstea, Coalgebra semantics for hidden algebra: parameterized objects and inheritance, in: F. Parisi-Presicce (Ed.), Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science, Vol. 1376, Springer, Berlin, 1998.; C. Cîrstea, Coalgebra semantics for hidden algebra: parameterized objects and inheritance, in: F. Parisi-Presicce (Ed.), Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science, Vol. 1376, Springer, Berlin, 1998.
[12] C. Cîrstea, A coequational approach to specifying behaviours, in: Proc. CMCS’99, Elective Notes in Theoretical Computer Science, Vol. 19, Elsevier, Amsterdam, 1999.; C. Cîrstea, A coequational approach to specifying behaviours, in: Proc. CMCS’99, Elective Notes in Theoretical Computer Science, Vol. 19, Elsevier, Amsterdam, 1999.
[13] C. Cîrstea, Semantic constructions for hidden algebra, in: J. Luiz-Fiadeiro (Ed.), Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science, Vol. 1589, Springer, Berlin, 1999.; C. Cîrstea, Semantic constructions for hidden algebra, in: J. Luiz-Fiadeiro (Ed.), Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science, Vol. 1589, Springer, Berlin, 1999.
[14] Clavel, M.; Durán, F. J.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J. F., Maudespecification and programming in rewriting logic, Theoret. Comput. Sci., 285, 187-243 (2002) · Zbl 1001.68059
[15] M. Clavel, S. Eker, P. Lincoln, J. Meseguer, Principles of Maude, in: Proc. WRLA, Elective Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, 1996.; M. Clavel, S. Eker, P. Lincoln, J. Meseguer, Principles of Maude, in: Proc. WRLA, Elective Notes in Theoretical Computer Science, Vol. 4, Elsevier, Amsterdam, 1996. · Zbl 0912.68095
[16] A. Corradini, R. Heckel, U. Montanari, From SOS specifications to structured coalgebras: how to make bisimulation a congruence, in: Proc. CMCS’99, Elective Notes in Theoretical Computer Science, Vol. 19, Elsevier, Amsterdam, 1999.; A. Corradini, R. Heckel, U. Montanari, From SOS specifications to structured coalgebras: how to make bisimulation a congruence, in: Proc. CMCS’99, Elective Notes in Theoretical Computer Science, Vol. 19, Elsevier, Amsterdam, 1999. · Zbl 0918.68065
[17] R. Diaconescu, K. Futatsugi, CafeOBJ Report, AMAST Series in Computing, Vol. 6, World Scientific, Singapore, 1998.; R. Diaconescu, K. Futatsugi, CafeOBJ Report, AMAST Series in Computing, Vol. 6, World Scientific, Singapore, 1998.
[18] Diaconescu, R.; Futatsugi, K., Behavioral coherence in object-oriented algebraic specification, J. Universal Comput. Sci., 6, 1, 74-96 (2000) · Zbl 0963.68104
[19] R. Diaconescu, J. Goguen, P. Stefaneas, Logical support for modularization, in: G. Huet, G. Plotkin (Eds.), Logical Environments, Cambridge, 1993, pp. 83-130.; R. Diaconescu, J. Goguen, P. Stefaneas, Logical support for modularization, in: G. Huet, G. Plotkin (Eds.), Logical Environments, Cambridge, 1993, pp. 83-130.
[20] V. Giarrantana, F. Gimona, U. Montanari, Observability concepts in abstract data specifications, in: Proc. MFCS, Lecture Notes in Computer Science, Vol. 45, Springer, Berlin, 1976.; V. Giarrantana, F. Gimona, U. Montanari, Observability concepts in abstract data specifications, in: Proc. MFCS, Lecture Notes in Computer Science, Vol. 45, Springer, Berlin, 1976. · Zbl 0338.68023
[21] J. Goguen, Types as theories, in: G.M. Reed, A.W. Roscoe, R.F. Wachter (Eds.), Topology and Category Theory in Computer Science, Oxford, 1991, pp. 357-390.; J. Goguen, Types as theories, in: G.M. Reed, A.W. Roscoe, R.F. Wachter (Eds.), Topology and Category Theory in Computer Science, Oxford, 1991, pp. 357-390. · Zbl 0792.68100
[22] Goguen, J.; Burstall, R., Institutionsabstract model theory for specification and programming, J. Assoc. Comput. Mach., 39, 1, 95-146 (1992) · Zbl 0799.68134
[23] J. Goguen, R. Diaconescu, Towards an algebraic semantics for the object paradigm, in: Proc. WADT, Lecture Notes in Computer Science, Vol. 785, Springer, Berlin, 1994.; J. Goguen, R. Diaconescu, Towards an algebraic semantics for the object paradigm, in: Proc. WADT, Lecture Notes in Computer Science, Vol. 785, Springer, Berlin, 1994. · Zbl 0941.68637
[24] Goguen, J.; Lin, K.; Roşu, G., Circular coinductive rewriting, (Proc. Automated Software Engineering 2000, IEEE, New York (2000)), 123-131
[25] J. Goguen, K. Lin, G. Roşu, Behavioral and coinductive rewriting, in: Proc. WRLA’01, Elective Notes in Theoretical Computer Science, Vol. 36, Elsevier, Amsterdam, 2001, pp. 1-22.; J. Goguen, K. Lin, G. Roşu, Behavioral and coinductive rewriting, in: Proc. WRLA’01, Elective Notes in Theoretical Computer Science, Vol. 36, Elsevier, Amsterdam, 2001, pp. 1-22. · Zbl 0962.68078
[26] Goguen, J.; Malcolm, G., Hidden coinductionbehavioral correctness proofs for objects, Math. Struct. Comput. Sci., 9, 3, 287-319 (1999) · Zbl 0931.68067
[27] Goguen, J.; Malcolm, G., A hidden agenda, J. Theoret. Comput. Sci., 245, 1, 55-101 (2000) · Zbl 0946.68070
[28] J. Goguen, J. Meseguer, Universal realization, persistent interconnection and implementation of abstract modules, in: Proc. ICALP, Lecture Notes in Computer Science, Vol. 140, Springer, Berlin, 1982, pp. 265-281.; J. Goguen, J. Meseguer, Universal realization, persistent interconnection and implementation of abstract modules, in: Proc. ICALP, Lecture Notes in Computer Science, Vol. 140, Springer, Berlin, 1982, pp. 265-281. · Zbl 0493.68014
[29] J. Goguen, G. Roşu, Hiding more of hidden algebra, in: Proc. FM’99, Lecture Notes in Computer Science, Vol. 1709, Springer, Berlin, 1999, pp. 1704-1719.; J. Goguen, G. Roşu, Hiding more of hidden algebra, in: Proc. FM’99, Lecture Notes in Computer Science, Vol. 1709, Springer, Berlin, 1999, pp. 1704-1719. · Zbl 0953.68094
[30] Goguen, J.; Roşu, G., Institution morphisms, Formal Aspects Comput., 13, 3-5, 274-307 (2002) · Zbl 1001.68019
[31] Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J.-P., Introducing OBJ, (Goguen, J.; Malcolm, G., Software Engineering with OBJ: Algebraic Specification in Action (2000), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht, The Netherlands), 3-167
[32] Groote, J. F.; Vaandrager, F. W., Structured operational semantics and bisimulation as a congruence, Inform. and Comput., 100, 2, 202-260 (1992) · Zbl 0752.68053
[33] Hennicker, R., Context inductiona proof principle for behavioral abstractions, Formal Aspects Comput., 3, 4, 326-345 (1991) · Zbl 0739.68060
[34] R. Hennicker, M. Bidoit, Observational logic, in: Proc. AMAST’98, Lecture Notes in Computer Science, Vol. 1548, Springer, Berlin, 1999, pp. 263-277.; R. Hennicker, M. Bidoit, Observational logic, in: Proc. AMAST’98, Lecture Notes in Computer Science, Vol. 1548, Springer, Berlin, 1999, pp. 263-277. · Zbl 1088.68112
[35] Jacobs, B.; Rutten, J., A tutorial on (co)algebras and (co)induction, Bull. European Assoc. Theoret. Comput. Sci., 62, 222-259 (1997) · Zbl 0880.68070
[36] A. Kurz, Specifying coalgebras with modal logic, in: Proc. CMCS’98, Elective Notes in Theoretical Computer Science, Vol. 11, Elsevier, Amsterdam, 1998.; A. Kurz, Specifying coalgebras with modal logic, in: Proc. CMCS’98, Elective Notes in Theoretical Computer Science, Vol. 11, Elsevier, Amsterdam, 1998. · Zbl 0917.68134
[37] D. Lucanu, O. Gheorghieş, A. Apetreim, Bisimulation and hidden algebra, in: Proc. CMCS’99, Elective Notes in Theoretical Computer Science, Vol. 19, Elsevier, Amsterdam, 1999, pp. 213-232.; D. Lucanu, O. Gheorghieş, A. Apetreim, Bisimulation and hidden algebra, in: Proc. CMCS’99, Elective Notes in Theoretical Computer Science, Vol. 19, Elsevier, Amsterdam, 1999, pp. 213-232.
[38] M. Majster, Limits of the algebraic specification of abstract data types, SIGPLAN Notices, October 1977, pp. 37-42.; M. Majster, Limits of the algebraic specification of abstract data types, SIGPLAN Notices, October 1977, pp. 37-42.
[39] J. Meseguer, J. Goguen, Initiality, induction and computability, in: M. Nivat, J.C. Reynolds (Eds.), Algebraic Methods in Semantics, Cambridge, 1985, pp. 459-541.; J. Meseguer, J. Goguen, Initiality, induction and computability, in: M. Nivat, J.C. Reynolds (Eds.), Algebraic Methods in Semantics, Cambridge, 1985, pp. 459-541.
[40] Mikami, S., Semantics of equational specifications with module import and verification method of behavioral equations, (Proc. CafeOBJ Symposium, Japan Advanced Institute for Science and Technology (1998))
[41] T. Mossakowski, H. Reichel, M. Roggenbach, L. Schroder, Algebraic-coalgebraic specification in CoCASL, in: Proc. WADT’02, Lecture Notes in Computer Science, Vol. 2755, Springer, Berlin,. 2002, pp. 376-392.; T. Mossakowski, H. Reichel, M. Roggenbach, L. Schroder, Algebraic-coalgebraic specification in CoCASL, in: Proc. WADT’02, Lecture Notes in Computer Science, Vol. 2755, Springer, Berlin,. 2002, pp. 376-392. · Zbl 1278.68209
[42] P. Padawitz, Swinging data types: syntax, semantics, and theory, in: Proc. WADT’95, Lecture Notes in Computer Science, Vol. 1130, Springer, Berlin, 1996, pp. 409-435.; P. Padawitz, Swinging data types: syntax, semantics, and theory, in: Proc. WADT’95, Lecture Notes in Computer Science, Vol. 1130, Springer, Berlin, 1996, pp. 409-435.
[43] P. Padawitz, Towards the one-tiered design of data types and transition systems, in: Proc. WADT’97, Lecture Notes in Computer Science, Vol. 1376, Springer, Berlin, 1998, pp. 365-380.; P. Padawitz, Towards the one-tiered design of data types and transition systems, in: Proc. WADT’97, Lecture Notes in Computer Science, Vol. 1376, Springer, Berlin, 1998, pp. 365-380.
[44] Padawitz, P., Swinging types = functions + relations + transition systems, Theoret. Comput. Sci., 243, 93-165 (2000) · Zbl 0947.68098
[45] Parnas, D., Information distribution aspects of design methodology, Inform. Process., 71, 339-344 (1972)
[46] Reichel, H., Behavioural equivalence—a unifying concept for initial and final specifications, (Proc. Third Hungarian Computer Science Conf. (1981), Akademiai Kiado: Akademiai Kiado Budapest, Hungary) · Zbl 0479.68017
[47] Reichel, H., Behavioural validity of conditional equations in abstract data types, (Contributions to General Algebra, Vol. 3 (1985), Teubner: Teubner Stuttgart) · Zbl 0616.68020
[48] G. Roşu, Hidden logic, Ph.D. Thesis, University of California at San Diego, 2000.; G. Roşu, Hidden logic, Ph.D. Thesis, University of California at San Diego, 2000.
[49] Roşu, G., Equational axiomatizability for coalgebra, Theoret. Comput. Sci., 260, 1-2, 229-247 (2001) · Zbl 0973.68176
[50] Roşu, G., On implementing behavioral rewriting, (Proc. ACM SIGPLAN RULE’02 (2002), ACM Press: ACM Press New York), 43-52
[51] G. Roşu, J. Goguen, Hidden congruent deduction, in: Automated Deduction in Classical and Non-Classical Logics, Lecture Notes in Artificial Intelligence, Vol. 1761, Springer, Berlin, 2000.; G. Roşu, J. Goguen, Hidden congruent deduction, in: Automated Deduction in Classical and Non-Classical Logics, Lecture Notes in Artificial Intelligence, Vol. 1761, Springer, Berlin, 2000.
[52] G. Roşu, J. Goguen, Circular coinduction, in: Internat. Joint Conf. on Automated Reasoning (IJCAR’01) 2001, Short paper, An extended version appeared as UCSD Technical Report CSE2000-0647.; G. Roşu, J. Goguen, Circular coinduction, in: Internat. Joint Conf. on Automated Reasoning (IJCAR’01) 2001, Short paper, An extended version appeared as UCSD Technical Report CSE2000-0647.
[53] Rothe, J.; Jacobs, B.; Tews, H., The coalgebraic class specification language CCSL, J. Universal Comput. Sci., 7, 175-193 (2001) · Zbl 0970.68104
[54] Sannella, D.; Tarlecki, A., On observational equivalence and algebraic specification, J. Comput. Syst. Sci., 34, 150-178 (1987) · Zbl 0619.68028
[55] H. Tews, Coalgebras for binary methods, in: Proc. CMCS’00, Elective Notes in Theoretical Computer Science, Vol. 33, Elsevier, Amsterdam, 2000.; H. Tews, Coalgebras for binary methods, in: Proc. CMCS’00, Elective Notes in Theoretical Computer Science, Vol. 33, Elsevier, Amsterdam, 2000. · Zbl 0966.68049
[56] Tews, H., Coalgebras for binary methodsproperties of bisimulations and invariants, Theoret. Inform. Appl., 35, 1, 83-111 (2001) · Zbl 0983.68126
[57] H. Tews, Greatest bisimulations for binary methods, in: Proc. CMCS’02, Elective Notes in Theoretical Computer Science, Vol. 65(1), Elsevier, Amsterdam, 2002.; H. Tews, Greatest bisimulations for binary methods, in: Proc. CMCS’02, Elective Notes in Theoretical Computer Science, Vol. 65(1), Elsevier, Amsterdam, 2002. · Zbl 1270.68228
[58] Walicki, M.; Meldal, S., Algebraic approaches to nondeterminisman overview, ACM Comput. Surveys, 29, 30-81 (1997)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.