Please use this identifier to cite or link to this item:
|Title:||Past expression: Encapsulating pre-states at post-conditions by means of AOP|
Runtime assertion checking (RAC)
|Source:||Yi, J.,Robby,Deng, X.,Roychoudhury, A. (2013). Past expression: Encapsulating pre-states at post-conditions by means of AOP. AOSD 2013 - Proceedings of the 2013 ACM on Aspect-Oriented Software Development : 133-144. ScholarBank@NUS Repository. https://doi.org/10.1145/2451436.2451453|
|Abstract:||Providing a pair of pre and post-condition for a method or a procedure is a typical way of program specification. When specifying a post-condition, it is often necessary to compare the post-state value of a variable with its pre-state value. To access a pre-sate value at a post-condition, most contract languages such as Eiffel and JML provide an old expression; old(x) returns a pre-state value of variable x. However, old expressions pose several problems, most notably the lack of encapsulation; old(x) does not encapsulate an object graph rooted from the pre-state value of x. Thus, method-call expressions like x.equals(old(x)) should generally not be used, and instead each field of x should be compared individually as in x.f1==old(x.f1) && x.f2==old(x.f2). In this paper, we first describe this lack of encapsulation and other problems of old expressions in more detail. Then, to address those problems, we propose our novel past expression along with its formal semantics. We also describe how our past expression can be supported during runtime assertion checking. We explain the involved problems, and show how we solve them. We implement our solution by means of AOP where we exploit various primitive pointcuts including our custom branch pointcut. Copyright © 2013 ACM.|
|Source Title:||AOSD 2013 - Proceedings of the 2013 ACM on Aspect-Oriented Software Development|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 16, 2017
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.