A new approach for programming that enables switching among contexts of commands during program execution is context-oriented programming (COP). This technique is more structured and modular than object-oriented and aspect-oriented programming and hence more flexible. For context-oriented programming, as implemented in COP languages such as ContextJ* and ContextL, this paper introduces accurate operational semantics. The language model of this paper uses Java concepts and is equipped with layer techniques for activation/deactivation of layer contexts. This paper also presents a logical system for COP programs. This logic is necessary for the automation of testing, developing, and validating of partial correctness specifications for COP programs and is an extension of separation logic. A mathematical soundness proof for the logical system against the proposed operational semantics is presented in the paper. 1. Introduction To support and dynamically control the modularization of crosscutting concerns [1], a new programming style, context-oriented programming (COP) [2], has appeared. COP can be defined as a programming approach that produces software that is dynamically adaptable. COP was invented to treat programming problems when the behavior of the required software changes at runtime depending on the execution conditions. This is not easily achieved by classical approaches of programming. COP was established on languages like Smalltalk [3], Java [4], and JavaScript [5]. While the idea of homogeneous crosscutting is to execute the same source code at the join points of concerns, the idea of heterogeneous crosscutting concerns is to execute different source code at the join points. Heterogeneous crosscutting [1] is the type of crosscutting concerns adopted by COP. Partial functions declarations adapting common functions to their new style are used in COP to implement these crosscutting methodologies. Main components of COP include (a) layers of variant functions for providing performance alterations and (b) a tool for layer activation/deactavation. A variant function is a function that can be executed after, before, and around the same (variant) function included in another layer. Hence a layer is a group of variant functions. Layer declarations are used to encapsulate partial function declarations. The semantics of classes and that of crosscutting can be combined at the runtime. COP [2] provides a block statement defining a group of layers to enable runtime layer composition. Determined by the statement block, an execution scope is also provided by
References
[1]
G. Kiczales, J. Lamping, A. Mendhekar, et al., “Aspect-oriented programming,” in Proceedings of the European Conference on Object-Oriented Programming (ECOOP '97), pp. 220–242, Jyv？skyl？, Finland, June 1997.
[2]
R. Hirschfeld, P. Costanza, and O. Nierstrasz, “Context-oriented programming,” The Journal of Object Technology, vol. 7, no. 3, pp. 125–151, 2008.
[3]
W. Golubski and W.-M. Lippe, “A complete semantics for SMALLTALK-80,” Computer Languages, vol. 21, no. 2, pp. 67–79, 1995.
[4]
M. Campione, K. Walrath, and A. Huml, The Java Tutorial: A Short Course on the Basics, Addison-Wesley Longman Publishing, Boston, Mass, USA, 3rd edition, 2000.
[5]
D. Flanagan, JavaScript—Pocket Reference: Activate Your Web Pages, O'Reilly, 3rd edition, 2012.
[6]
J. C. Reynolds, “Separation logic: a logic for shared mutable data structures,” in Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS '02), pp. 55–74, July 2002.
[7]
S. S. Samin and P. W. O'Hearn, “BI as an assertion language for mutable data structures,” in Principles of Programming Languages, C. Hankin and D. Schmidt, Eds., pp. 14–26, ACM, 2001.
[8]
B. Jacobs, “Weakest pre-condition reasoning for Java programs with JML annotations,” Journal of Logic and Algebraic Programming, vol. 58, no. 1-2, pp. 61–88, 2004.
[9]
L. Burdy, Y. Cheon, D. R. Cok et al., “An overview of JML tools and applications,” International Journal on Software Tools for Technology Transfer, vol. 7, no. 3, pp. 212–232, 2005.
[10]
M. Huisman and B. Jacobs, “Java program verification via a hoare logic with abrupt termination,” in Fundamental Approaches to Software Engineering, T. S. E. Maibaum, Ed., vol. 1783 of Lecture Notes in Computer Science, pp. 284–303, Springer, Berlin, Germany, 2000.
[11]
J. M. Morris, “A general axiom of assignment,” in Theoretical Foundations of Programming Methodology, pp. 25–34, Springer, Berlin, Germany, 1982.
[12]
N. Dershowitz, Ed., Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, vol. 2772 of Lecture Notes in Computer Science, Springer, Berlin, Germany, 2003.
[13]
A. Banerjee and D. A. Naumann, “Ownership confinement ensures representation independence for object-oriented programs,” Journal of the ACM, vol. 52, no. 6, pp. 894–960, 2005.
[14]
M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino, “Boogie: a modular reusable verifier for object-oriented programs,” in Formal Methods for Components and Objects, F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P. de Roever, Eds., vol. 4111 of Lecture Notes in Computer Science, pp. 364–387, Springer, Berlin, Germany, 2006.
[15]
P. Müller, A. Poetzsch-Heffter, and G. T. Leavens, “Modular invariants for layered object structures,” Science of Computer Programming, vol. 62, no. 3, pp. 253–286, 2006.
[16]
D. von Oheimb, “Hoare logic for Java in Isabelle/hol,” Concurrency Computation Practice and Experience, vol. 13, no. 13, pp. 1173–1214, 2001.
[17]
G. Klein and T. Nipkow, “A machine-checked model for a Java-like language, virtual machine, and compiler,” ACM Transactions on Programming Languages and Systems, vol. 28, no. 4, pp. 619–695, 2006.
[18]
R. Hirschfeld, A. Igarashi, and H. Masuhara, “Contextfj: a minimal core calculus for context-oriented programming,” in Proceedings of the 10th International Workshop on Foundations of Aspect-Oriented Languages (FOAL '11), pp. 19–23, ACM, March 2011.
[19]
M. A. El-Zawawy and E. A. Aleisa, “A new model for context-oriented programs,” Life Science Journal, vol. 10, no. 2, pp. 2515–2523, 2013.
[20]
H. Schippers, D. Janssens, M. Haupt, and R. Hirschfeld, “Delegation-based semantics for modularizing crosscutting concerns,” in Proceedings of the 23rd ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '08), pp. 525–542, Nashville, Tenn, USA, October 2008.
[21]
D. Clarke and I. Sergey, “A semantics for context-oriented programming with layers,” in Proceedings of the International Workshop on Context-Oriented Programming (COP '09), ACM, Genova, Italy, July 2009.
