Categories and Subject Descriptors: C.0 [General]; D.1.4 [Programming Techniques]: Sequential Programming; D.2.1 [Software Engineering]: Requirements/Specifications -- methodologies; D.2.1 [Software Engineering]: Requirements/Specifications; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs -- specification techniques
General Terms: Design, Verification
Additional Key Words and Phrases: Interactive systesm, refinement, specification
Selected references
- Martín Abadi and Leslie Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73-132, January 1993.
- Martín Abadi and Gordon D. Plotkin. A logical view of composition and refinement. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 323-332, Orlando, Florida, January 1991.
- Luca Aceto and Matthew Hennessy. Adding action refinement to a finite process algebra. In Javier Leach Albert and Burkhard Monien and Mario Rodríguez-Artalejo, editors, Automata, Languages and Programming, 18th International Colloquium, volume 510 of Lecture Notes in Computer Science, pages 506-519, Madrid, Spain, 8-12 July 1991. Springer-Verlag.
- Manfred Broy, Bernhard Möller, Peter Pepper, and Martin Wirsing. Algebraic implementations preserve program correctness. Science of Computer Programming, 7(1):35-53, July 1986.
- C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271-281, 1972.
- Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27(3):333-354, December 1983.
- Leslie Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190-222, April 1983.
- Walter Vogler. Bisimulation and action refinement. In 8th Annual Symposium on Theoretical Aspects of Computer Science, volume 480 of Lecture Notes in Computer Science, pages 309-321, Hamburg, Germany, 14-16 February 1991. Springer.