×

zbMATH — the first resource for mathematics

A graph-based implementation for mechanized refinement calculus of OO programs. (English) Zbl 1325.68066
Davies, Jim (ed.) et al., Formal methods: foundations and applications. 13th Brazilian symposium on formal methods, SBMF 2010, Natal, Brazil, November 8–11, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-19828-1/pbk). Lecture Notes in Computer Science 6527, 258-273 (2011).
Summary: This paper extends the mechanization of the refinement calculus done by von Wright in HOL, representing the state of a program as a graph instead of a tuple, in order to deal with object-orientation. The state graph structure is implemented in Isabelle, together with definitions and lemmas, to help the manipulation of states. We then show how proof obligations are automatically generated from the rCOS tool and can be loaded in Isabelle to be proved. We illustrate our approach by generating the proof obligations for a simple example, including object access and method invocation.
For the entire collection see [Zbl 1213.68032].
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
LOOP; rCOS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Back, R.-J.: On the Correctness of Refinement Steps in Program Development. PhD thesis, Helsinki, Finland, Report A–1978–4 (1978)
[2] Back, R.-J., Fan, X., Preoteasa, V.: Reasoning about pointers in refinement calculus. Technical Report 543, TUCS - Turku Centre for Computer Science, Turku, Finland (July 2003)
[3] Carrington, D., Hayes, I., Nickson, R., Watson, G., Welsh, J.: A tool for developing correct programs by refinement. In: Proc. BCS 7th Refinement Workshop. Springer, Heidelberg (1996) · Zbl 0910.68050
[4] Cavalcanti, A., Naumann, D.A.: A weakest precondition semantics for refinement of object-oriented programs. IEEE Transactions on Software Engineering 26, 713–728 (2000) · Zbl 05114166 · doi:10.1109/32.879810
[5] Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in component-based model driven design. Science of Computer Programming 74(4), 168–196 (2009); UNU-IIST TR 388 · Zbl 1178.68158 · doi:10.1016/j.scico.2008.08.003
[6] Chen, Z., Liu, Z., Stolz, V.: The rCOS tool. In: Modelling and Analysis in VDM: Proceedings of the Fourth VDM/Overture Workshop, number CS-TR-1099 in Technical Report Series. Newcastle University (May 2008) · Zbl 1151.68380
[7] Chen, Z., Morisset, C., Stolz, V.: Specification and validation of behavioural protocols in the rCOS modeler. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 387–401. Springer, Heidelberg (2010) · Zbl 05663825 · doi:10.1007/978-3-642-11623-0_23
[8] Depasse, C.: Constructing Isabelle proofs in a proof refinement calculus. Research Report, UCL (2001)
[9] Filliâtre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud (2003)
[10] He, J., Liu, Z., Li, X.: rCOS: A refinement calculus of object systems. Theor. Comput. Sci. 365(1-2), 109–142 (2006); UNU-IIST TR 322 · Zbl 1118.68049 · doi:10.1016/j.tcs.2006.07.034
[11] Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998) · Zbl 1005.68036
[12] Ke, W., Liu, Z., Wang, S., Zhao, L.: A graph-based operational semantics of oo programs. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 347–366. Springer, Heidelberg (2009) · Zbl 05635818 · doi:10.1007/978-3-642-10373-5_18
[13] Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006) · doi:10.1145/1146809.1146811
[14] Laibinis, L.: Mechanised Formal Reasoning About Modular Programs. PhD thesis, Abo Akademi (2000)
[15] Lei, B., Liu, Z., Morisset, C., Li, X.: State based robustness testing for components. In: FACS 2008. ENTCS, vol. 260, pp. 173–188. Elsevier, Amsterdam (2008)
[16] Liu, Z., Morisset, C., Stolz, V.: rCOS: theory and tools for component-based model driven development. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 62–80. Springer, Heidelberg (2010) · Zbl 05663805 · doi:10.1007/978-3-642-11623-0_3
[17] Morgan, C.: Programming from specifications, 2nd edn. Prentice Hall International, Englewood Cliffs (1994) · Zbl 0829.68083
[18] Paige, R., Ostroff, J., Brooke, P.: Formalising eiffel references and expanded types in pvs. In: Proc. International Workshop on Aliasing, Confinement, and Ownership in Object-Oriented Programming (2003)
[19] Paige, R.F., Ostroff, J.S.: ERC – An object-oriented refinement calculus for Eiffel. Form. Asp. Comput. 16(1), 51–79 (2004) · Zbl 1084.68022 · doi:10.1007/s00165-003-0024-3
[20] Sekerinski, E.: A type-theoretic basis for an object-oriented refinement calculus. In: Formal Methods and Object Technology. Springer, Heidelberg (1996)
[21] Stolz, V.: An integrated multi-view model evolution framework. Innovations in Systems and Software Engineering (2009)
[22] Utting, M.: An object-oriented refinement calculus with modular reasoning (1992)
[23] van den Berg, J., Jacobs, B.: The loop compiler for java and jml. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001) · Zbl 0978.68708 · doi:10.1007/3-540-45319-9_21
[24] von Wright, J.: Program refinement by theorem prover. In: BCS FACS Sixth Refinement Workshop – Theory and Practise of Formal Software Development. Springer, Heidelberg (1994)
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.