Abstract
The unifying ground for interactive programs and component- based systems is the interaction between a user and the system or between a component and its environment. Modeling and reasoning about interactive systems in a formal framework is critical for ensuring the systems' reliability and correctness. A mathematical foundation based on the idea of contracts permits this kind of reasoning. In this paper we study an iterative choice contract statement which models an event loop allowing the user to repeatedly choose from a number of actions an alternative which is enabled and have it executed. We study mathematical properties of iterative choice and demonstrate its modeling capabilities by specifying a component environment which describes all actions the environment can take on a component, and an interactive dialog box permitting the user to make selections in a dialog with the system. We show how to prove correctness of the dialog box with respect to given requirements, and develop its renement allowing more complex functionality and providing wider choice for the user.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable specifications of reactive systems. In Proceedings of 16th ICALP, volume 372 of LNCS, pages 1–17, Stresa, Italy, 11-15 July 1989. Springer-Verlag.
R. Back, A. Mikhajlova, and J. von Wright. Modeling component environments and interactive programs using iterative choice. Technical Report 200, Turku Centre for Computer Science, September 1998.
R. J. R. Back. Changing data representation in the re nement calculus. In 21st Hawaii International Conference on System Sciences. IEEE, January 1989.
R. J. R. Back and J. von Wright. Contracts, games and re nement. In 4th Work-shop on Expressiveness in Concurrency, EXPRESS’97, volume 7 of Electronic Notes in Theoretical Computer Science. Elsevier, September 1997.
[5]R. J. R. Back and J. von Wright. Reasoning algebraically about loops. Technical Report 144, Turku Centre for Computer Science, November 1997.
R. J. R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, April 1998.
M. Broy. A theory for nondeterminism, parallelism, communication, and concurrency. Theoretical Computer Science, 45:1–61, 1986.
R. W. Floyd. Assigning meaning to programs. In J. T. Schwartz, editor, Math-ematical aspects of computer science, volume 19, pages 19–31. American Mathematical Society, 1967.
D. Garlan and D. Notkin. Formalizing design spaces: Implicit invocation mechanisms. In VDM 91, Volume 1: Conference Contributions, LNCS 551, pages 31–44. Springer-Verlag, Oct. 1991.1476 Ralph Back, Anna Mikhajlova, and Joakim von Wrigh
C. C. Morgan. Programming from Specifications. Prentice-Hall, 1990.
Y. N. Moschovakis. A model of concurrency with fair merge and full recursion. Information and Computation, 93(1):114–171, July 1991.
N. Ward and I. Hayes. Applications of angelic nondeterminism. In P.A.C. Bailes, editor, 6th Australian Software Engineering Conference, pages 391–404, Sydney,Australia, 1991.
P. Wegner. Interactive software technology. In J. Allen B. Tucker, editor, The Computer Science and Engineering Handbook. CRC Press, in cooperation with ACM, 1997.
[14] P. Wegner. Interactive foundations of computing. Theoretical Computer Science, 192(2):315–351, Feb. 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Back, R., Mikhajlova, A., von Wright, J. (1999). Reasoning about interactive systems. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_27
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive