OESPA: A Theory of Programming that Support Software Engineering

Chongyi Yuan

Wen Zhao, Sen Ma

School Of Electronics Engineering

National Engineering Research Center for Software

And Computer Science

Engineering

Peking University

Peking University

Beijing, China

Beijing, China

lwyuan@pku.edu.cn

zhaowen@pku.edu.cn , masen@pku.edu.cn

Abstract
A new theory of programming is proposed. The
theory consists of OE (Operation Expression), SP
(Semantic Predicate) and A (Axiom), abbreviated as
OESPA.
OE is for programming: its syntax is given by
BNF formulas and its semantics is defined by axioms
on these formulas. Similar to predicates in logic, SP is
for describing properties of OE (i.e. programs) and for
program property analysis. But SP is different from
predicates, it directly relates the final values of
variables upon termination of a given OE with initial
values of these variables before the same OE. As such,
it is feasible to prove or disprove whether a given SP is
a property of a given OE by computation based on A
(Axioms). SP calculus is proposed for program
specification and specification analysis, that is missing
in software engineering.

firm foundation for civil engineering. As such, a
blueprint can be approved, prior to its construction, by
computing expectable properties against user’s
requirements.
Is there a way to compute program properties
from given program text? Or, in other words, does
software engineering have a foundation comparable to
the foundation of civil engineering?
The answer is NO! Not yet for today. The fact is,
software products rely on post-development testing for
its approval. Formal methods do not help much in this
regard. For example, model checking requires a formal
model to be built from a given program in order to
prove properties of it. The consequence is, properties
proven by model checking are not necessarily
properties of the program[1,2]. They are just the
properties of the formal model.
Software engineering needs a firm foundation so
that properties of its products can be computed directly
from the products.

Key words-OE, SOE, SP, Axioms, SP Calculus, 3-step
formalism, foundation of software engineering

1.2 An investigation: formal semantics is missing from
programming languages in use
1. INTRODUCTION
1.1 Software engineering need a foundation
Mathematics, physics, dynamics etc. provide a

A programming language has a formal syntax for
its compiler, but no formal semantics for property
analysis. To be more precise, the BNF formulas that
define a programming language have no concern about

formal semantics.
For example, the two appearances of x in
“ x =: x + 1 ” would be recognized by the compiler as a
unique identifier, representing the same variable. But a
single variable is a two-facet semantic object: it
represents a memory location as well as a data stored in
that location.
The way in which variables are used by
programming languages has obscured this semantic
difference. This is why a assignment like “ x =: x + 1 ”
has always been treated as a whole in the discipline of
formal semantics, by saying that “the semantics of
x =: x + 1 ” is “an operation”, “a function”, or “a
denotation”. In Hoare logic[3,4], the same semantics is
given by assertions
∀a ∈ D :{x = a} x := x + 1{x = a + 1}

where D is the domain of x .
This observation explains why program properties
can not be computed from program text. Formal
semantics is missing in the BNF formulas that define
programming languages in use.
1.3 Predicate and program semantics
Predicates are suitable for formal description of
state properties of programs. But, state properties are
not the only thing important to program semantics. An
even more important aspect of program semantics is
how two consecutive states are related with each other.
For example, let S be a program (or program
segment) to exchange values of variables x and y . As
long as x and y hold valid data, S should do the
exchange, regardless what exact values are there in x
and y . With the predicates as the means, this property

It is clear at a glance that (2) is much simpler and
more explicit than (1). The point is, how to relate (2)
with a given program? Or, how to prove formally that
(2) is a property of S when the text of S is given?
We have proposed a new way of programming in
the last few years[6,7,8,9], in which assignments are
operations on physical object (one of the two facets of
variables) and programs are expressions consisting of
such operations and control operators. This new type of
expressions is called Operation Expression, OE for
short.
OE has a formal syntax as well as a formal
semantics, and the former is given by BNF formulas
while the latter is given by axioms based on BNF
formulas.
Semantic axioms are given in terms of two
read_operations. In addition to the conventional instant
read_operation on variables, two new read_operations
are introduced: to read a variable before or after an OE.
What obtained by such a read operation is a
mathematical expression, telling how a variable before
or after the given OE is related to initial values. To read
a variable before an OE is meaningful when that OE is
a constituent portion of another OE.
Recall the above mentioned program S . If S is
given as an OE, then x( S ) and y ( S ) , where “ ” is the
read_after operator, tell respectively how x and y after
S is related to variables before S . So, in case
x( S ) =
y ∧ y(S ) =
x (3)

is true, S does exchange the values of x and y . Note
that x( S ) and y ( S ) are computable from S (i.e. OE)

has to be given indirectly by
∀a, b ∈ D :{x = a ∧ y = b} S {x = b ∧ y = a}

of x and y upon termination of S .[5]

(1)

where D is the domain of both x and y .
A straightforward description of this property
would be
x ' = y ∧ y ' =x (2)
where x ', y ' represent respectively the final values

based on semantic axioms. Here S is considered a
stand-alone program, not part of anther OE.
If S is removed from (3), we get
x = y ∧ y = x (4)

(4) is called a semantic predicate, SP for short, x and y
are “functions” defined on OE. For any given OE, say
P , we can compute

x( P)

and

y ( P)

based on

semantic axioms on OE, and to check whether
x( P) =
y ∧ y ( P) =
x is true. (4) is a property of P if

and only if x( P) =
y ∧ y ( P) =
x is true. It is in this sense,
we say that program properties can be computed.
Recall (2) given above, (4) is as direct as (2) and
as formal as (2), but we know how to compute x and y
for a given program while there is no formal connection
between x ', y ' and a given program.
1.4 3-step formalism: how this paper is organized
A general understanding of formalism may be
stated as “to express something in precise and rigorous
mathematics”. But, this understanding does not bring
much hint with it about how to do formalism. Here we
proposed a 3-step approach as a guideline for practising
formalism. The 3 steps are: abstraction, representation
and analysis methods.
• Abstraction
Physical objects should be abstracted as
mathematical objects, based on the purpose of the
formalism in question, by forgetting physical aspects
that have on connection with the purpose.
• Representation
This step focuses on how mathematical objects
obtained by abstraction are related with each other.
Such relations usually form a mathematical system like
an equation system.
• Analysis methods
To develop and/or to apply analysis methods for
the mathematical system to solve problems raised by
the purpose of the formalism.
Formalism has focused too much on the
representation step so far, with the abstraction step

more or less overlooked. The practice of defining
programming languages is but one such example. The
purpose of our study is to propose a theory of
programming that may serve as the foundation of
software engineering, and that is comparable to the
foundation of civil engineering. To this end, we
followed the 3-step approach in practice.
• Abstraction
Programming languages in use have abstracted
memory locations as mathematical variables. A
mathematical variable allows a read operation applied
on it: whenever it appears in a mathematical expression,
the read operation is implied. This is an instant read
(the returned value is always the value currently held by
the variable) and needs no operator. To cope with the
need of programming, assignments on the variables are
introduced with “ := ” as the assign operator for most of
programming languages. But, as an operator “ := ” is not
well defined since its semantics is not formally given.
That means, the abstraction is incomplete.
We propose a complete abstraction of memory
locations as a program variable in section 2 as the basis
for BNF formulas that define the syntax of OE. Section
2 is about BNF formulas.
• Representation
A mathematical expression relates mathematical
variables with each other. An OE (Operation Expression)
defined by BNF formulas given in section 2 relates
program variables with each other. Thus, what an OE
provides is a syntactic representation.
All mathematical operators have well defined
semantics so that every mathematical expression can be
computed to yield a value. We defined semantics for
OE operators with semantic axioms in section 3, so that
every OE can be executed. Thus, semantic axioms
provide a semantic representation of how program
variables are related.
This paper focuses on sequential operation
expressions, SOE for short, while parallel operation
expressions (POE) and reactive operation expressions
(ROE) are left for separate discussion. Operators for

SOE include the write_operator (i.e. assign operator),
and control operator to form operation sequences,
choices and loops[10].
• Analysis methods
Section 4 is about theorems derived from semantic
axioms, Section 5 discusses properties of SOE and
Section 6 proposes a SP calculus for program
specification and specification analysis. These 3
sections are about methods for SOE property analysis.
Section 7 relates SP calculus with SOE specification,
Section 8 points out how to derive SOE from
specification, and section 9 talks about SOE and
software engineering: why OESPA may serve as the
foundation of software engineering. Section 10, the last
section, plans our future work and expresses our thanks
to those who have supported our research. References
are given to end this paper.
2. BNF FORMULAS FOR OE SYNTAX
2.1 Where to start
We don’t start from scratch. Data types, scalar or
structured, are well defined, syntactically and
semantically, and shared by programming languages.
OE assumes their definitions without redefining them.
It is in this sense, OE is not a complete programming
language.
Furthermore, we don’t make it explicit what data
types are included in OE. It is left for implementation
of OE to decide when it becomes mature enough for
practical use. For structured data types, array is used as
an example to show how to be included in OE. OE is
open to everything: as long as it has a well-defined
syntax and a well-defined semantics that fit in OE, it
may be included, in a nature way, as a constituent of
OE.
In the rest of this paper, the word “variable” will
mean a scalar variable, an array element or an array as a
whole, unless otherwise stated. The range of all arrays
are assumed to be [0..N ] .

2.2 Preliminary
2.2.1 Operations on variables
Let V be the set of variables in question.
There are 3 operations on a variable, namely the
write_operation,
the
read_after_operation
and
read_before_operation. The over_bar “
”, the
under_bar “ ”, and the curved under_bar

“ ” are
~

respectively the operator as given below:
: V × EM → E0 , i.e. for

x ∈ V and

e ∈ EM ,

x ∈ V and

p ∈ E0 ,

: V × E0 → EM , i.e. for x ∈ V and

p ∈ E0 ,

x(e) ∈ E0 ,

: V × E0 → EM , i.e. for
x ( p ) ∈ EM ,
~

x ( p ) ∈ EM ,

where EM is the set of mathematical expression on V

(i.e. every expression in EM contains only variables in
V ), E0 is the set of OE to be defined. These operators
are binary: “ × ” represents Cartesian product.
Let x ∈ V
x( x(e)) ∈ EM

and e ∈ EM , then x(e) ∈ E0 , and

and x( x(e)) ∈ EM . For example, let be


e ≡ x + y , then we have, by intuition, x( x( x + y )) =x + y ,

and

x( x( x + y )) =
x when


x( x + y )

is studied in

isolation. Semantic axioms specify how these operators
are related as suggested by above examples from
intuition.
2.2.2 Variable functions and Semantic predicates
From the definitions of the read_after_operation
“ ” and the read_before_operation “ ”:
~

: V × E0 → EM

= x( p ) + 1 = ( x + 1) + 1 = x + 2

where y ( p) | ( x( p) = x(q)) indicates that the initial


and
~

: V × E0 → EM

value of x before p is the final value
q.
Note from this example, x is the
value before S . x + 1 is the final value
well as the initial value before p . Thus,

We have, for every v in V :
v : E0 → EM

and
v : E0 → EM


Definition 1
1. v and v are called variable functions: v is

the final function and v is the initial function,


of x after

very initial
after q as
x + 2 is the
final value after S . The exact value of x is irrelevant
in above computation.

F_function and I_function for short respectively.
2. =
V {v | v ∈ V } , the set of all F_functions, is

Definition 2
1. A predicate R on V  V is called a semantic

called the F_set,

predicate if it contains at least one variable function
from V ;
2. A Boolean expression on V  V is called a

=
V {v | v ∈ V } , the set of all I_functions, is



called the I_set.
3. For operation expression p ,
=
V ( p ) {v( p ) | v ∈ V } , is called the F_set of p ,
=
V ( p ) {v( p ) | v ∈ V } , is called the I_set of p .


4. For operation expressions p and q ,
V ( p ) = V (q ) if and only if ∀v ∈ V : v( p ) =v(q ) ,
V ( p ) = V (q ) if and only if ∀v ∈ V : v( p ) =v(q ) ,




V ( p ) = V (q ) if and only if ∀v ∈ V : v( p ) =v(q ) .

A semantic predicate is denoted by R(V ,V ) and a
semantic Boolean expression is denoted by b . The
domain of semantic predicates is E0 since V is the
F_set defined on E0 .

Example 1

Example 2





Let

p ≡ y ( x + 1)

and q ≡ x( x + 1) be operation

semantic Boolean expression if it contains at least one
variable function from V .

R1 (V , V ) ≡ x = y ∧ y = x

,

R2 (V , V ) ≡ x ≤ y

are

expressions, where operator “ ” takes y and x + 1 ,

semantic predicates, x ≤ y , x + x =
y are semantic

respectively x and x + 1 as its first and second
operands. Let S ≡ q; p where “ ; ” is the sequential

Boolean expressions.

control operator shared by programming languages. We
have, from intuition,

it contains no variable functions. x < y is a Boolean

y ( y ( x + 1)) =x + 1 and x( x( x + 1)) =x + 1

i.e. y ( p)= x + 1 and x(q)= x + 1
In the context of S , we have
x( p )= x(q )= x + 1

and y ( S ) y=
=
( p ) | ( x( p ) x(q ))


R ≡ x+ y+z =
0 is not a semantic predicate since

expression, but not a semantic one since it has nothing
to do with V .

2.2.3 Conditional expressions
Let e1 , e2 ,..., en be expressions of the same type
and b1 , b2 ,..., bn be Boolean expressions, where n is
an integer with n > 1 .

Definition 3
1. e1 if b1 ~ e2 if b2 ~ ... ~ en if bn is called a
conditional expression, if

( B1.1) s_term ::= x(e) | A[i ](e) | A( E )
( B1.2) vs_term::= e | v(e)b

∀i, j :1 ≤ i, j ≤ n : (i ≠ j ∧ bi ∧ b j → ei =
ej )

( B1.3) es_term::= v(e1 )b1 v(e2 )b2 ...v(en )bn

∧ (b1 ∨ b2 ∨ ... ∨ bn )

2. Let l be the value of the above defined
conditional expression, then ∀i :1 ≤ i ≤ n : (bi → l =ei )
This definition ensures that every conditional
expression has a unique value if every ei , i = 1, 2,..., n ,
has a value at a given state.
A conditional expression is also called a table by
some
formal
methods
like
PVS,
where
∀i, j :1 ≤ i, j ≤ n : (i ≠ j → ¬(bi ∧ b j ))

is required. We

Remarks
 A simple_term applies write_operation on a
single variable.
 A vs_term is a variation of s_term: it is either
the special term ε , or a conditional term v(e)b .
 An es_term is an extension of a s_term: a

multiple choices for the same variable. It is required by
semantic axioms to be given that
i ≠ j ∧ bi ∧ b j → ei =
ej

have this requirement relaxed a bit here.
Conditional expressions are mainly used in
semantic axioms.

( B 2) = ( B 2.0) + ( B 2.1) + ( B 2.2) + ( B 2.3)
( B 2.0)

multi_term::=<m_term> | <vm_term> |

<am_term>
( B 2.1)

2.3 BNF Formulas
In the BNF formulas given below, v represents
either a scalar variable like x , or an array element like
A[i ] , or an array as a whole like A . All arrays are
assumed to share [0..N ] as their index range. In
addition, type match is always assumed whenever it is
required.
Conventions we follow are:
i, j : variables for array index,
n, N : integer constants, n > 0 , N > 1 ,
E : array expressions,
b : semantic Boolean expressions,
b, b1 , b2 ,..., bn , b(i ) : Boolean expressions,
e, e1 , e2 ,..., en , e(i ) : mathematical expressions
BNF formulas
( B1) = ( B1.0) + ( B1.1) + ( B1.2) + ( B1.3)
( B1.0)

<es_term>

simple_term ::=<s_term> | <vs_term> |

m_term::=simple_term  simple_term |

m_term  simple_term
( B 2.2) vm_term::=m_term b
( B 2.3) am_term::= A[i : b(i )](e(i ))

Remarks
 A multi_term applies write_operation on
more than one variable.
 A vm_term is a conditional m_term.
 An am_term is a conditional m_term for
elements of the same array.
 The operator “  ” between two simple_terms is
often omitted, just like the operator for multiplication.
( B3) = ( B3.0) + ( B3.1) + ( B3.2) + ( B3.3)
( B3.0) sequential_O_expression::=<soe> | <v_soe>
|

<r_soe>

sequential_O_expression;sequential_O_expression
( B3.1) soe::=<term> | <term>;soe
term::=simple_term | multi_term

|

( B3.2) v_soe::=soe

b

( A3.1)

v ( pq) =
v ( p ) if v ∈ V p ~ v (q ) if v ∈ Vq

for

v ∈ Vp q

n

( B3.3) r_soe::=soe | soe b

Remarks
 ”;” is the sequential control operator
 r_soe is for loops
 SOE is used as an abbreviation of
Sequential_O_expressions, and sometimes it is also
used to denote the set of all Sequential_O_expressions
when no confusion possible. Thus, SOE is a subset of
E0 .

( A3.2) ( p q )b = p b q b
( A3.3) A[i : b(i )](e(i ))
= A[0](e(0))b (0)  A[1](e(1))b (1) ... A[ N ](e( N ))b ( N )

( A4) = ( A4.1) + ( A4.2) + ( A4.3) + ( A4.4) + ( A4.5) + ( A4.6)
p, q, p1 , p2 , p3 ∈ SOE
( A4.1)
=
v ( p; q ) (=
v (q ) | V (q ) V ( p )) for all v ∈ V

( A4.2) p1 ; p2 ; p3 = ( p1 ; p2 ); p3

3. SEMANTIC AXIOMS ON SOE
Let

p, q

be SOE, i.e.

p, q ∈ SOE, and let

=
V p {v | v (e) ∈ p} be the subset of V , consisting of

variables on which p applies write_operation.
( A1) = ( A1.1) + ( A1.2) + ( A1.3) , Foundation
( A1.1)

p = q ⇔ ∀v ∈ V : v ( p )= v (q )

( A4.3) p b p if b ~ ε if ¬b
=
( A4.4)=
p n p=
if n 1 ~ p n −1 ; p if n > 1
( A4.5) p b εεε
=
if b ( ) ~ p n if ¬ b ( )
∧∃n : ( b ( p n ) ∧ ∀l : 0 < l < n : ¬ b ( p l )) ~ p; p b otherwise

( A1.2) v ∉ V p → v ( p ) =
v
( A1.3) v ∈ V → v( p ) =
v if p is in isolation.

( A2) = ( A2.1) + ( A2.2) + ( A2.3) + ( A2.4)

( A4.6) v( p; q ) = v( p ) for all v ∈ V



Remarks


v (q) | V (q) = V ( p)




p; p b

indicates that q takes
u ( p ) as the initial value of u for every u ∈ V .

simple_term
( A2.1) v (v (e)) = e
( A2.2) Vε = φ
(=
A2.3) v (e) v (e) if b ~ e if ¬b

in

( A4.5)

represents an endless

b

repetition of p . For SOE at the mean time, this is a
semantic error. We keep it as it is since we will extend
SOE to include reactive actions.

( A2.4) v (e1 )b1 v (e2 )b2 ...v (en )bn =
v (e1 ) if b1 ~ v (e2 ) if b2 ~ ... ~ v (en ) if bn

4. THEOREMS DERIVED FROM SEMANTIC AXIOMS

~ ε if ¬(b1 ∨ b2 ∨ ... ∨ bn )

Distributive
expressions:

law

on

conditional

v ( p1 if b1 ~ p2 if b2 ~ ... ~ pn if bn )
= v ( p1 ) if b1 ~ v ( p2 ) if b2 ~ ... ~ v ( pn ) if bn
( A3) = ( A3.1) + ( A3.2) + ( A3.3) multi_term

operation

Theorem 1
All axioms given with conditional expressions,
namely (A2.3),(A2.4),(A3.1),(A4.3) and (A4.4),(A4.5)
are deterministic.
Proof.
Conclusions in this theorem are ensured by (A1.1).
All those that do not fulfill this theorem, are not

semantically valid, and should be excluded from SOE.
Definition 4
A sequential

operation

expression

p

2. x ≤ y is a property of x( y ) x > y since, by (A2.3),
x( x( y ) x > y ) = y if x > y ~

,

syntactically satisfies all BNF formulas given in
subsection 2.3, is a valid SOE if and only if it is
semantically deterministic, i.e. it leads to no ambiguity
no matter which semantic axiom is applied.

x= y∧ y = x

3.

is

x if x ≤ y .

a

property

of

p ≡ x( x + y ); y ( x − y ); x( x − y )

Detailed Computations for 2 and 3:
In what follows SOE refers to only valid
sequential operation expressions.

p =x( y ) if x > y ~ ε if x ≤ y

Theorem 2
( p1 ; p2 ); p3 = p1 ;( p2 ; p3 ) for p1 , p2 , p3 ∈ SOE

Proof.
V (( p1 ; p2 ); p3 ) = V ( p3 ) | V ( p3 ) = V ( p1 ; p2 ) (A4.1)

= V=
( p3 ) | V ( p3 ) (V=
( p2 ) | V ( p2 ) V ( p1 )) (A4.1)


= (V
=
( p3 ) | V ( p3 ) V ( p2=
)) | V ( p2 ; p3 ) V ( p1 ) (A4.6)


(A4.1)
= V ( p2 ; p2 ) | V ( p2 ; p3 ) | V ( p1 )

(A4.1)
= V ( p1 ;( p2 ; p3 ))

i.e. ( p1 ; p2 ); p3 = p1 ;( p2 ; p3 )

(A1.1)

Theorem 3
(p ) = p
b1 b2

2. p ≡ x( y ) x > y ,

x( p ) = x( x( y ) if x > y ~ ε if x ≤ y )
= x( x( y )) if x > y ~ x(ε ) if x ≤ y

(by distributive law)
=
y if x > y ~ x if x ≤ y

(A2.1),(A2.2),(A1.2)

i.e. x( p) ≤ y
3. p ≡ x( x + y ); y ( x − y ); x( x − y )
=
( x( x + y ); y ( x − y )); x( x − y )

b1 ∧ b2

(A2.3)

(A4.2)

(A4.3)
x( x( x + y )) =x + y, y ( x( x + y )) =y (A2.1),(A1.2)

Corollary 1 for terms
1. εε
(A3.1)
=
 p p=

p
2. p p = p
(A3.1)
3. pq = q p
(A3.1)
4. ( p1  p2 ) p3 = p1 ( p2  p3 )

so,
x( x( x + y ); y ( x − y ))
=
( x( y ( x − y )) | x =+
x y, y =
y ) (A4.1)


= x+ y

(A3.1)

5. PROPERTIES OF SOE
Definition 5
R(V , V ) is a property of

p ,

p ∈ SOE , if

y ( x( x + y ); y ( x − y )) =( y ( y ( x − y )) | x =x + y, y =y )


= ( x + y) − y = x

R(V ( p ), V ) , i.e. p makes R(V , V ) true.

Thus,

Example 3

x( p) =
x( x( x − y )) | x =+
x y, y =
x


= ( x + y) − x = y

1. x = y is a property of x( y ) since x( x( y )) = y
by (A2.1).

y( p) =
y ( x( x − y )) | x =+
x y, y =
x



=x

then
1. stable( R '(V ) ) ∧ R '(V ) → R '(V ( p))
2. inherit( R '(V ) ) ∧ R '(V ) → R '(V ( p))
3. traceable( R '(V ) ) ∧ ¬R '(V ) → ¬R '(V ( p))

Definition 6
Semantic predicate R(V ,V ) is bipartite if it takes
the
form
,
where
R(V , V ) ≡ R '(V ) op R '(V )
op ∈ {=, <, ≤, >, ≥, →, ←} and R '(V ) , R '(V ) share the
same structure with variables from V and V
respectively.
Note that op is a binary transitive operator, “ → ”
is the “implies” operator and “ ← ” is the “implied by”
operator.

The proof is straightforward from Definition 7.
Definition 8
A semantic predicate is a state predicate if it
contains only variable functions. A state predicate R
is denoted by R(V ) .
Example 5

Example 4

R1 (V ) ≡ x + y + z =
100 ,

R1 (V , V ) ≡ x + y + z = x + y + z

and

,

R3 (V , V ) ≡ x + y > 0 ← x + y > 0

R2 (V , V ) ≡ x < x

are

Definition 7
If bipartite R(V ,V ) ≡ R '(V ) op R '(V ) is a property
of p , then R '(V ) is said to be, as shown by the table
below, stable, inheritable, traceable, respectively,
constant, decreasing, not increasing, increasing and not
decreasing. Such R '(V ) will be denoted by,
respectively, stable( R '(V ) ), inherit( R '(V ) ),
traceable( R '(V ) ), const( R '(V ) ), dec( R '(V ) ),
not_inc( R '(V ) ), inc( R '(V ) ) and not_dec( R '(V ) ).
R '(V ) ∈ EL

op

=

stable
inheritable
traceable

=

are

state predicates.

bipartite.

R4 (V , V ) ≡ x < y ← x < z is not bipartite.

op

R2 (V ) = x ≤ y ∧ y ≤ z

R '(V ) ∉ EL

constant
←
<
decreasing
→
≤
not increasing
>
increasing
EL :Set of logic expression
≥
not decreasing
Table 1 R '(V ) op R '(V ) is a property of p
Theorem 4
If R(V ,V ) ≡ R '(V ) op R '(V ) is a property of p ,

Definition 9
1. R(V ) is an invariant of
p , if
R (V (ε )) ∧ R (V ( p )) .
2. R(V ) is a conditional property of p if there
exists a state predicate
such that
Q(V )
Q(V (ε )) → R(V ( p )) . Q(V ) is called the condition of
( R(V ), p ) .
Example 6
1. Let be

p ≡ x( x + 1) y ( y − 1) ,

R1 (V ) ≡ x + y + z =
100

and R2 (V ) ≡ x + y + z , then R1 (V ) is an invariant of p
if x + y + z =
100 initially, and R2 (V ) is a constant of
p regardless x + y + z =
100 or not. Note R2 (V ) is
itself not a predicate.
2.

Q(V ) ≡ x ≤ y ∧ x ≤ z

is

the

condition

for

(( y ( z ) z ( y )) y > z , x ≤ y ∧ y ≤ z ) .

Definition 10
State predicate R(V ) is irrelevant to p , p ∈ SOE ,

if and only if VR  V p = φ where =
VR {v | v ∈ R(V )}

=
v(q; p ) v=
( p )|V ( p ) V (q ) by (A4.1)

For variable x that appears in v( p) , we know
x ∉ Vq thus x(q ) = x , i.e. x( p ) = x . Since x is an


and
=
V p {v | v(e) ∈ p} .

arbitrary variable appearing in v( p) , we know
Example 7
R (V ) ≡ x ≤ y is irrelevant to =
p z ( x + y ) , since

Theorem 6
1. If R(V ) is an invariant of p , then R(V ) is

VR = {x, y} and V p = {z} .

also an invariant of p n for n > 1 .

Corollary 2
If
R (V )

is irrelevant to
then
p ,
v ∈ VR → v( p ) =
v and thus R (V ( p )) = R (V ) , where
R (V ) is obtained for R (V ) by replacing every
variable function v with the variable v .

R(V ) ≡ x ≤ y and =
p z( x + y) ,

2. If there exists n , n ≥ 0 , such that p b = p n by
(A4.5), then b is a property of p b , and every
invariant of p is also invariant of p b .

Example 8
For

(v( p )|V=
( p ) V=
(q )) v( p )

so, v(q; p) = v( p) .

we have

x( p ) = x and y ( p ) = y . Thus, R (V ( p )) ≡ x( p ) ≤ y ( p ) ,

i.e. R(V ( p)) ≡ x ≤ y .
Theorem 5
1. If R(V ) is a conditional property of p with
Q(V ) as the condition of ( R(V ), p ) , R (V ) is
irrelevant to q and Q(V ) is a property of q , then
R (V ) is a property of q; p .
2. If R(V ) is a property of q and it is irrelevant
to p , then R(V ) is a property of q; p .
3. If R(V ) is an invariant of both q and p ,
then R(V ) is a property of q; p , or to be more precise,
R (V ) is also an invariant of q; p .
4. For v ∈ V p , if v( p) contains no variable in Vq

Proof. Direct consequence of Theorem 5.
Example 9
i −1

Let p =+
i (i 1)m(m + A[i ]) , then R(V ) ≡ m =
∑ A[l ]
l =0

is an invariant of p n for n , 0 < n ≤ N , if initially
i =1 ∧ m =A[0] . It’s easy to compute that i ( p N =
) N +1
N

and m( p N ) = ∑ A[l ] , i.e. q; p N is a program to
l =0

compute the sum of array elements for array A , where
q = i (1)m( A[0]) .

Note that array A is not changed by p , i.e. for
any index l , A[l ]( p) = A[l ] (or A( p)[l ] = A[l ] ). As such
i −1

R (V ) can be written as R '(V , V ) ≡ m =
∑ A[l ] , and say
l =0

then v(q; p) = v( p) .
Proof.
1, 2 and 3 are direct consequences of relevant
definitions.
For conclusion 4,

R '(V , V ) is an invariant of p and p N . The difference

between R(V ) and R '(V ,V ) in this example is that
the former is a state predicate and the latter is not. From
now on we relax the definition of an invariant to

include semantic predicates like R '(V ,V ) .

serve the need of SP calculus.

Example 10
Let p , q and R '(V ,V ) as given in example 9. By
theorem 6 we know R '(V ,V ) is also an invariant of

Definition 11
A predicate

N

p b where b ≡ i = N + 1 , and m( p b ) = ∑ A[l ] , as long as
l =0

i =1 ∧ m =A[0]

initially, i.e. i ( p b ) =
1 ∧ m( p b ) =
A[0] .




So, q; p b is also a program to compute the sum of all

R

defined on V  V  V

is a



semantic predicate, SP for short, if it contains no
contradiction.
Apparently, all semantic predicates satisfying
Definition 2 remain to be semantic predicates by
Definition 11. All semantic predicates takes SOE as
their domain since V , V are respectively the F_set


and I_set defined on SOE.

elements of array A .

6. SP CALCULUS
SP calculus is developed mainly for program
specification and specification analysis based on
semantic axiom (A 1.2) , (A 4.1) and (A 4.6) .
A noticeable fact is , the write_operation (i . e
assignment) is the only operation that changes a
program state . Thus for a complete program
specification , there must be an expression ev for an
arbitrary variable v such that v = ev is derivable
from it ,where ev contains only variables in V , no
variable function from V . SP calculus tries to capture
the process of deriving v = ev for all v in V , from
a given specification . A specification is called a SP
formula in this calculus.

6.1 Semantic Predicates (SP)

Example 11
x < x , x < x ∧ x < x are contradictions.


We write v ∈ R for semantic predicate R if v
appears in R . Similarly, we write v ∈ R and v ∈ R .
Let be
=
VR {v | v ∈ R} , =
VR {v | v ∈ R} and
=
VR {v | v ∈ R} .

 

Definition 12
R is said to be V _free , V _free and V _free

respectively , if VR = φ , VR = φ or VR = φ .

R is said to be V _complete , V _complete and
V _complete respectively , if VR = V , VR = V and

VR = V .




6.2 SP formulas and computation Rules
SP is the simplest formula.
Definition 13
SP_formula ::= SP | SP; SP_formula
In what follows, a SP_formula will be called a
formula .
For R , R is not V _complete , we have , by

The concept of semantic predicates was defined
earlier by Definition 2. But, axiom (A 4.1) indicates
that I_functions v for v ∈ V are needed in the process

Axiom (A 1.2) ,

of reasoning. Thus, we will extend the definition to

Computation Rule 1: Extension





v ∉ R → R ≡ (R ∧ v =
v) .

ind ( R1 , R2 ) ≡ y =
cos x .

We now develop computation Rules for structured
formulas, i.e. for ( R1 ; R2 ) and ( R1 ; F ) where R1 ,
R2 are SP while F is itself a formula .

Definition 15
Let R1 , R2 be V _free . R1 is said to be


For given R , R is a SP without saying , let
R(V , V ) denote what is obtained by replacing

every appearance of v in R with v for all v ∈ V ;

R(V , V ) denote what is obtained by replacing

every appearance of v in R with v for all v ∈ V ;

R(V , V ) denote what is obtained by replacing

every appearance of v in R with v for all v ∈ V ;

complete with respect to R2 if VR ⊇ VR and for every

Example 12

Example 14



For

R≡x=
x2



, we have



R (V , V ) ≡ x =
x2



,

1

v ∈ V , an equation v = ev is derivable from R1 (V , V )
 


such that ev contains only variable from V and

R2 (V , V ) | R1 (V ,V ) represents a substitution in R2 (V , V )



that every appearance of v is replaced by ev for

every v ∈ V .
 

Let be R1 ≡ { x, y, z} =
{x, y, z} ,
R2 ≡ { x , y, z} =
{x, y, z} ,

R (V , V ) ≡ x =
x 2 and R (V , V ) ≡ x =
x2 .




2

we have : V=
V=
{ x , y, z}
R
R
1

2

and R1 (V ,V ) ≡ {x, y, z} =
{x, y, z} ,


Theorem 7
R (V , V ) and


R (V , V ) are both SP if R is V



_free .
Proof

VR = φ ensures that both R (V , V ) and R (V , V ) are




contradiction free .

Let R1 , R2 be both V _free SP .


Definition 14
1. R1 is said to be independent of

R2

if

VR1  VR2 = φ .

2. If R1 is not independent of R2 , then R ' is said
to be the independent portion of R1 with respect
to R2 if R ' is the maximum portion of R1
such that VR '  VR = φ . This fact is denoted by
1

2

R '1 = ind ( R1 , R2 ) .

Example 13
R1 ≡ x= sin x ∧ y= cos x

,

R2 ≡ x =x

,

then

  

R2 (V , V ) ≡ { x , y, z} =
{x, y, z} and

  
R2 (V , V ) | R1 (V ,V ) ≡ { x , y, z} =
{x, y, z} .



Thus,

R1

is

complete with respect to R2 .
Note that both R1 and R2 require some sorting of
x, y, z . Thus, R1 ; R2 requires one sorting after another,
and is itself a sorting . This example explains why we
have Definition 15 : preparing for a rule applicable to
formula R1 ; R2 . Definition 15 requires only the existence
of ev , not the precise expression ev .
Computation Rule 2: Resolution
If R1 is complete with respect to R2 , then
R1 ; R2 → R1 '∧ ( R2 (V , V ) | R1 (V , V )) where R1 ' ≡ ind ( R1 , R2 )








Semantic axiom(A 4.1) is the foundation of this
rule .
An obvious conclusion is :
Theorem 8
If R1 is complete with respect to R2 , then
R1 '∧ ( R2 (V , V ) | R1 (V , V )) is V _free .


Example 15
Let be R1 ≡ x = x + y ∧ y = y and R2 ≡ y = x − y ,we
have ind ( R1 , R2 ) ≡ x = x + y , R1 (V ,V ) ≡ x = x + y ∧ y = y ,






By Computation Rule 1 we know R1 ' ≡ R1 , by
Computation Rule 4 we know R1 '; R2 ≡ R1 ; R2 ,so
R1 '; R2 ; R3 ≡ R1 ; R2 ; R3 .That is, R1 '; R2 ; R3 is as good as
R1 ; R2 ; R3 .
Theorem 9
R1 ; R2 ; R3 ; R4 ≡ ( R1 ; R2 );( R3 ; R4 )

R2 (V , V ) ≡ y = x − y and R2 (V , V ) | R1 (V , V )

 



Proof

≡ y = ( x + y) − y ≡ y =
x .By Computation Rule 2:

R1 ; R2 ; R3 ≡ ( R1 ; R2 ); R3

R1 ; R2 → ind ( R1 , R2 ) ∧ ( R2 (V , V ) | R1 (V ,V )) ,


i.e. x = x + y ∧ y = y; y= x − y → x = x + y ∧ y = x .

R1 ; R2 ; R3 ; R4 ≡ ( R1 ; R2 ); R3 ; R4
( R1 ; R2 ); R3 ; R4 ≡ ( R1 ; R2 );( R3 ; R4 )

In the same way we can prove x = x + y ∧ y = x;

(Rule 3)
(Rule 4)
(Rule 3)

Thus, R1 ; R2 ; R3 ; R4 ≡ ( R1 ; R2 );( R3 ; R4 )
Note that Rule 2 reduces R1 ; R2 to a single SP ,Rule
3 allows to apply Rule 2 more than once to reduce any
formula to a single V _free SP. Rule 4 let us do the

x = x− y → x = y∧ y = x .



This example concludes that x = x + y ∧ y = y; y= x − y;
x = x− y → x = y∧ y = x ,

i.e. x = x + y ∧ y = y; y = x − y; x = x − y is a specification

reduction in parallel. It is important to notice that all
actual reductions always reduces two SP’s to a single
V _free one, and the two SP’s to be reduced must

satisfy the requirement that “ R1 is complete with
respect to R2 ”.
To ensure such completeness, we define the
concept of reducible formulas.

of a program that exchanges the values of x and y .
But, to derive this conclusion formally, we need the
Computation Rule below:
Computation Rule 3: Association
R1 ; R2 ; R3 ≡ ( R1 ; R2 ); R3

Definition 16
A SP formula R1 ; R2 ;...; Rn , n ≥ 2 ,is reducible if
R1 ; R2 can be reduced to a single SP and
( R1 ; R2 ); R3 ;...; Rn is reducible.
With this concept, we have

R1 ; R2 ; R3 ≡ R1 ;( R2 ; R3 )

Theorem 2 in Section 4 is the foundation of this rule.
People would prefer to take R ' ≡ x = x + y instead
of

R1 ≡ x = x + y ∧ y = y as

the

first

SP in

the

specification in Example 15. But, R1 ' is not complete
with respect to R2 . To prove R1 '; R2 ; R3 is as good as
R1 ; R2 ; R3 as a specification of exchanging values of x
and y , we need the next computation rule:

Theorem 10
1. All reducible formulas can always be reduced to a
single V _free SP.


2. Reducible formulas comply with associative law.
The second part of this theorem can be proved in
the way Theorem 9 is proved. The first part is a direct
conclusion from Definition 16.
Example 16

Computation Rule 4: substitution
R1 ≡ R1 '∧ R2 ≡ R2 ' → R1 ; R2 ≡ R1 '; R2 '

f ≡ x ≤ y; x ≤ z; y ≤ z may be taken, by many, as a

specification of sorting x, y, z into ascending order.
But this formula is not complete. The OE program
x(1) y (2); x(3) y (4); y (1) z (2)

satisfies f . But this OE ends up at x = 3 ∧ y =1 ∧ z = 2

x ≤ y ∧ z = z ∧ {x, y, z} = {x, y, z}
  
  
and R2 (V ,V ) ∧ R(V ,V ) ≡


x ≤ z ∧ y = y ∧ {x, y, z} = {x, y, z} ,
  


by Rule 2:
and x, y, z have nothing to do with their initial values
and they are not in ascending order.
Example 18 in next section will suggest a correct
specification for sorting x, y, z into ascending order.
Example 17

f ' → x ≤ z ∧ y = y ∧ {x, y, z} = {x, y, z}
  

| x ≤ y ∧ z = z ∧ {x, y, z} = {x, y, z}
  
  
≡ x ≤ z ∧ { x, =
y, z} {x, y, z} ∧ x ≤ y .

where x ≤ y is obtained in the following way:

For R1 ≡ x =
sin x , R2 ≡ x =
x and R3 = x ,we have
3

R1 ; R2 ≡ x =
(sin x)

3

,

( R1 ; R2 ); R3 ≡ x =(sin x)

3

and

R2 ; R3 ≡ x =x 3 , R1 ;( R2 ; R3 ) ≡ x =(sin x)3 .

7. SP CALCULUS AND SPECIFICATION ANALYSIS

leads to x ≤ y .

Examples are used in this section to illustrate how
to do specification analysis with SP calculus.
Examples 15-17 given in section 6 have in fact
shown the function of SP calculus in specification
analysis as long as all those formulas are considered as
program specifications.
Specification process includes a phase for
refinements.

x= y∧ y = x

x =+
x y; y =−
x y; x =−
x y .

can

be

refined

The

former

x ≤ z ∧ y = y ∧ {x, y, z} = {x, y, z}
  

→ x ≤ z ∧ {x, z} =
{x, z}
 
→ x ≤ x , since x is the smaller one in the set.

But, x ≤ y and y = y , so x ≤ y . Thus x ≤ x
 




to

indicates

That is, f ' is complete, and
f '→ x≤ y∧x≤ z∧R.

Similarly we can prove that
R1 ∧ R; R2 ∧ R; R3 ∧ R → x ≤ y ∧ y ≤ z ∧ R .

This is a proper specification of a sorting program.
Example 19
f (n) ≡ i =1 ∧ f =1;(i =i + 1 ∧ f =f i ) n

“WHAT” is wanted and the latter tells “HOW” to do it.
Example 18
Let be R ≡ {x, y, z} =
{x, y, z} , R1 ≡ x ≤ y ∧ z =
z ,
R2 ≡ x ≤ z ∧ y =
y and R3 ≡ y ≤ z ∧ x =
x , we first prove

that f ' ≡ R1 ∧ R; R2 ∧ R is a complete SP formula.
Since R1 (V ,V ) ∧ R(V ,V ) ≡




is a specification for the program to compute n !
for n ≥ 1 ,
since
f ( n) → f = n ! ∧ i = n + 1

If we take the Boolean constant True as a SP, and
for R , R is an arbitrary SP, define R 0 = True, then
f (n) can be relaxed to allow n = 0 . We have, by Rule

0.

2:
f (0) → i = 1 ∧ f = 1

since i =1 ∧ f =1 is

independent of True. i.e. f (0) → f =
0!
The prove of f (n) → f = n ! ∧ i = n + 1 requires the

intended meaning:
l < 9 ∧ i ≥ 0 → A[i ] =l

is a candidate for the

(i + 1)th queen.
l=
8 → A[0..i − 1] is not part of next solution.
i =−1 → no more solution
i ≥ 0 → A[0..i − 1] may be part of next solution.

application of mathematical induction.

We need two predicates:

Example 20
A specification in terms of SP calculus will be
proposed for the 8_Queen Problem.
The first step towards a formalization of this
problem is to do abstraction: to find a mathematical
representation of physical objects involved, namely the
chess board and the queens on the board.
To keep data structure as simple as possible, we
use an array as the abstraction of the board, i.e. array
whose elements take values from
A[0..7]
{0,1, 2,3, 4,5, 6, 7} , and A[i ] = j denotes that a queen is
placed at (i, j ) on the board.
The second step is to represent in terms of A[0..7]

i, 0 ≤ i ≤ 8

R( A, i ) ≡ ∀j , k : 0 ≤ j , k < i :: peace( A, j , k )

what the problem is required: to place 8 queens on
board such that they stay in peace, i.e. no one is in a
position to kill anyone else. For two queens A[i ] = l
and A[ j ] = k , they can not kill each other if and only if
l ≠ k ∧l −k ≠ i − j ∧l −k ≠ j −i

i.e. A[i ] ≠ A[ j ] ∧ A[i ] − A[ j ] ≠ i − j ∧ A[i ] − A[ j ] ≠ j − i .
We denote this with peace ( A, i, j ) , i.e.
peace ( A, i, j )
≡ A[i ] ≠ A[ j ] ∧ A[i ] − A[ j ] ≠ i − j ∧ A[i ] − A[ j ] ≠ j − i

The third step is to propose a solution.
There are two ways to understand this problem: to
find one solution for the 8 queens, or to find all
solutions for the 8 queens. The auxiliary variables
proposed next aim at all solutions.
Auxiliary variables:
i, l : integer with −1 ≤ i ≤ 7 and 0 ≤ l ≤ 8 .
P : array[0..7] of integer whose element set is
{0,1, 2,3, 4,5, 6, 7} .
Q : constant array[0..7] with all elements being

,

for

H ( A, i, l ) ≡ ( A[i ] =
l → R( A, i + 1))

We have
R( A,8) → ( A is a solution )

Specification for finding one solution:
Let be
R0 ≡ i =1 ∧ l =0 ∧ P =Q ∧ A =Q
R1 ≡ l = 8 ∨ (l < 8 ∧ H ( A, i, l ))
R2 ≡ l < 8 → A[i ] =
l
R3 ≡ (i = 7 ∧ l < 8 → P = A)
⊕(i < 7 ∧ l < 8 → i = i + 1 ∧ l = 0)
⊕(i > 0 ∧ l = 8 → i = i − 1 ∧ l = A[i − 1] + 1)
⊕(l =8 ∧ i =0 → i =−1)

The solution is
R0 ;( R1 ; R2 ; R3 ) P ≠ Q ∨ i =−1

This solution includes a formula ( R1 ; R2 ; R3 ) P ≠ Q ∨ i =−1 ,
and this formula can not be derived from the definition
of SP_formulas. We may extend the definition to
include this, but we didn’t. We have treated R n as an
abbreviation of R; R;; R for simplicity. R b , where
b is a SP, can also be viewed as an abbreviation of
R; R;; R , with a flexible times of repetition of R . If
this repetition does not lead to b , R b is not a right
formula. For one solution,

P ≠ Q ∨ i =−1

can be

reached, since when A is considered as an octal
number, A < A is derivable from ( R1 ; R2 ; R3 ) n for
some n unless P ≠ Q ∨ i =−1 .

P ≠ Q denotes the fact that P is a solution, and
i = −1 means that there is no solution.

Specification for finding all solutions:
Let be
R3 ' ≡ (i = 7 ∧ l < 8 → P = A ∧ l = A[6] + 1 ∧ i = 6)
⊕(i < 7 ∧ l < 8 → i = i + 1 ∧ l = 0)
⊕(i > 0 ∧ l = 8 → i = i − 1 ∧ l = A[i − 1] + 1)
⊕(l =8 ∧ i =0 → i =−1)

The solution is
R0 ;( R1 ; R2 ; R3 ')i = −1

and each time P is changed, a new solution is found.
Note that the difference between a specification
and a program is that a program consists of details of
operations while a specification contains only the result
of these operations. For example, R1 demands l to
be either l = 8 , or l < 8 ∧ H ( A, i, l ) , it does not tell how
to achieve the goal.

8. HOW TO DEVELOP SOE FROM GIVEN
SPECIFICATIONS
The SOE for x = y ∧ y = x is x( y ) y ( x)
The SOE for x =+
x y; y =−
x y; x =−
x y is
x( x + y ); y ( x − y ); x( x − y )

The SOE for x ≤ y ∧ R; x ≤ z ∧ R; y ≤ z ∧ R , where
R ≡ {x, y, z} =
{x, y, z} , is
( x( y ) y ( x)) x > y ;( x( z ) z ( x)) x > z ;( y ( z ) z ( y )) y > z

The SOE for i =1 ∧ f =1;(i =i + 1 ∧ f =f * i ) n is
i (1) f (1);(i (i + 1) f ( f * i )) n .

The SOE for the 8_Queen problem is:

SOE for R0 : P0 ≡ i (1)l (0) P(Q) A(Q)
SOE for R1 : P1 ≡ (l (l + 1))l =

8 ∨ H ( A, i , l )

SOE for R2 : P2 ≡ A[i ](l )l <8
SOE for R3 :
P4 ≡ P( A)i = 7 ∧ l = 8 (i (i + 1)l (0))i < 7 ∧ l = 8 
(i (i − 1)l ( A[i − 1] + 1))i > 0 ∧ l = 8 i (−1)l = 8∧ i = 0

SOE for R3 ' :
P4 ≡ ( P( A)i (6)l ( A[6] + 1))i = 7 ∧ l = 8 
(i (i + 1)l (0))i < 7 ∧ l = 8 (i (i − 1)l ( A[i − 1] + 1)i > 0 ∧ l = 8 (i (−1))l = 8∧ i = 0

SOE for one solution P0 ;( P1 ; P2 ; P3 ) P ≠ Q ∨ i =−1
SOE for all solutions P0 ;( P1 ; P2 ; P4 )i = −1
Apparently, it is not difficult to develop a SOE
from a given SP_formula since for R ( R is a SP), VR
is the set of variables that require a simultaneous write
operation.
The analysis of the specifications for the 8_Queen
problem has been omitted here to save space. In fact,
this problem is among those that are used for
demonstration of prototype tools developed in our lab
for SOE analysis.
The prototype tools are in fact a SOE property
verifier capable to do semi_automatic SOE analysis
(human interfere is needed when, say, mathematical
induction is required). A SOE may be re_structured as a
tree, called analysis tree, whose intermediate nodes are
control operators for operation sequences, choices and
loops, while leaf nodes are SOE Terms. We go no
further here on these tools since this paper focuses on
OESPA, the theory itself.
Advantages of SOE and SP calculus include:
• SOE is syntactically formal as well as
semantically formal. As such, properties can be

computed from SOE texts.
• SP, i.e. semantic predicates, and SP formulas
provide a firm foundation for program specification,
since direct descriptions of how consecutive program
states are related become feasible. SP calculus has made
specification analysis practical.
• Specification in SP formulas let users focus on
WHAT instead of HOW, since operation details are left
for later consideration.
To end this section, we have the following
definition:
Definition 17
A SOE developed from a given reducible SP
formula is correct if and only if the given formula is a
property of it.
Note that, in our theory OESPA, a SOE is a
program, a reducible SP formula is a program
specification, and a reducible SP formula can always be
reduced to a single SP.
9. SOE AND SOFTWARE ENGINEERING
The software industry depends heavily on software
engineering. But software engineering relies on
post-development testing for the quality of its products.
It is impossible, at least for the time being, to have
SOE as the main means of programming. But SOE and
SP_calculus provide a formal foundation for software
engineering. With the help of SOE and SP calculus,
programmers may better understand what programming
is about.
We wish to have a programming language that has
a BNF definition similar to programming languages in
wide use, but potentially equivalent to the BNF
definition of SOE. In this way, software qualities may
be guaranteed with testing being of second importance
only.
We have applied our theory to develop tools for
the analysis of C pointers. It has turned out to be very
helpful. It leads us to a systematical way of thinking,
and makes it possible to develop a C-pointer analysis

prototype tool within half a year.

10. FUTURE WORK
This paper focused on SOE, sequential operation
expression. We will have POE and ROE proposed in
the future: POE is an abbreviation for Parallel
Operation Expression while ROE, an abbreviation for
Reactive Operation Expression.
Parallelism is the only means to promote software
efficiency and to make full use of super computers.
Reactive systems are important for computer
applications in the area of management and control.

ACKNOWLEDGMENTS
We are grateful to the National Engineering
Research Center For Software Engineering of Peking
University, Beijing Beida Software Engineering
Development Company for their continuous support.
Thanks to everyone in our lab among them Mr. Zhang
Hang has helped us with typesetting. The authors are
sponsored by the National Basic Research Program of
China (973) No.2009CB320706.
REFERENCES
[1] Emerson Clarke, Formal Methods: State of the
Art and Future Directions [R]. VeriSign Inc,
Mountain View, CA, 2004.
[2] E.M. Clarke, O. Grumberg, and D.A. Peled, Model
Checking[C]. MIT Press, 1999.

[3] Hoare C A R. Communicating sequential
processes[M]. Prentice Hall，1985.
[4] Hoare C A R. An axiomatic basis for computer
programming[J]. Communications of the ACM,
1969, 12(10): 576-580.
[5] C.A.R.Hoare, HeJifeng. Unifying Theories of
Programming[M].Prentice Hall International，1998
[6] Chongyi Yuan, Assignment ： Operation on a

physical

object[J].

Journal

of

Frontiers

of

Computer Science and Technology，2008，2（5）
：
487-499.

[7] Chongyi Yuan, Huang Yu, Zhao Wen. 2009.
Program:Expressions of Operations On
Physical Objects. Journal of Frontiers of
Computer Science and Technology. 2009
Vol.3(2):144-153.
[8] Chongyi Yuan, Zhao Wen, Gao Xin, Huang Yu.
2010. Definitions and Specifications of
O-expression properties. Journal of Frontiers
of Computer Science and Technology. 2010
Vol.4(1):20-28.
[9] Chongyi Yuan, Wen Zhao, Yu Huang. Operation
Expression: A Way to Verified Software. The 2010
International

Conference

on

Foundations

of

Computer Science (FCS2010, WORLDCOMP’10),
Las Vegas Nevada, USA, 2010, 91-96.
[10] Dijkstra E W. Letters to the editor: go to statement
considered harmful[J]. Communications of the
ACM, 1968, 11(3): 147-148.

