Abstract
We introduce a language in terms of syntax and a logical calculus that provides a theory for the specification and logical deduction of functional and relational programs modeling nondeterministic interactive systems specifications. We use formulas of classical predicate logic for formulating the specifications. The calculus consists of special rules for manipulating these formulas. These rules allow us to transform formulas containing functional nondeterministic programs into pure formulas of predicate logic. We put emphasis onto rules for the treatment of nondeterminism and recursive declarations including communication feedback. This way both a design calculus for the transformational development of interactive functional programs, as well as a calculus for their verification, is given. We demonstrate the usage of the calculus by a number of short examples.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. D. Brock and W. B. Ackermann. Scenarios: A Model of Nondeterminate Computation. In: J. Diaz, I. Ramos (eds): Lecture Notes in Computer Science 107, Springer 1981, 252-259.
M. Broy. A Fixed Point Approach to Applicative Multiprogramming. In: M. Broy, G. Schmidt (eds.): Theoretical Foundations of Programming Methodology, Reidel Publ. Comp. 1982, 565-623.
M. Broy. Fixed Point Theory for Communication and Concurrency. In: D. Björner (ed.): IFIP TC2 Working Conference on Formal Description of Programming Concepts II, Garmisch, June 1982, Amsterdam-New York-Oxford: North Holland Publ. Company 1983, 125–147.
M. Broy. Algebraic Methods for Program Construction: The Project CIP. In: P. Pepper (ed.): Program Transformation and Programming Environments. NATO ASI Series. Series F: 8. Berlin-Heidelberg-New York-Tokyo: Springer 1984, 199–222.
M. Broy. Specification and Top Down Design of Distributed Programs. In: H. Ehrig et al. (eds.): TAPSOFT 85. Lecture Notes in Computer Science 185. Berlin-Heidelberg-New York-Tokyo: Springer 1985, 4–28.
M. Broy. Predicative Specification of Robust Correctness for Functional Programs Describing Communicating Networks. Universität Passau, Fakultät für Mathematik und Informatik, MIP-8605, April 1986.
M. Broy. Predicative Specification for Functional Programs Describing Communicating Networks. Information Processing Letters 25, 1987, 93–101.
M. Broy. Nondeterministic Data Flow Programs: How to avoid the merge anomaly. Science of Computer Programming 10 (1988), 65–85.
M. Broy. Functional Specification of Time-Sensitive Communicating Systems. ACM Transactions on Software Engineering and Methodology 2:1, 1993, 1–46.
M. Broy and P. Pepper. Programming as a formal activity. IEEE Transactions on Software Engineering SE-7:1, 1983, 14–22
E. W. Dijkstra. A Discipline of Programming Prentice Hall, 1976.
P. Dybier. Reasoning about Streams in Intuitionistic Logic. Unpublished manuscript
E.C.R. Hehner. Predicative Specification. Part I+II. CACM 27:2 (1984) 134–151.
H. Hußmann. Nichtdeterministische algebraische Spezifikation. Dissertation, Universität Passau, Fakultät für Mathematik und Informatik, 1989.
S. J. Garland, J. V. Guttag. On Overview of LP, The Larch Prover. Lecture Notes in Computer Science 355, 1986, 137–151.
P. Hitchcock and D. Park. Induction Rules and Termination Proofs. M. Nivat (ed.): Proc. 1st ICALP. North Holland 73.
R. M. Keller. Denotational Semantics for Parallel Programs with Indeterminate Operators. In: E. J. Neuhold (ed.): Formal Description of Programming Concepts. Amsterdam North Holland 1978, 337–366.
Z. Manna. Mathematical Theory of Computation. McGraw Hill 1974
Z. Manna and R. Waldinger. A Logical Basis for Computer Programming. Addison-Wesley 1985.
D. Park. On the Semantics of Fair Parallelism. In: D. Björner (ed.): Abstract Software Specification. Lecture Notes in Computer Science 86, Berlin-Heidelberg-New York: Springer 1980, 504–526.
P. Pepper. Application of Modal Logics to the Reasoning about Applicative Programs. Habilitation Thesis. Technische Universität München, Fakultät für Mathematik und Informatik 1985.
A. Rabinovich and B. A. Trakhtenbrot. Communication among Relations. In: M.S. Paterson: ICALP 90, Lecture Notes in Computer Science 443, Berlin-Heidelberg-New York: Springer 1990, 294–307.
D. Scott. Lectures on a Mathematical Theory of Computation. In: Theoretical Foundations of Programming Methodology, edited by M. Broy and G. Schmidt. D. Reidel Publishing Company, 1982, pp. 145-292.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Broy, M. (2003). A Functional Calculus for Specification and Verification of Nondeterministic Interactive Systems. In: Dershowitz, N. (eds) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39910-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-39910-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21002-3
Online ISBN: 978-3-540-39910-0
eBook Packages: Springer Book Archive