# Testing Automation of Context-Oriented Programs Using Separation Logic

Authors: Mohamed A. El-Zawawy
Journal: Applied Computational Intelligence and Soft Computing
 (2014)

---

## Abstract

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.


---

## Body

## 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 COP. In this scope layers are typically combined with the base system. Another statement enables stopping execution of specified layers. The keywords denoting these two statements arewith andwithout statements [2]. COP appears to be a very convenient technique for encapsulation of homogeneous crosscutting concerns as proved by many applications.However, so far research did not provide appropriate logic to reason about context-oriented programs. A main concern in COP is the treatment of layers activations/deactivations. Usually, the set of active layers changes from one program point to another. Therefore the efficiency of any logic for COP strongly depends on using correct layers. In spite of the concept of activating/deactvating a layer is simple, and its logical treatment is a bit complex.To reason about resources, Reynolds [6] and independently Samin and O’Hearn [7] presented new logic (separation logic). This was based on Burstall’s early work. A logical operator (separation conjunction) enabling localizing operation actions on shared resources is among the main contributions of separation logic. Sound form of local reasoning was reached by the separation conjunction which ensures the invariance of resources not included in preconditions.To model the meanings of COP concepts, this paper introduces operational semantics. Accurate meanings for basics of COP languages are provided by the semantics. Axiomatic semantics for COP is the second contribution of this paper. This semantics is an extension of separation logic to establish and ensure partial correctness specifications for COP programs. Rather than other logic, separation logic seems most suitable for verifying COP. This is so as the concept of context changing is explicitly “treated” by the special operators of separation logic. One of the challenges in this paper is to expose this explicit relationship in the form of formal definitions and inference rules. Judgments of the proposed logic have the formL
⊨
P
S
{
Q
} meaning that(i)
if layers ofL are active, then executing S in a state satisfying P is ensured not to abort,
(ii)
if layers ofL are active and the execution of S in a state satisfying P ended at some state, then this last state satisfies Q.AssertionsP and Q may reason about the program control locations as well as upon the values of local and global variables. A system of axioms and inference rules constituting the proposed logic is introduced in the paper which presents a partial correctness specification, for example, COP-program, as well. Against the proposed operational semantics, the mathematical soundness of the logical system is shown in this paper.Contributions of this paper are as follows:(1)
new operational semantics to provide accurate meanings for COP concepts,
(2)
novel axiomatic semantics to construct and validate partial correctness specifications for COP programs.The rest of the paper is organized as follows. Section2 presents in detail the programming language J-COP and its operational semantics. The assertion language, axioms, and inferences rules constituting the logical system are presented in Section 3 which also presents the mathematical proof for the correctness of the system and an example of its use. Related research is presented in Section 4.


## 2. Programming Language and Operational Semantics

The syntax and semantics of the programming language (dubbed J-COP) used in this paper are presented in this section. Basic aspects of object-oriented programming like inheritance and subtyping are modeled in J-COP which follows Java syntax for comparable structures. Algorithm1 presents the syntax of J-COP.Algorithm 1:The programming language J-COP.
e
∈
AExpr
∶
:
=
n
∣
o
∣
e
⋅
v
∣
e
1
i
o
p
e
2
∣
(
C
)
e
∣
this
b
∈
BExpr
∶
:
=
true
∣
false
∣
e
1
c
o
p
e
2
∣
b
1
b
o
p
b
2
l
e
∈
LayerExpr
∶
:
=
with
l
∣
without
l
∣
ϵ
∣
l
e
l
e
S
∈
Stat
∶
:
=
e
1
⋅
v
≔
e
2
∣
o
1
≔
l
e
o
2
⋅
f
(
e
)
∣
o
1
≔
o
2
⋅
f
(
e
)
∣
o
≔
s
u
p
e
r
⋅
f
(
e
)
∣
o
1
≔
proceed
o
2
⋅
f
(
e
)
∣
o
≔
new
C
∣
S
;
S
∣
if
b
then
S
t
else
S
f
∣
while
b
do
S
t
funs
∈
Fun
∶
:
=
f
(
p
)
{
S
;
return
(
e
)
;
}
layer
∈
Lay
∶
:
=
Layer
l
{
fun
}
inhrt
∈
Inherits
∶
:
=
ϵ
∣
inherits
C
cls
∈
Class
∶
:
=
class
C
inhrt
{
fu
n
*
laye
r
*
}
prog
∈
Prog
∶
:
=
cls
*
main
(
)
{
S
}J-Cop is a rich model for COP. The model includes basic language constructs and is extendable directly over well-studied Java features. Although the model is expressive enough to include more language features, it is simple. In addition to typical Java constructs, the model allows layers activation/deactivation, overriding variant functions, and a technique for executingproceed andsuper.We letC denote the typical member of the set of names of classes C which is included in the set of types (Types). In addition to C,Types includes function and reference types. The typical element ofTypes is denoted by τ. As it is common in programming, J-COP’s functions contain local variables whose scopes are the same as their functions. Also parameters for functions are local variables which are denoted byLVar. Instance variables model internal states of classes. We let I
V
a
r
C denote the set of instance variables of the class C. The symbols o and v denote typical elements ofLVar and I
V
a
r
C, respectively. Sequences of layers activation/deactivation constitute layer expressions (LayerExpr) with l
e
∈
L
a
y
e
r
E
x
p
r.FunNames andLayerNames denote the sets of function and layer names, respectively, with f
∈
F
u
n
N
a
m
e
s and l
∈
L
a
y
e
r
N
a
m
e
s.A class in J-COP includes function definitions and a group of layers containing function definitions. A function is defined via a parameter, a statement, and an expression. The expression models the returned value of the function. A set of classes and a main function (marks the start of program execution) are the components of a J-COP program.The operational semantics of J-COP presented in this section is defined using state representations and a subtype relation on classes. IfC inherits D by definition of C, then C is asubclass of D (denoted by C
≪
D) and D is asuperclass of C. The reflexive transitive closure of ≪ is denoted by ≤. States of the operational semantics are presented in Definition 1 where A denotes an infinite set of memory addresses with α
∈
A and Z is the set of integers.Definition 1.
One has the following:(1)
D
=
Z
∪
A;
(2)
L
a
y
e
r
C and F
u
n
C denote the sets of function and layer names of C, respectively;
(3)
Stacks
=
{
s
∣
s
:
L
V
a
r
→
p
Z
};
(4)
ObjCont
=
{
O
C
∣
O
C
:
I
V
a
r
C
→
Z
,
C
∈
C
};
(5)
Heaps
=
{
h
∣
h
:
A
→
p
ObjCont
};
(6)
S
t
a
t
e
s
=
Stacks
×
Heaps.The setD includes model values. States of the operational semantics are pairs of a stack and a heap. A special variable (called this), to point at the object being executed, is included in the set of local variables. For each class C, we assume two functions F
C and L
C. The map F
C determines for every function f
∈
F
u
n
C its components (
p
f
,
S
f
,
e
f
), the parameter variable of the function, the function statement, and the returned expression of the function. The map I
C determines for every layer l
∈
L
a
y
e
r
C the parts of the layer’s function (
f
,
p
f
,
S
f
,
e
f
). We also assume a function SerLay(
L
,
l
e
,
f
)
=
L
′
=
{
l
1
,
…
,
l
m
} whose inputs are a set of layers, a layer expression, and a function name. SerLay adds (removes) layers activated (deactivated) by l
e to (from) L. ThenSerLay returns the set of layers in L containing definitions for f.The semantics of arithmetic and boolean expressions of J-COP is similar to the case of simple imperative language. The cases of(
C
)
e and e
·
v are shown in Algorithm 2. Some comments on this algorithm are in order. The expression e
·
v denotes the variable v of the class referenced by e. In line with common OOP concepts, variables of C and that of its ancestors are included in domain of I
V
a
r
C. Therefore the semantics of e
·
v is defined only if v is a local variable of the class referenced by e or any of the class’s ancestors. The semantics of e (in e
·
v) is supposed to be an address containing a class object. The semantics of (
C
)
e is undefined if e is the address of an object of a class D that is not a descendant of C.Algorithm 2:Semantics of J-COP expressions.
[
C
(
e
)
]
(
s
,
h
)
=
{
u
n
d
e
f
i
n
e
d
,
if
[
e
]
(
s
,
h
)
∈
d
o
m
(
h
)
,
h
(
[
e
]
(
s
,
h
)
)
=
O
D
,
a
n
d
D
≰
C
;
[
e
]
(
s
,
h
)
,
otherwise
.
[
e
⋅
v
]
(
s
,
h
)
=
{
O
D
(
v
)
,
if
h
(
[
e
]
(
s
,
h
)
)
=
O
D
a
n
d
v
∈
d
o
m
(
O
D
)
;
u
n
d
e
f
i
n
e
d
,
otherwise.Algorithm3 presents the semantics of J-COP’s statements. The judgments of the semantics have the form L
⊣
S
:
(
s
,
h
)
→
(
s
′
,
h
′
) meaning that executing S in the state (
s
,
h
) results in the state (
s
′
,
h
′
) provided that L is the set of the currently active layers. Some comments on the rules are as follows. The local variable v of the object pointed to by e
1 is updated in the rule (
:
=
e
s
). This amounts to modifying the function O
C in the image of [
e
1
]
(
s
,
h
) under h. With input e, the rule (
:
=
o
·
f
s
) provides semantics for running the function f of the object pointed to by o
2. The semantics of l
e in o
1
:
=
l
e
o
2
·
f
(
e
) is to activate/deactivate certain layers. The rule (
:
=
l
·
o
·
f
s
) provides operational semantics for this statement. This rule does the call SerLay(
L
,
l
e
,
f
) to add (remove) layers activated (deactivated) via l
e to (from) L. This call then returns the subset of L with definitions for f. The rule then executes the bodies of layer functions sequentially. The execution number i builds on its previous execution by updating o
1 to the value [
e
i
-
1
]
(
s
i
,
h
i
). The statement o
:
=
super
·
f
(
e
) running the function f of an ancestor of the current object is given semantics in the rule (
sup
⁡
s
). The rule assumes a functionsuper that finds the ancestor of the class pointed to by o
2 such that this ancestor includes a definition for f. Semantics for o
1
:
=
proceed
o
2
·
f
(
e
) is given in the rule (
pro
s
). This statement runs all functions f in active layers of the object referenced by o
2.Algorithm 3:Inference rules of the operational semantics for J-COP constructs.
O
C
=
h
(
[
e
1
]
(
s
,
h
)
)
O
C
′
=
O
C
[
v
↦
[
e
2
]
(
s
,
h
)
]
L
⊣
e
1
⋅
v
≔
e
2
:
(
s
,
h
)
→
(
s
,
h
[
[
e
1
]
(
s
,
h
)
↦
O
C
′
]
)
(
≔
e
s
)
h
(
[
o
2
]
(
s
,
h
)
)
=
O
C
F
C
(
f
)
=
(
p
f
,
S
f
,
e
f
)
L
⊣
S
f
:
(
s
[
this
↦
s
(
o
2
)
,
p
f
↦
[
e
]
(
s
,
h
)
]
,
h
)
→
(
s
′
′
,
h
′
′
)
L
⊣
o
1
≔
o
2
⋅
f
(
e
)
:
(
s
,
h
)
→
(
s
′
′
[
o
1
↦
[
e
f
]
(
s
′
′
,
h
′
′
)
]
,
h
′
′
)
(
≔
o
⋅
f
s
)
SerLay
(
L
,
l
e
,
f
)
=
L
′
=
{
l
1
,
…
,
l
m
}
h
(
s
(
o
2
)
)
=
O
C
∀
1
≤
i
≤
m
(
L
C
(
l
i
)
=
(
f
,
p
i
,
S
i
,
e
i
)
)
L
′
⊣
S
1
:
(
s
[
this
↦
s
(
o
2
)
,
p
1
↦
[
e
]
(
s
,
h
)
]
,
h
)
→
(
s
2
,
h
2
)
∀
i
>
1
.
L
′
⊣
S
i
:
(
s
i
[
o
1
↦
[
e
i
-
1
]
(
s
i
,
h
i
)
,
this
↦
s
i
(
o
2
)
,
p
i
↦
[
e
]
(
s
i
,
h
i
)
]
,
h
i
)
→
(
s
i
+
1
,
h
i
+
1
)
L
⊣
o
1
≔
l
e
o
2
⋅
f
(
e
)
:
(
s
,
h
)
→
(
s
m
+
1
[
o
1
↦
[
e
m
]
(
s
m
+
1
,
h
m
+
1
)
]
,
h
m
+
1
)
(
≔
l
⋅
o
⋅
f
s
)
h
(
s
(
this
)
)
=
O
C
C
≪
E
super
(
E
,
f
)
=
D
F
D
(
f
)
=
(
p
f
,
S
f
,
e
f
)
L
⊣
S
f
:
(
s
[
p
f
↦
[
e
]
(
s
,
h
)
]
,
h
)
→
(
s
′
′
,
h
′
′
)
L
⊣
o
≔
super
⋅
f
(
e
)
:
(
s
,
h
)
→
(
s
′
′
[
o
↦
[
e
f
]
(
s
′
′
,
h
′
′
)
]
,
h
′
′
)
(
sup
⁡
s
)
a
∈
A
∖
d
o
m
(
h
)
L
⊣
o
≔
new
C
:
(
s
,
h
)
→
(
s
[
o
↦
a
]
,
h
[
a
↦
∅
]
)
(
new
s
)
h
(
s
(
o
2
)
)
=
O
C
L
′
=
{
l
1
,
…
,
l
m
}
⊆
L
.
(
∀
1
≤
i
≤
m
(
L
C
(
l
i
)
)
=
(
f
,
p
i
,
S
i
,
e
i
)
)
L
′
⊣
S
1
:
(
s
1
[
this
↦
s
(
o
2
)
,
p
1
↦
[
e
]
(
s
1
,
h
1
)
]
,
h
1
)
→
(
s
2
,
h
2
)
∀
i
>
1
.
L
′
⊣
S
i
:
(
s
i
[
o
1
↦
[
e
i
-
1
]
(
s
i
,
h
i
)
,
this
↦
s
(
o
2
)
,
p
i
↦
[
e
]
(
s
i
,
h
i
)
]
,
h
i
)
→
(
s
i
+
1
,
h
i
+
1
)
L
⊣
o
1
≔
proceed
o
2
⋅
f
(
e
)
:
(
s
,
h
)
→
(
s
m
+
1
[
o
1
↦
[
e
m
]
(
s
m
+
1
,
h
m
+
1
)
]
,
h
m
+
1
)
(
p
s
)
(
[
b
]
(
s
,
h
)
=
true
∧
L
⊣
S
t
:
(
s
,
h
)
→
(
s
′
,
h
′
)
)
∨
(
[
b
]
(
s
,
h
)
=
false
∧
L
⊣
S
f
:
(
s
,
h
)
→
(
s
′
,
h
′
)
)
L
⊣
if
b
then
S
t
else
S
f
:
(
s
,
h
)
→
(
s
′
,
h
′
)
(
if
s
)
[
b
]
(
s
,
h
)
=
false
L
⊣
while
b
do
S
t
:
(
s
,
h
)
→
(
s
,
h
)
(
whl
1
s
)
L
⊣
S
1
:
(
s
,
h
)
→
(
s
′
′
,
h
′
′
)
L
⊣
S
2
:
(
s
′
′
,
h
′
′
)
→
(
s
′
,
h
′
)
L
⊣
S
1
;
S
2
:
(
s
,
h
)
→
(
s
′
,
h
′
)
(
sq
s
)
[
b
]
(
s
,
h
)
=
true
L
⊣
S
t
:
(
s
,
h
)
→
(
s
′
′
,
h
′
′
)
L
⊣
while
b
do
S
t
:
(
s
′
′
,
h
′
′
)
→
(
s
′
,
h
′
)
L
⊣
while
b
do
S
t
:
(
s
,
h
)
→
(
s
′
,
h
′
)
(
whl
2
s
)


## 3. Assertion Language and Logical System

Extended separation logic to cover context-oriented programs is presented in this section. The section introduces the assertion language followed by the logical system’s axioms and inference rules. Against the operational semantics presented in the previous section, this section also outlines a formal mathematical proof for the correctness of the logical system. Finally an example of a derivation for a partial correctness specification using the logical system is included in this section as well.Boolean expressions, classical connectives, first order quantifications, and assertions specific to separation logic are the components of separation logic assertions. The following version of assertions is used in this section.(i)
emp denotes an empty heap.
(ii)
e
↦
C denotes that the heap has a unique memory cell whose address is e and whose content is an instance of the class C.
(iii)
this
↦
C denotes a special case of the previous assertion where e
=
this.
(iv)
P
*
Q dubbed separating conjunction.
(v)
P
-

*
Q dubbed separating implication.
(vi)
⊛
i
∈
I
P
i is a general form of separating conjunction.Algorithm4 presents the specific definition of the language of assertions. A group of states are modeled by every assertion via a modeling relation ((
s
,
h
)
⊨
P). The semantics of this relation is that the state (
s
,
h
) satisfies the assertion P. Definition 2 formalizes the semantics of the modeling relation.Algorithm 4:The assertion language.
e
∈
AExpr
:
≔
n
∣
o
∣
e
⋅
v
∣
e
1
i
o
p
e
2
∣
(
C
)
e
∣
this
b
∈
BExpr
:
≔
true
∣
false
∣
e
1
c
o
p
e
2
∣
b
1
b
o
p
b
2
P
,
Q
,
R
,
J
1
,
J
2
∈
Asset
:
≔
b
∣
P
∧
Q
∣
P
∨
Q
∣
P
⇒
Q
∣
¬
P
∣
∀
x
.
P
∣
∃
x
.
P
∣
fine
(
e
)
∣
emp
∣
e
↦
C
∣
P
*
Q
∣
P  −*  Q
∣
⊛
i
∈
I
P
i.Definition 2.
One has the following:(i)
s
,
h
⊨
fine
e
1
,
…
,
e
n
⇔
def for all i. ⟦
e
i
⟧
s
,
h
≠
abort;
(ii)
(
s
,
h
)
⊨
emp
⇔
def
dom
⁡
(
h
)
=
∅;
(iii)
s
,
h
⊨
e
↦
C
⇔
def
dom
⁡
h
=
{
⟦
e
⟧
(
s
,
h
)
} and h
(
⟦
e
⟧
(
s
,
h
)
)
=
O
C;
(iv)
s
,
h
⊨
P
1
*
P
2
⇔
def
∃
h
′
,
h
′′.  h
′
#
h
′′
,
h
=
h
′
·
h
′′
,
s
,
h
′
⊨
P
1, and (
s
,
h
′′
)
⊨
P
2;
(v)
(
s
,
h
)
⊨
P
1
-

*
P
2
⇔
def for all h
′
(
(
h
′
#
h
and
(
s
,
h
′
)
⊨
P
1
)
⇒
(
s
,
h
·
h
′
)
⊨
P
2
).
The fact thatdom
⁡
(
h
1
)
∩
dom
⁡
(
h
2
)
=
∅ is denoted by the expression h
1
#
h
2. The union of heaps is denoted by h
1
·
h
2 and is defined only if h
1
#
h
2.A judgment of the proposed logical system is of the formL
⊨
{
P
}
S
{
Q
} where P and Q are the pre- and postconditions, respectively. The semantics of this judgment is that if layers of L are active and S is executed in a state satisfying P, then the final state will satisfy Q. Definition 3 formalizes the soundness concept of specifications produced by the logical system. Axioms and inference rules of the logical system are introduced in Algorithm 5.Algorithm 5:The inference rules of the proposed logical system.
L
⊣
{
e
1
↦
C
∧
fine
(
e
1
⋅
v
)
∧
fine
(
e
2
)
∧
Q
[
e
2
/
e
1
⋅
v
]
}
e
1
⋅
v
≔
e
2
{
Q
}
(
≔
e
l
)
F
C
(
f
)
=
(
p
f
,
S
f
,
e
f
)
L
⊣
{
R
[
o
2
/
this
,
e
/
p
f
]
}
S
f
{
Q
[
e
f
/
o
1
]
}
L
⊣
{
o
2
↦
C
∧
R
∧
fine
(
e
,
e
f
)
}
o
1
≔
o
2
⋅
f
(
e
)
{
Q
}
(
≔
o
⋅
f
l
)
SerLay
(
L
,
l
e
,
f
)
=
L
′
=
{
l
1
,
…
,
l
m
}
L
′
⊣
{
R
[
o
2
/
this
,
e
/
p
1
]
}
S
1
{
Q
1
[
e
1
/
o
1
]
}
∀
i
>
1
.
L
′
⊣
{
Q
i
-
1
[
o
2
/
this
,
e
/
p
i
]
}
S
i
{
Q
i
[
e
i
/
o
1
]
}
L
⊣
{
o
2
↦
C
∧
R
∧
fine
(
e
,
e
1
,
…
,
e
m
)
}
o
1
≔
l
e
o
2
⋅
f
(
e
)
{
Q
m
}
(
≔
l
⋅
o
⋅
f
l
)
super
(
E
,
f
)
=
D
F
D
(
f
)
=
(
p
f
,
S
f
,
e
f
)
L
⊣
{
R
[
e
/
p
f
]
}
S
f
{
Q
[
e
f
/
o
]
}
L
⊣
{
this
↦
C
∧
C
≪
E
∧
R
∧
fine
(
e
,
e
f
)
}
o
≔
super
⋅
f
(
e
)
{
Q
}
(
sup
⁡
l
)
L
⊣
{
emp
}
o
≔
new
C
{
o
↦
C
}
(
new
l
)
L
′
=
{
l
1
,
…
,
l
m
}
⊆
L
.
(
∀
1
≤
i
≤
m
(
L
C
(
l
i
)
)
=
(
f
,
p
i
,
S
i
,
e
i
)
)
L
′
⊣
{
R
[
o
2
/
this
,
e
/
p
1
]
}
S
1
{
Q
1
[
e
1
/
o
1
]
}
∀
i
>
1
.
L
′
⊣
{
Q
i
-
1
[
o
2
/
this
,
e
/
p
i
]
}
S
i
{
Q
i
[
e
i
/
o
1
]
}
L
⊣
{
o
2
↦
C
∧
R
}
o
1
≔
proceed
o
2
⋅
f
(
e
)
{
Q
m
}
(
pro
l
)
L
⊣
{
P
}
S
1
{
R
}
L
⊣
{
R
}
S
2
{
Q
}
L
⊣
{
P
}
S
1
;
S
2
{
Q
}
(
Seq
l
)
L
⊣
{
P
}
S
{
Q
}
L
⊣
{
P
′
}
S
{
Q
′
}
L
⊣
{
P
∨
P
′
}
S
{
Q
∨
Q
′
}
(
Disj
l
)
L
⊣
{
P
∧
b
}
S
t
{
Q
}
L
⊣
{
P
∧
¬
(
b
)
}
S
f
{
Q
}
L
⊣
{
P
}
if
b
then
S
t
else
S
f
{
Q
}
(
if
l
)
L
⊣
{
fine
(
b
)
∧
P
}
S
t
{
fine
(
b
)
∧
P
}
L
⊣
{
fine
(
b
)
∧
P
}
while
b
do
S
t
{
¬
(
b
)
∧
P
}
(
while
l
)
L
⊣
{
P
}
S
{
Q
}
P
′
⟹
P
Q
⟹
Q
′
L
⊣
{
P
′
}
S
{
Q
′
}
(
seq
l
)
L
1
⊣
{
P
}
S
{
Q
}
L
2
⊣
{
P
′
}
S
{
Q
′
}
L
1
∪
L
2
⊣
{
P
∧
P
′
}
S
{
Q
∧
Q
′
}
(
Conj
l
)
L
1
⊣
{
P
}
S
{
Q
}
L
2
⊣
{
R
}
S
{
R
}
L
1
∩
L
2
=
∅
L
1
∪
L
2
⊣
{
P
*
R
}
S
{
Q
*
R
}
(
share
l
)
L
⊣
{
P
}
S
{
Q
}
f
v
(
R
)
∩
mod
⁡
(
S
,
L
)
=
∅
L
⊣
{
P
*
R
}
S
{
Q
*
R
}
(
frame
l
)
{
l
}
⊣
{
P
}
S
{
Q
}
L
∖
{
l
}
⊣
{
J
1
}
S
{
J
2
}
L
⊣
{
P
∧
J
1
}
S
{
Q
∨
J
2
}
(
glob
l
)
L
⊣
{
P
}
S
{
Q
}
x
∉
f
v
(
S
)
L
⊣
{
∃
x
.
P
}
S
{
∃
x
.
Q
}
(
Ex
l
)We fix theabortion notion for Definition 3. A statement S isaborting at (
s
,
h
) (denoted by S
:
(
s
,
h
,
L
)
→
abort
) if (a) a state (
s
′
,
h
′
) such that S
:
(
s
,
h
)
→
(
s
′
,
h
′
) is not available and (b) S is not stuck in an infinite loop.Definition 3.
A specificationL
⊣
{
P
}
S
{
Q
} is sound if, for each (
s
,
h
) such that s
,
h
⊨
P, the following is satisfied:(1)
¬
(
L
⊨
S
:
(
s
,
h
)
→
abort
),
(2)
ifL
⊨
S
:
(
s
,
h
)
→
(
s
′
,
h
′
), then (
s
′
,
h
′
)
⊨
Q.Some of the rules in Algorithm5 are certainly noteworthy. In many rules like (
≔
e
l
) and (
≔
o
·
f
l
), the expressions of relevant statements contribute to the preconditions of the rules. This has the advantage of ensuring that the meant memory addresses are indeed allocated and hence evaluations of expressions do not abort. The preconditions of (
≔
e
l
) and (
≔
o
·
f
l
) also ensure that appropriate variables reference objects in heap. The side-conditions of (
≔
o
·
f
l
) and (
≔
l
·
o
·
f
l
) consider that executing these statements involves executing certain function bodies. We let mod
⁡
(
S
,
L
) denote the set of locations modified by S provided that layers of L are active. The symbol f
v
(
R
) denotes the set of free variables of R. The rule (
share
l
) enables the composition of specifications having disjoint sets of activated layers if the preconditions of the specifications describe disjoint regions of the heap. The rule (
frame
l
) enables avoiding a frame of the heap, R, that does not affect the statement. This rule also ensures that R is satisfied by the postcondition.Soundness. The soundness of the logical system is guaranteed by the following theorem.Theorem 4.
SpecificationsL
⊣
{
P
}
S
{
Q
} that resulted using the logical system of Algorithm 5 are sound (Definition 3).Proof.
Structure induction on axioms and inference rules of Algorithm5 achieves the proof. In the following, basic cases are outlined.(i)
The case of the rule(
≔
e
l
): in this case
(a)
S
=
e
1
·
v
≔
e
2,
(b)
P
⇔
e
1
↦
C
∧
fine
(
e
1
·
v
)
∧
fine
(
e
2
)
∧
Q
[
e
2
/
e
1
·
v
].
Suppose that, for state(
s
,
h
)
,
(
s
,
h
)
⊨
P. Hence O
C
=
h
(
⟦
e
1
⟧
(
s
,
h
)
) and ⟦
e
2
⟧
(
s
,
h
)
=
abort. Therefore O
C
′
=
O
C
[
v
↦
⟦
e
2
⟧
(
s
,
h
)
] is defined and so does (
s
,
h
[
⟦
e
1
⟧
(
s
,
h
)
↦
O
C
′
]
). Hence ¬
(
L
⊨
S
:
(
s
,
h
)
→
abort
). Now we suppose L
⊨
S
:
(
s
,
h
)
→
(
s
′
,
h
′
). In this case (
s
′
,
h
′
)
=
(
s
,
h
[
⟦
e
1
⟧
(
s
,
h
)
↦
O
C
′
]
). Therefore (
s
′
,
h
′
)
⊨
Q because (
s
,
h
)
⊨
Q
[
e
2
/
e
1
·
v
]. This completes the proof for this case.
(ii)
The case of the rule(
*
≔
o
·
f
l
): in this case
(a)
S
=
o
1
≔
o
2
·
f
(
e
),
(b)
F
C
(
f
)
=
(
p
f
,
S
f
,
e
f
),
(c)
L
⊣
{
R
[
o
2
/
this
,
e
/
p
f
]
}
S
f
{
Q
[
e
f
/
o
1
]
},
(d)
L
⊣
S
f
:
(
s
[
this
↦
s
(
o
2
)
,
p
f
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
)
→
(
s
′′
,
h
′′
),
(e)
P
⇔
o
2
↦
C
∧
R
∧
fine
(
e
,
e
f
).
Suppose that, for state(
s
,
h
)
,
(
s
,
h
)
⊨
P. This implies h
(
⟦
o
2
⟧
(
s
,
h
)
)
=
O
C. The condition fine
(
e
,
e
f
) implies (
s
[
this
↦
s
(
o
2
)
,
p
f
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
) is defined. Therefore (
s
[
this
↦
s
(
o
2
)
,
p
f
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
)
⊨
R
[
o
2
/
this
,
e
/
p
f
]. By induction hypothesis S
f does not abort at (
s
[
this
↦
s
(
o
2
)
,
p
f
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
) and therefore o
1
≔
o
2
·
f
(
e
) does not abort at (
s
,
h
). Now we suppose that o
1
≔
o
2
·
f
(
e
)
:
(
s
,
h
)
→
(
s
′
,
h
′
). By (
≔
o
·
f
s
), (
s
′
,
h
′
)
=
(
s
′′
[
o
1
↦
⟦
e
f
⟧
(
s
′′
,
h
′′
)
]
,
h
′′
). Also by induction hypothesis s
′′
,
h
′′
⊨
Q
[
e
f
/
o
1
] implying (
s
′
,
h
′
)
⊨
Q. This completes the proof for this case.
(iii)
The case of the rule(
*
≔
l
·
o
·
f
l
): in this case
(a)
S
=
o
1
≔
l
e
o
2
·
f
(
e
),
(b)
SerLay
(
L
,
l
e
,
f
)
=
L
′
=
{
l
1
,
…
,
l
m
}, for all 1
≤
i
≤
m
(
L
C
(
l
i
)
=
(
f
,
p
i
,
S
i
,
e
i
)
),
(c)
L
′
⊣
S
1
:
(
s
[
this
↦
s
(
o
2
)
,
p
1
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
)
→
(
s
2
,
h
2
),
(d)
for alli
>
1
.
L
′
⊣
S
i
:
(
s
i
[
o
1
↦
⟦
e
i
-
1
⟧
(
s
i
,
h
i
), this ↦
s
i
(
o
2
)
,
p
i
↦
⟦
e
⟧
(
s
i
,
h
i
)
]
,
h
i
)
→
(
s
i
+
1
,
h
i
+
1
),
(e)
L
′
⊣
{
R
[
o
2
/
this
,
e
/
p
1
]
}
S
1
{
Q
1
[
e
1
/
o
1
]
},
(f)
for alli
>
1
.
L
′
⊣
{
Q
i
-
1
[
o
2
/
this
,
e
/
p
i
]
}
S
i
{
Q
i
[
e
i
/
o
1
]
},
(g)
P
⇔
o
2
↦
C
∧
R
∧
fine
(
e
,
e
1
,
…
,
e
m
).
Suppose that, for state(
s
,
h
)
,
(
s
,
h
)
⊨
P. This implies h
(
⟦
o
2
⟧
(
s
,
h
)
)
=
O
C. The condition fine
(
e
,
e
1
,
…
,
e
m
) implies (
s
[
this
↦
s
(
o
2
)
,
p
1
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
) is defined. Therefore (
s
[
this
↦
s
(
o
2
)
,
p
1
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
)
⊨
R
[
o
2
/
this
,
e
/
p
1
]. By induction hypothesis S
1 does not abort at (
s
[
this
↦
s
(
o
2
)
,
p
1
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
). Now we suppose that S
1
:
(
s
,
h
)
→
(
s
2
,
h
2
). By induction hypothesis s
2
,
h
2
⊨
Q
[
e
1
/
o
1
] implying (
s
2
[
o
1
↦
⟦
e
1
⟧
(
s
2
,
h
2
), this ↦
s
2
(
o
2
)
,
p
2
↦
⟦
e
⟧
(
s
2
,
h
2
)
]
,
h
2
)
⊨
Q
1
[
o
2
/
this
,
e
/
p
2
]. Therefore by induction hypothesis S
2 does not abort at (
s
2
[
o
1
↦
⟦
e
1
⟧
(
s
2
,
h
2
), this ↦
s
2
(
o
2
)
,
p
2
↦
⟦
e
⟧
(
s
2
,
h
2
)
]
,
h
2
). Now we suppose that S
2
:
(
s
2
[
o
1
↦
⟦
e
1
⟧
(
s
2
,
h
2
), this ↦
s
2
(
o
2
)
,
p
2
↦
⟦
e
⟧
(
s
2
,
h
2
)
]
,
h
2
)
→
(
s
3
,
h
3
). By induction hypothesis (
s
3
,
h
3
)
⊨
Q
[
e
2
/
o
1
] implying (
s
3
[
o
1
↦
⟦
e
2
⟧
(
s
3
,
h
3
), this ↦
s
3
(
o
2
)
,
p
3
↦
⟦
e
⟧
(
s
3
,
h
3
)
]
,
h
3
)
⊨
Q
2
[
o
2
/
this
,
e
/
p
3
]. Therefore by induction hypothesis S
3 does not abort at (
s
3
[
o
1
↦
⟦
e
2
⟧
(
s
3
,
h
3
), this ↦
s
3
(
o
2
)
,
p
3
↦
⟦
e
⟧
(
s
3
,
h
3
)
]
,
h
3
). Hence a simple induction on m completes the proof for this case.
(iv)
The case of the rule(
sup
⁡
l
): in this case
(a)
S
=
o
≔
super
·
f
(
e
),
(b)
super
(
E
,
f
)
=
D,
(c)
F
D
(
f
)
=
(
p
f
,
S
f
,
e
f
),
(d)
L
⊣
S
f
:
(
s
[
p
f
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
)
→
(
s
′′
,
h
′′
),
(e)
L
⊣
{
R
[
e
/
p
f
]
}
S
f
{
Q
[
e
f
/
o
]
},
(f)
P
⇔
this
↦
C
∧
C
≪
E
∧
R
∧
fine
(
e
,
e
f
).
Suppose that, for states
,
h
,
(
s
,
h
)
⊨
P. This implies h
(
⟦
this
⟧
(
s
,
h
)
)
=
O
C. The condition fine
(
e
,
e
f
) implies (
s
[
p
f
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
) is defined. Therefore (
s
[
this
↦
s
(
o
2
)
,
p
f
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
)
⊨
R
[
e
/
p
f
]. By induction hypothesis S
f does not abort at (
s
[
p
f
↦
⟦
e
⟧
(
s
,
h
)
]
,
h
) and therefore o
≔
super
·
f
(
e
) does not abort at (
s
,
h
). Now we suppose that o
1
≔
o
2
·
f
(
e
)
:
(
s
,
h
)
→
(
s
′
,
h
′
). By (
≔
o
·
f
s
), (
s
′
,
h
′
)
=
(
s
′′
[
o
↦
⟦
e
f
⟧
(
s
′′
,
h
′′
)
]
,
h
′′
). Also by induction hypothesis (
s
′′
,
h
′′
)
⊨
Q
[
e
f
/
o
] implying (
s
′
,
h
′
)
⊨
Q. This completes the proof for this case.
(v)
The case of the rule(
pro
l
): it is similar to the case of (
*
≔
l
·
o
·
f
l
).


## 4. Discussion

Related Work. The most related logic to our work is that of object-oriented programs. Specifically for Java, a huge literature on specification proof techniques for object-oriented languages exists. For example, for annotated Java programs in JML (Java modeling language), [8] presents calculus for weakest precondition. An introduction to applications and tools of JML is presented in [9]. Via annotating Java source files, JML enables determining Java interfaces and classes. Considering abnormal termination resulting from failures of Java programs, [10] presents an extension to Hoare logic. For theses failures, transformational techniques do not work.Notably, dynamically growing reference-structures are involved in object-oriented programs. This results in the aliasing problem in OOP languages. Much logic treating aliasing does exist. One of these techniques is presented in [11] and reasons about linked lists which are treated using separation logic [6]. Via including global stores in the assertion language, [12] presents Hoare logic for OOP languages. However the use of this model for global storing is proved to be a potential cause of incompleteness. Classes encapsulation in an OOP language equipped with subtyping and pointers is guaranteed by aliasing restrictions in [13].The work in [14] is an example of logic achieving modular verification for OOP and focusing on corresponding methodology and object invariants. Modular verification of complex object structures was treated in [15] using an invariant class. Sound proof systems producing restricted formal justifications for OOP languages were introduced in [16, 17]. Producing a complete logical system for OOP languages is a very complex problem due to complex features of OOP languages.Interestingly, none of the techniques mentioned above treat context-oriented programs. This adds to the value of the work presented in the current paper; apparently there is no research to generalize separation logic to cover context-oriented programs.Operational semantics and type systems are presented in [18, 19] for checking and modeling context-oriented programs. The language model of [19] is structural and very similar to the model of the current paper. The language model of [18] is functional. Type systems introduced in both of these papers prevent execution of faculty functions byproceed. The operational semantics of the current paper is much simpler and powerful than semantics of [18, 19].Utilizing concepts of delegation based calculus, [20] presents operational semantics for a COP language, namely, c
j. For COP concepts as introduced in ContextJ* and ContextL, [21] introduces syntax-based semantics. Compared to the work mentioned above, a logical system that stops COP program from getting stuck is presented in the current paper. To model context-dependent behavior of COP programs, the proposed logical system is based on general calculi.Future Work. Extending the language model of the current paper to allow executing candidate functions ofproceed on priority bases is a direction for a future work. Extending the language to include layer inheritance and layer dependency is another direction for future work. Doing so allows one layer to assume the existence of another layer and allows expressing the assumption that two layers are not active at the same time.



---

*Source: 930186-2014-12-29.xml*