Abstract
SOCOS is a prototype tool for constructing programs and reasoning about their correctness. It supports the invariant based programming methodology by providing a diagrammatic environment for specification, implementation, verification and execution of procedural programs. Invariants and contracts (pre- and postconditions) are evaluated at runtime, following the Design by Contract paradigm. Furthermore, SOCOS generates correctness conditions for static verification based on the weakest precondition semantics of statements. To verify the program the user can attempt to automatically discharge these conditions using the Simplify theorem prover; conditions which were not automatically discharged can be proved interactively in the PVS theorem prover.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Back, R.J.: Invariant based programming. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 1–18. Springer, Heidelberg (2006)
Back, R.J.: Invariant based programs and their correctness. In: Biermann, W., Guiho, G., Kodratoff, Y. (eds.) Automatic Program Construction Techniques, pp. 223–242. MacMillan Publishing Company, NYC (1983)
Back, R.J., Myreen, M.: Tool support for invariant based programming. In: The 12th Asia-Pacific Software Engineering Conference, Taipei, Taiwan (December 2005)
Back, R.J., Milovanov, L., Porres, I.: Software development and experimentation in an academic environment: The Gaudi experience. In: Bomarius, F., Komi-Sirviö, S. (eds.) PROFES 2005. LNCS, vol. 3547, Springer, Heidelberg (2005)
Back, R.J.: Incremental software construction with refinement diagrams. In: Broy Gunbauer, H., Hoare (eds.) Engineering Theories of Software Intensive Systems. NATO Science Series II: Mathematics, Physics and Chemistry, pp. 3–46. Springer, Marktoberdorf, Germany (2005)
Back, R.J., Milovanov, L., Porres, I., Preoteasa, V.: XP as a framework for practical software engineering experiments. In: Wells, D., Williams, L. (eds.) Extreme Programming and Agile Methods - XP/Agile Universe 2002. LNCS, vol. 2418, Springer, Heidelberg (2002)
Dijkstra, E.W.: A constructive approach to the problem of program correctness. BIT 8, 174–186 (1968)
Reynolds, J.C.: Programming with transition diagrams. In: Gries, D. (ed.) Programming Methodology, Springer, Berlin (1978)
Back, R.J.: Program construction by situation analysis. Research Report 6, Computing Centre, University of Helsinki, Helsinki, Finland (1978)
van Emden, M.H.: Programming with verification conditions. In: IEEE Transactions on Software Engineering, vol. SE–5, IEEE Computer Society Press, Los Alamitos (1979)
Abrial, J.R., Lee, M.K.O., Neilson, D.S., Scharbach, P.N., Sorensen, I.H.: The B-method (software development). In: Prehn, S., Toetenel, W.J. (eds.) VDM 1991. LNCS, vol. 552, pp. 398–405. Springer, Heidelberg, Germany (1991)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 212–232 (2005)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002. Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 234–245. ACM Press, New York, USA (2002)
van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, p. 299+. Springer, Heidelberg (2001)
Burdy, L., Requet, A., Lanet, J.L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction (Graduate Texts in Computer Science). Springer, Heidelberg (1998)
Alanen, M., Porres, I.: The Coral Modelling Framework. In: Koskimies, K., Kuzniarz, L., Lilius, J., Porres, I. (eds.) NWUML 2004. Proceedings of the 2nd Nordic Workshop on the Unified Modeling Language, Turku Centre for Computer Science, July 2004, vol. 35, General Publications (2004)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)
Back, R.J.: Software construction by stepwise feature introduction. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 162–183. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Back, RJ., Eriksson, J., Myreen, M. (2007). Testing and Verifying Invariant Based Programs in the SOCOS Environment. In: Gurevich, Y., Meyer, B. (eds) Tests and Proofs. TAP 2007. Lecture Notes in Computer Science, vol 4454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73770-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-73770-4_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73769-8
Online ISBN: 978-3-540-73770-4
eBook Packages: Computer ScienceComputer Science (R0)