×

zbMATH — the first resource for mathematics

Constructor-based observational logic. (English) Zbl 1088.68112
Summary: This paper focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework. In the first part of this work, we develop the essential ingredients that are needed to define the constructor-based observational logic institution, called COL, which takes into account both the generation- and observation-oriented aspects of software systems. The underlying paradigm of our approach is that the semantics of a specification should be as loose as possible to capture all its correct realizations. We also consider the “black box” semantics of a specification which is useful to study the behavioral properties a user can observe when he/she is experimenting with the system.
In the second part of this work, we develop proof techniques for structured COL-specifications. For this purpose we introduce an institution encoding from the COL institution to the institution of many-sorted first-order logic with equality and sort-generation constraints. Using this institution encoding, we can then reduce proofs of consequences of structured specifications built over COL to proofs of consequences of structured specifications written in a simple subset of the algebraic specification language Casl. This means, in particular, that any inductive theorem prover, such as e.g. the Larch Prover or PVS, can be used to prove theorems over structured COL-specifications.

MSC:
68Q65 Abstract data types; algebraic specification
03B70 Logic in computer science
Software:
PVS; CafeOBJ; LARCH
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Astesiano, E.; Bidoit, M.; Kirchner, H.; Krieg-Brückner, B.; Mosses, P.D.; Sannella, D.; Tarlecki, A., C{\scasl}: the common algebraic specification language, Theor. comput. sci., 286, 2, 153-196, (2002) · Zbl 1061.68103
[2] ()
[3] M. Bidoit, M.V. Cengarle, R. Hennicker, Proof systems for structured specifications and their refinements, in: [2], Springer, 1999, pp. 385-433 (chapter 11). · Zbl 0948.68118
[4] Bidoit, M.; Hennicker, R., Behavioural theories and the proof of behavioural properties, Theor. comput. sci., 165, 1, 3-55, (1996) · Zbl 0872.68167
[5] M. Bidoit, R. Hennicker, Observer complete definitions are behaviourally coherent, in: Proc. OBJ/CafeOBJ/Maude Workshop at Formal Methods’99, Toulouse, France, September 1999, pp. 83-94. THETA, 1999. Preliminary long version available as Report LSV-99-4 at www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-1999-4.rr.ps.
[6] Bidoit, M.; Hennicker, R., On the integration of observability and reachability concepts, (), 21-36 · Zbl 1077.68709
[7] Bidoit, M.; Hennicker, R.; Kurz, A., On the duality between observability and reachability, (), 72-87 · Zbl 0986.68018
[8] Bidoit, M.; Hennicker, R.; Kurz, A., Observational logic, constructor-based logic, and their duality, Theor. comput. sci., 298, 3, 471-510, (2003) · Zbl 1038.68079
[9] Bidoit, M.; Hennicker, R.; Wirsing, M., Behavioural and abstractor specifications, Sci. comput. program., 25, 2-3, 149-186, (1995) · Zbl 0853.68130
[10] Bidoit, M.; Mosses, P.D., ()
[11] Bidoit, M.; Sannella, D.; Tarlecki, A., Architectural specifications in C{\scasl}, Formal aspects comput., 13, 3-5, 252-273, (2002) · Zbl 1001.68078
[12] Borzyszkowski, T., Logical systems for structured specifications, Theor. comput. sci., 286, 2, 197-245, (2002) · Zbl 1061.68104
[13] Diaconescu, R.; Futatsugi, K., Cafeobj report: the language, proof techniques, and methodologies for object-oriented algebraic specification, AMAST series in computing, vol. 6, (1998), World Scientific · Zbl 0962.68115
[14] Ehrig, H.; Mahr, B., Algebraic specification I, (1985), Springer · Zbl 0557.68013
[15] Goguen, J.; Roşu, G., Hiding more of hidden algebra, (), 1704-1719 · Zbl 0953.68094
[16] Goguen, J.; Burstall, R., Institutions: abstract model theory for specification and programming, J. ACM, 39, 1, 95-146, (1992) · Zbl 0799.68134
[17] Goguen, J.; Lin, K.; Roşu, G., Circular coinductive rewriting, (), 123-132
[18] Goguen, J.; Roşu, G., Institution morphisms, Formal aspects comput., 13, 3-5, 274-307, (2002) · Zbl 1001.68019
[19] Guttag, J.V.; Horning, J.J., Larch: languages and tools for formal specification, (1993), Springer · Zbl 0794.68103
[20] Hennicker, R., Context induction: a proof principle for behavioural abstraction and algebraic implementations, Formal aspects comput., 3, 4, 326-345, (1991) · Zbl 0739.68060
[21] Hennicker, R.; Bidoit, M., Observational logic, (), 263-277
[22] Hoare, C.A.R., Proofs of correctness of data representations, Acta inform., 1, 271-281, (1972) · Zbl 0244.68009
[23] Hofmann, M.; Sannella, D., On behavioural abstraction and behavioural satisfaction in higher-order logic, Theor. comput. sci., 167, 3-45, (1996) · Zbl 0874.68196
[24] Keisler, H.J., Model theory for infinitary logic, (1971), North-Holland · Zbl 0222.02064
[25] Loeckx, J.; Ehrich, H.-D.; Wolf, M., Specification of abstract data types, (1996), Wiley and Teubner · Zbl 0868.68077
[26] Mossakowski, T.; Reichel, H.; Roggenbach, M.; Schröder, L., Algebraic-coalgebraic specification in C{\sco}C{\scasl}, (), 376-392 · Zbl 1278.68209
[27] Mossakowski, T., Relating C{\scasl} with other specification languages: the institution level, Theor. comput. sci., 286, 2, 367-475, (2002) · Zbl 1061.68106
[28] ()
[29] Nivela, M.P.; Orejas, F., Initial behaviour semantics for algebraic specifications, (), 184-207 · Zbl 0679.68026
[30] Owre, S.; Rushby, J.; Shankar, N.; Stringer-Calvert, D., PVS: an experience report, (), 338-345
[31] Padawitz, P., Swinging data types: syntax, semantics, and theory, (), 409-435
[32] P. Padawitz, Basic inference rules for algebraic and coalgebraic specifications, Technical report, September 2002. Available from: <http://ls5-www.cs.uni-dortmund.de/peter/WADT01.ps.gz>.
[33] H. Reichel, Behavioural validity of conditional equations in abstract data types, in: Proc. of the Vienna Conference, June 1984, Contributions to General Algebra 3, Verlag B.G. Teubner, 1985, pp. 301-324.
[34] Rosu, G., Inductive behavioral proofs by unhiding, () · Zbl 1270.68196
[35] Sannella, D.; Tarlecki, A., On observational equivalence and algebraic specification, J. comput. syst. sci., 34, 150-178, (1987) · Zbl 0619.68028
[36] Sannella, D.; Tarlecki, A., Specifications in an arbitrary institution, Inform. comput., 76, 165-210, (1988) · Zbl 0654.68017
[37] A. Tarlecki, Institutions: an abstract framework for formal specification, in: [2], Springer, 1999, pp. 105-130 (chapter 4). · Zbl 0945.68130
[38] Tarlecki, A., Towards heterogeneous specifications, (), 337-360 · Zbl 0988.03056
[39] Wirsing, M., Algebraic specification, (), 676-788, (chapter 13) · Zbl 0900.68309
[40] Wirsing, M.; Broy, M., A modular framework for specification and information, (), 42-73
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.