Information Technology Reference
In-Depth Information
and
e
is an expression; a conditional statement
d
2
,where
d
1
and
d
2
are designs and
b
is a boolean expression; a sequence
d
1
;
d
2
,where
d
1
and
d
2
are
designs; a loop
do
bd
,where
d
is a design and
b
is a boolean expression; a local
variable declaration and un-declaration
var
Tx=e
;
end
x
,where
T
is a type.
Objects are created through the command
C
.
new
(
p
), where
C
is a class type
and
p
is a navigation path. It creates a new object of type
C
whose attributes
have the initial values as declared in
C
, and attaches the new object to
p
.A
method invocation has the form
e.m(ve, re)
,where
m
is a method and
e, ve, re
are expressions. Intuitively, it first records the value of the actual value parameter
ve
in the formal value parameter of
m
, and then executes the body of
m
.Atthe
end it returns the value of the formal return parameter to the actual return
parameter
re
.
The rCOS language includes the notion of components, which provide or re-
quire contracts. A contract includes an interface (a set of field and method dec-
larations), the specification of each method and a protocol stating the allowed
sequences of method calls (for instance, for a buffer, the method
put
must be
called before the method
get
). A component provides a contract through a class,
which is the usual notion of class, where each method has to be defined using a
design. Note that the design of a method does not have to be executable in gen-
eral, only if the user wants to generate Java code, since executable rCOS designs
are quite similar to Java programs. For instance, all the following examples are
correct rCOS programs.
class
A {
int
x;
public
m(
int
v)
{
x:=v
}
d
1
b
class
B
2
{
Aa;
public
foo()
{
[
true
|−
a.x' = 1 ] ;
a.x:=a.x+1
}
class
B
3
{
Aa;
public
foo()
{
a.m(1) ; a.x := a.x + 1
}
}
class
B
1
{
Aa;
public
foo()
{
[
true
|−
a.x' = 2
∨
a.x' = 3 ]
}
}
The method
B
1
::foo
is abstract and non-deterministic: it just specifies, under the
true precondition, that the value of the field x of the field a should be either
equal to 2 or to 3. The method
B
2
::foo
mixes abstract pre/post-conditions with
a concrete assignment while
B
3
::foo
is completely concrete and could be directly
translated to Java. In this example, we can see that
B
1
::foo
is refined by
B
2
::foo
,
whichisrefinedby
B
3
::foo
. We detail in the following section the mechanization
of the notion of refinement.
}
3 Mechanized Refinement
The refinement calculus [1,17] is a program construction method, where a non-
deterministic specification is incrementally refined to deterministic code, using
Search WWH ::
Custom Search