Abstract
Previously, we presented Circus, an integration of Z, CSP, and Morgan’s refinement calculus, with a semantics based on the unifying theories of programming. Circus provides a basis for development of state-rich concurrent systems; it has a formal semantics, a refinement theory, and a development strategy. The design of Circus is our solution to combining data and behavioural specifications. Here, we further explore this issue in the context of object-oriented features. Concretely, we present an object-oriented extension of Circus called OhCircus. We present its syntax, describe its semantics, explain the formalisation of method calls, and discuss our approach to refinement.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial J-R (1996) The B-Book: Assigning Progams to Meanings. Cambridge University Press
Back RJR (1987) Procedural Abstraction in the Refinement Calculus. Technical report, Department of Computer Science, Åbo, Finland. Ser. A No. 55.
Bolognesi T (2003) On State-oriented versus Object-oriented Thinking in Formal Behavioural Specifications. Technical Report 2003-TR-20, ISTI – Istituto di Scienza e Tecnologie della Informazione Alessandro Faedo
Borba PHM, Sampaio ACA, Cavalcanti ALC, Cornélio ML (2004) Algebraic Reasoning for Object-Oriented Programming. Science of Computer Programming 52:53–100
Borba PHM, Sampaio ACA, Cornélio ML (2003) A Refinement Algebra for Object-oriented Programming. In: European Conference on Object-oriented Programming 2003 – ECOOP 2003. Lecture Notes in Computer Science, vol 2743. Springer-Verlag, pp 457–482
Cavalcanti ALC, Naumann DA (2000) A Weakest Precondition Semantics for Refinement of Object-oriented Programs. IEEE Transactions on Software Engineering 26(8):713–728
Cavalcanti ALC, Naumann DA (2002) Forward simulation for data refinement of classes. In: Eriksson L, Lindsay PA (eds) FME 2002: Formal Methods – Getting IT Right, Lecture Notes in Computer Science, vol 2391. Springer-Verlag, pp 471–490
Cavalcanti ALC, Sampaio ACA, Woodcock JCP (2002) Refinement of Actions in Circus. In: Proceedings of REFINE’2002, Eletronic Notes in Theoretical Computer Science. Invited paper
Cavalcanti ALC, Sampaio ACA, Woodcock JCP (2003) A Refinement Strategy for Circus. Formal Aspects of Computing 15(2–3):146–181
Derrick J, Boiten E (2001) Refinement in Z and Object-Z. Springer
Dijkstra EW (1976) A Discipline of Programming. Prentice-Hall
Fischer C (1997) CSP-OZ: A combination of Object-Z and CSP. In: Bowman H, Derrick J (eds) Formal Methods for Open Object-Based Distributed Systems (FMOODS’97), vol 2. Chapman & Hall, pp 423–438
Fischer C (1998) How to Combine Z with a Process Algebra. In: Bowen J, Fett A, Hinchey M (eds) ZUM’98: The Z Formal Specification Notation. Springer-Verlag
Fischer C (2000) Combination and Implementation of Processes and Data: from CSP-OZ to Java. PhD thesis, Fachbereich Informatik Universität Oldenburg
Fisher C, Wehrheim H (2000) Behavioural Subtyping Relations for Object-oriented Formalisms. In: Rus T (ed) AMAST 2000: International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, vol 1816
Formal Systems (Europe) Ltd (1999) FDR: User Manual and Tutorial, version 2.28
Fowler M (1999) Refactoring. Addison-Wesley
Gosling J, Joy B, Steele G (1996) The Java Language Specification. Addison-Wesley
Hoare CAR, He J (1998) Unifying Theories of Programming. Prentice-Hall
Ichbiah J (1979) Rationale for the Design of the Ada Programming Language. ACM SIGPLAN Notices 14(6B (special issue))
Jones G (1988) Programming in occam 2. Prentice-Hall
Mahony B, Dong JS (2000) Timed Communicating Object Z. IEEE Transactions on Software Engineering 26(2):150–177
Morgan CC (1994) Programming from Specifications. Prentice-Hall, 2nd edition
Morris JM, Bunkenburg A (1998) Partiality and Nondeterminacy in Program Proofs. Formal Aspects of Computer Science 10:76–96
Mota AC, Sampaio ACA (2001) Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming 40:59–96
Oliveira MVM, Cavalcanti ALC (2004) From Circus to JCSP. In: Davies J et al. (eds) Sixth International Conference on Formal Engineering Methods. Lecture Notes in Computer Science, vol 3308. Springer-Verlag, pp 320–340, November 2004
Roscoe AW (1998) The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall
Sampaio ACA, Mota AC, Ramos RT (2003) Class and Capsule Refinement in UML for Real Time. In: Cavalcanti ALC, Machado PDL (eds) WMF 2003: 6th Brazilian Workshop on Formal Methods. Electronic Notes in Theoretical Computer Science, vol 95. Elsevier Science. Invited paper
Sampaio ACA, Mota AC, Ramos RT (2004) Class and Capsule Refinement in UML for Real Time. In: Cavalcanti ALC, Machado P (eds) WMF 2003: 6th Brazilian Workshop on Formal Methods, Electronic Notes in Theoretical Computer Science, vol 95. Elsevier
Sampaio ACA, Woodcock JCP, Cavalcanti ALC (2002) Refinement in Circus. In: Eriksson L, Lindsay PA (eds) FME 2002: Formal Methods – Getting IT Right, Lecture Notes in Computer Science, vol 2391. Springer-Verlag, pp 451–470
Schneider S, Treharne H (2002) Communicating B Machines. In: Bert D, Bowen J, Henson M, Robinson K (eds) ZB’2002: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, vol 2272, pp 416–435
Smith G (1999) The Object-Z Specification Language. Kluwer Academic Publishers
Sweeney C, Bowen M (1998) D-1-C Handel-C Language Reference Manual. Embedded Solutions Ltd
Wehrheim H (2000) Subtyping patterns for active objects. In: 8ter Workshop des GI Arbeitskreises GROOM (Grundlagen objektorientierter Modellierung)
Welch PH, Aldous JR, Foster J (2002) CSP Networking for Java (JCSP.net). In: Global and Collaborative Computing Workshop Proceedings, ICCS 2002, Lecture Notes in Computer Science, vol 2330. Springer-Verlag, pp 695–708
Woodcock JCP, Cavalcanti ALC (2001) A Concurrent Language for Refinement. In: Butterfield A, Pahl C (eds) IWFM’01: 5th Irish Workshop in Formal Methods, BCS Electronic Workshops in Computing, Dublin, Ireland, July 2001
Woodcock JCP, Cavalcanti ALC (2002) The Semantics of Circus. In: Bert D, Bowen JP, Henson MC, Robinson K (eds) ZB 2002: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, vol 2272. Springer-Verlag, pp 184–203
Woodcock JCP, Davies J (1996) Using Z – Specification, Refinement, and Proof. Prentice-Hall
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Cavalcanti, A., Sampaio, A. & Woodcock, J. Unifying classes and processes. Softw Syst Model 4, 277–296 (2005). https://doi.org/10.1007/s10270-005-0085-2
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10270-005-0085-2