×

Proof systems for structured specifications with observability operators. (English) Zbl 0901.68116

Summary: An ASL-like kernel language for structured specifications is presented which contains observability operators for determining the observable behaviour, the observational quotient and, as a derived operator, the observational abstraction of a specification. Sound and complete infinitary proof systems for first-order properties of specifications and for proving implementation relations between specifications are provided. The relationships to approaches based on an observational satisfaction relation are discussed.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

LARCH; OBSCURE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Astesiano, E.; Giovini, A.; Reggio, G., Observational structures and their logic, Theoret. Comput. Sci., 96, 249-283 (1992) · Zbl 0756.68073
[2] Astesiano, E.; Reggio, G.; Wirsing, M., Relational specifications and observational semantics, (Gruska, I.; Rovan, B.; Wiedermann, J., Proc. MFCS’86 Mathematical Foundations of Computer Science. Proc. MFCS’86 Mathematical Foundations of Computer Science, Bratislava. Proc. MFCS’86 Mathematical Foundations of Computer Science. Proc. MFCS’86 Mathematical Foundations of Computer Science, Bratislava, Lecture Notes in Computer Science, Vol. 233 (1986), Springer: Springer Berlin), 209-217 · Zbl 0637.68012
[3] Barwise, K. J., (Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, Vol. 90 (1977), North-Holland: North-Holland Amsterdam)
[4] Bauer, F. L.; Berghammer, R.; Broy, M.; Dosch, W.; Geiselbrechtinger, F.; Gnatz, R.; Hangel, E.; Hesse, W.; Krieg-Brückner, B.; Laut, A.; Matzner, T.; Möller, B.; Nickl, F.; Partsch, H.; Pepper, P.; Samelson, K.; Wirsing, M.; Wössner, H., The Munich Project CIP, Vol. 1: The Wide Spectrum language CIP-L, (Lecture Notes in Computer Science, Vol. 183 (1985), Springer: Springer Berlin) · Zbl 0469.68003
[5] Bernot, G.; Bidoit, M., Proving the correctness of algebraically specified software: modularity and observability issues, (Proc. AMAST ’91, Springer Workshops in Computing Series (1992)), 216-242
[6] Bidoit, M.; Choppy, C., Asspegique: an integrated environment for algebraic specifications, (Proc. TAPSOFT ’85, 1st Internat. Joint Conf. on Theory and Practice of Software Development. Proc. TAPSOFT ’85, 1st Internat. Joint Conf. on Theory and Practice of Software Development, Lecture Notes in Computer Science, Vol. 186 (1985), Springer: Springer Berlin), 246-260
[7] Bidoit, M.; Gaudel, M.-C.; Mauboussin, A., How to make algebraic specifications more understandable? An experiment with the PLUSS specification language, Sci. Comput. Programming, 12, 1-38 (1989) · Zbl 0678.68011
[8] Bidoit, M.; Hennicker, R., Behavioural theories and the proof of behavioural properties, Theoret. Comput. Sci., 175, 3-55 (1996) · Zbl 0872.68167
[9] Bidoit, M.; Hennicker, R., Proving the correctness of behavioural implementations, (Proc. AMAST ’95. Proc. AMAST ’95, Lecture Notes in Computer Science, Vol. 936 (1995), Springer: Springer Berlin), 152-168 · Zbl 0988.03525
[10] Bidoit, M.; Hennicker, R.; Wirsing, M., Behavioural and abstractor specifications, Sci. Comput. Programming, 25, 149-186 (1995) · Zbl 0853.68130
[11] Broy, M.; Facchi, C.; Grosu, R.; Hettler, R.; Huβmann, H.; Nazareth, D.; Regensburger, F.; Slotosch, O.; Stølen, K., The requirement and design specification language SPECTRUM: an informal introduction, TU München, Tech. Rep. TUM-I9311 (1993), Version 1.0, Part I
[12] Burstall, R. M.; Goguen, J. A., The semantics of CLEAR, a specification language, (Proc. Advanced Course on Abstract Software Specifications. Proc. Advanced Course on Abstract Software Specifications, Lecture Notes in Computer Science, Vol. 86 (1980), Springer: Springer Berlin), 292-332 · Zbl 0456.68024
[13] Cengarle, M. V., Formal Specifications with Higher-Order Parameterization (1995), Verlag Shaker: Verlag Shaker Aachen
[14] Chang, C. C.; Keisler, H. J., Model Theory (1990), North-Holland: North-Holland Amsterdam · Zbl 0697.03022
[15] Dershowitz, N.; Jouannaud, J. P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), North-Holland: North-Holland Amsterdam), 243-320 · Zbl 0900.68283
[16] Ehrig, H.; Baldamus, M.; Cornelius, F.; Orejas, F., Theory of algebraic module specification including behavioural semantics, constraints, and aspects of generalized morphisms, (Proc. AMAST ’91, Springer Workshops in Computing Series (1992))
[17] Ehrig, H.; Kreowski, H. J.; Mahr, B.; Padawitz, P., Algebraic implementation of abstract data types, Theoret. Comput. Sci., 20, 209-263 (1982) · Zbl 0483.68018
[18] Ehrig, H.; Mahr, B., Fundamentals of Algebraic Specification 1, (EATCS Monographs on Theoretical Computer Science, Vol. 6 (1985), Springer: Springer Berlin) · Zbl 0557.68013
[19] Ehrig, H.; Mahr, B., Fundamentals of Algebraic Specification 2, (EATCS Monographs on Theoretical Computer Science, Vol. 21 (1990), Springer: Springer Berlin) · Zbl 0557.68013
[20] Farrés-Casals, J., Verification in ASL and related specification languages, (Report CST-92-92. Report CST-92-92, Ph.D. thesis (1992), University of Edinburgh)
[21] Futatsugi, K.; Goguen, J. A.; Jouannaud, J. P.; Meseguer, J., Principles of OBJ2, (Proc. 12th ACM Symp. on Principles of Programming Languages. Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans (1985)), 52-66
[22] Gaudel, M.-C., Structuring and modularizing algebraic specifications: the PLUSS specification language, evolutions and perspectives, (Proc. STACS ’92, 9th Symp. on Theoretical Aspects of Computer Science. Proc. STACS ’92, 9th Symp. on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, Vol. 577 (1992), Springer: Springer Berlin), 3-23 · Zbl 1493.68229
[23] Geser, A.; Huβmann, H., Experiences with the RAP system — a specification interpreter combining term rewriting and resolution, (Robinet, B.; Wilhelm, R., Proc. ESOP ’86, Europ. Symp. on Programming. Proc. ESOP ’86, Europ. Symp. on Programming, Lecture Notes in Computer Science, Vol. 213 (1986), Springer: Springer Berlin), 339-350
[24] Goguen, J. A.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (Proc. ICALP ’82. Proc. ICALP ’82, Lecture Notes in Computer Science, Vol. 140 (1982), Springer: Springer Berlin), 265-281 · Zbl 0493.68014
[25] (Guttag, J. V.; Horning, J. J., Larch: Languages and Tools for Formal Specification. Larch: Languages and Tools for Formal Specification, Texts and Monographs in Computer Science (1993), Springer: Springer Berlin) · Zbl 0794.68103
[26] Harper, R.; Sannella, D. T.; Tarlecki, A., Structure and representation in LF, (Proc. 4th IEEE Symp. on Logic in Computer Science. Proc. 4th IEEE Symp. on Logic in Computer Science, Asilomar (1989)), 226-237
[27] Harper, R.; Sannella, D. T.; Tarlecki, A., Structured theory presentations and logic representations, Ann. Pure Appl. Logic, 67, 113-160 (1994) · Zbl 0809.03019
[28] Hennicker, R., Context induction: a proof principle for behavioural abstractions and algebraic implementations, Formal Aspects Comput., 3, 326-345 (1991) · Zbl 0739.68060
[29] Hennicker, R.; Nickl, F., A behavioural algebraic framework for modular system design with reuse, (Ehrig, H.; Orejas, F., Proc. 9th Workshop on Algebraic Specification of Abstract Data Types joint with 4th COMPASS Workshop. Proc. 9th Workshop on Algebraic Specification of Abstract Data Types joint with 4th COMPASS Workshop, Caldes de Malavella. Proc. 9th Workshop on Algebraic Specification of Abstract Data Types joint with 4th COMPASS Workshop. Proc. 9th Workshop on Algebraic Specification of Abstract Data Types joint with 4th COMPASS Workshop, Caldes de Malavella, Lecture Notes in Computer Science, Vol. 785 (1993), Springer: Springer Berlin), 220-234
[30] Hennicker, R.; Wirsing, M., Behavioural specifications, (Proof and Computation, International Summer School Marktoberdorf. Proof and Computation, International Summer School Marktoberdorf, NATO ASI Series F, Vol. 139 (1993), Springer: Springer Berlin), 193-230 · Zbl 0831.68061
[31] Hoare, C. A.R., Proofs of correctness of data representations, Acta Inform., 1, 271-281 (1972) · Zbl 0244.68009
[32] Hofmann, M.; Sannella, D. T., (Proc. TAPSOFT ’95. Proc. TAPSOFT ’95, Lecture Notes in Computer Science, Vol. 915 (1995), University of Edinburgh: University of Edinburgh Berlin), 247-261, A short version appeared · Zbl 0874.68196
[33] Jonkers, H. B.M., An introduction to COLD-K, (Bergstra, J. A.; Wirsing, M., Algebraic Methods: Theory, Tools and Applications. Algebraic Methods: Theory, Tools and Applications, Lecture Notes in Computer Science, Vol. 394 (1989), Springer: Springer Berlin), 139-205 · Zbl 0513.68008
[34] Kahrs, S.; Sannella, D. T.; Tarlecki, A., The semantics of Extended ML: a gentle introduction, Theoret. Comput. Sci. (1996), in this volume
[35] Kreisel, G.; Krivine, J. L., Eléments de Logique Mathématique (1967), Dunod: Dunod Paris · Zbl 0146.00703
[36] Lehmann, T.; Loeckx, J., The specification language of OBSCURE, (Sannella, D. T.; Tarlecki, A., Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types. Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types, 1987. Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types. Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types, 1987, Lecture Notes in Computer Science, Vol. 332 (1988), Springer: Springer Berlin), 131-153 · Zbl 0663.68024
[37] Malcolm, G.; Goguen, J. A., Proving correctness of refinement and implementation, (Technical Monograph PRG-114 (1994), Oxford University Computing Laboratory)
[38] Milner, R., Fully abstract models of typed λ-calculi, (Theoret. Comput. Sci., 4 (1977), Springer: Springer Berlin), 1-22 · Zbl 0386.03006
[39] Nivela, P.; Orejas, F., Initial behaviour semantics for algebraic specifications, (Sannella, D. T.; Tarlecki, A., Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types. Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types, 1987. Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types. Recent Trends in Data Type Specification, 5th Workshop on Specification of Abstract Data Types, 1987, Lecture Notes in Computer Science, Vol. 332 (1988), Springer: Springer Berlin), 184-207 · Zbl 0679.68026
[40] Orejas, F.; Navarro, M.; Sanchez, A., Implementation and behavioural equivalence: a survey, (Bidoit, M.; Choppy, C., Recent Trends in Data Type Specification. Recent Trends in Data Type Specification, Lecture Notes in Computer Science, Vol. 655 (1991), Springer: Springer Berlin), 93-125
[41] Orejas, F.; Nivela, M. P., Constraints for behavioural specifications, (Ehrig, H.; Jantkc, K. P.; Orejas, F.; Reichel, H., Recent Trends in Data Type Specification, Proc. 7th Workshop on Specification of Abstract Data Types. Recent Trends in Data Type Specification, Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen/Dosse. Recent Trends in Data Type Specification, Proc. 7th Workshop on Specification of Abstract Data Types. Recent Trends in Data Type Specification, Proc. 7th Workshop on Specification of Abstract Data Types, Wusterhausen/Dosse, Lecture Notes in Computer Science, Vol. 534 (1990), Springer: Springer Berlin), 220-245
[42] Reichel, H., Behavioural equivalence — a unifying concept for initial and final specification methods, (Arato, M.; Varga, L., Math. Models in Comp. Systems, Proc. 3rd Hungarian Computer Science Conf.. Math. Models in Comp. Systems, Proc. 3rd Hungarian Computer Science Conf., Budapest (1981), Springer: Springer Berlin), 27-39 · Zbl 0479.68017
[43] Reichel, H., Initial restrictions of behaviour, (IFIP Working Conf.. IFIP Working Conf., The Role of Abstract Models in Information Processing (1985)) · Zbl 0594.68013
[44] Reichel, H., Initial computability, algebraic specifications, and partial algebras, (International Series of Monographs in Computer Science, Vol. 2 (1987), Clarendon Press: Clarendon Press Oxford) · Zbl 0634.68001
[45] Sannella, D. T.; Burstall, R. M., Structured theories in LCF, (Ausiello, G.; Protasi, M., 8th CAAP. 8th CAAP, L’Aquila. 8th CAAP. 8th CAAP, L’Aquila, Lecture Notes in Computer Science, Vol. 159 (1983), Springer: Springer Berlin), 377-391 · Zbl 0527.68070
[46] Sannella, D. T.; Tarlecki, A., On observational equivalence and algebraic specification, J. Comput. System Sci., 34, 150-178 (1987) · Zbl 0619.68028
[47] Sannella, D. T.; Tarlecki, A., Toward formal development of programs from algebraic specifications: implementation revisited, Acta Inform., 25, 233-281 (1988) · Zbl 0621.68004
[48] Sannella, D. T.; Tarlecki, A., Specifications in an arbitrary institution, Inform. Comput., 76, 165-210 (1988) · Zbl 0654.68017
[49] Sannella, D. T.; Tarlecki, A., Toward formal development of ML programs: foundations and methodology, (Diaz, J.; Orejas, F., Proc. TAPSOFT ’89. Proc. TAPSOFT ’89, Lecture Notes in Computer Science, Vol. 352 (1989)), 375-389
[50] Sannella, D. T.; Wirsing, M., A kernel language for algebraic specifications and implementation, (Karpinski, M., Proc. FCT ’83. Proc. FCT ’83, Lecture Notes in Computer Science, Vol. 158 (1983), Springer: Springer Berlin), 413-427
[51] Schoett, O., Data abstraction and the correctness of modular programming, (CST-42-87. CST-42-87, Ph.D. Thesis (1987), Department of Computer Science, University of Edinburgh)
[52] Schoett, O., Behavioural correctness of data representation, Sci. Comput. Programming, 14, 43-57 (1990) · Zbl 0699.68031
[53] Schoett, O., Two impossibility theorems on behavioural specification of abstract data types, Acta Informatica, 29, 595-621 (1992) · Zbl 0790.68080
[54] Wirsing, M., Structured algebraic specifications: a kernel language, Theoret. Comput. Sci., 42, 123-249 (1986) · Zbl 0599.68021
[55] Wirsing, M., Algebraic specification, (van Leeuwen, J., Handbook of Theoretical Computer Science (1990), North-Holland: North-Holland Amsterdam), 675-788 · Zbl 0900.68309
[56] Wirsing, M., Structured specifications: syntax, semantics and proof calculus, (Bauer, F. L.; Brauer, W.; Schwichtenberg, H., Logic and Algebra of Specification, International Summer School Marktoberdorf (1993), Springer: Springer Berlin), 411-442, 1991
[57] Wolter, U., The power of behavioural validity, (Preprint 1-87 (1987), TU Magdeburg, Sektion Mathematik)
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.