×

zbMATH — the first resource for mathematics

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
PDF BibTeX XML Cite
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, (), 209-217
[3] Barwise, K.J., ()
[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, () · Zbl 0469.68003
[5] Bernot, G.; Bidoit, M., Proving the correctness of algebraically specified software: modularity and observability issues, (), 216-242
[6] Bidoit, M.; Choppy, C., Asspegique: an integrated environment for algebraic specifications, (), 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.; Bidoit, M.; Hennicker, R., Proving the correctness of behavioural implementations, (), 152-168, (1995), Available by · 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, (), 292-332 · Zbl 0456.68024
[13] Cengarle, M.V., Formal specifications with higher-order parameterization, (1995), Verlag Shaker Aachen
[14] Chang, C.C.; Keisler, H.J., Model theory, (1990), North-Holland Amsterdam · Zbl 0697.03022
[15] Dershowitz, N.; Jouannaud, J.P., Rewrite systems, (), 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, ()
[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, () · Zbl 0557.68013
[19] Ehrig, H.; Mahr, B., Fundamentals of algebraic specification 2, () · Zbl 0557.68013
[20] Farrés-Casals, J., Verification in ASL and related specification languages, ()
[21] Futatsugi, K.; Goguen, J.A.; Jouannaud, J.P.; Meseguer, J., Principles of OBJ2, (), 52-66
[22] Gaudel, M.-C., Structuring and modularizing algebraic specifications: the PLUSS specification language, evolutions and perspectives, (), 3-23
[23] Geser, A.; Huβmann, H., Experiences with the RAP system — a specification interpreter combining term rewriting and resolution, (), 339-350
[24] Goguen, J.A.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (), 265-281 · Zbl 0493.68014
[25] ()
[26] Harper, R.; Sannella, D.T.; Tarlecki, A., Structure and representation in LF, (), 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, (), 220-234
[30] Hennicker, R.; Wirsing, M., Behavioural specifications, (), 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.; Hofmann, M.; Sannella, D.T., On behavioural abstraction and behavioural satisfaction in higher-order logic, (), 247-261, A short version appeared · Zbl 0874.68196
[33] Jonkers, H.B.M., An introduction to COLD-K, (), 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 Paris · Zbl 0146.00703
[36] Lehmann, T.; Loeckx, J., The specification language of OBSCURE, (), 131-153 · Zbl 0663.68024
[37] Malcolm, G.; Goguen, J.A., Proving correctness of refinement and implementation, ()
[38] Milner, R., Fully abstract models of typed λ-calculi, (), 1-22 · Zbl 0386.03006
[39] Nivela, P.; Orejas, F., Initial behaviour semantics for algebraic specifications, (), 184-207 · Zbl 0679.68026
[40] Orejas, F.; Navarro, M.; Sanchez, A., Implementation and behavioural equivalence: a survey, (), 93-125
[41] Orejas, F.; Nivela, M.P., Constraints for behavioural specifications, (), 220-245
[42] Reichel, H., Behavioural equivalence — a unifying concept for initial and final specification methods, (), 27-39 · Zbl 0479.68017
[43] Reichel, H., Initial restrictions of behaviour, () · Zbl 0594.68013
[44] Reichel, H., Initial computability, algebraic specifications, and partial algebras, () · Zbl 0634.68001
[45] Sannella, D.T.; Burstall, R.M., Structured theories in LCF, (), 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, (), 375-389
[50] Sannella, D.T.; Wirsing, M., A kernel language for algebraic specifications and implementation, (), 413-427
[51] Schoett, O., Data abstraction and the correctness of modular programming, ()
[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, (), 675-788 · Zbl 0900.68309
[56] Wirsing, M., Structured specifications: syntax, semantics and proof calculus, (), 411-442, 1991
[57] Wolter, U., The power of behavioural validity, ()
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.