Ta
.
p ch´ı Tin ho
.
c v`a Diˆe
`
u khiˆe
’
n ho
.
c, T.21, S.3 (2005), 261—270
M
ˆ
O H
`
INH DA
.
I S
ˆ
O
´
QUAN H
ˆ
E
.
CU
’
A H
ˆ
E
.

C
1
, NGUY
ˆ
E
˜
N V
˘
AN VY
.
2
, D
˘
A
.
NG V
˘
AN D
´
U
.
C
3
1
Khoa To´an, Tru
.
`o
.
ng
Da

´
c gia H`a Nˆo
.
i
3
Viˆe
.
n Cˆong nghˆe
.
thˆong tin
Abstract. This article presents semantics of object oriented system with classes, visibility, dynamic
binding and recursive methods. The class declarations and commands are served as designs in terms
of pre- and post conditions; the relations of components in system This approach shows clearer
relations of components in object oriented system, possibility of using tools and cheecking method to
improve the refinement for further development of systems. The algebraical laws are expanded for
design specification of object oriented programs.
T´om t˘a
´
t. B`ai b´ao tr`ınh b`ay ng˜u
.
ngh˜ıa cu
’
a hˆe
.
thˆo
´
ng hu
.
´o
.

quy. C´ac khai b´ao l´o
.
p v`a c´ac lˆe
.
nh nhu
.
l`a c´ac thiˆe
´
t kˆe
´
du
.
.
a trˆen
tiˆe
`
n
diˆe
`
u kiˆe
.
n, hˆa
.
u diˆe
`
u kiˆe
.
n v`a c´ac mˆo
´
i quan hˆe

´o
.
ng
dˆo
´
i tu
.
o
.
.
ng, v`a
c´ac kha
’
n˘ang su
.
’
du
.
ng c´ac cˆong cu
.
v`a c´ach th´u
.
c kiˆe
’
m tra
dˆe
’
ca
’
i tiˆe

c ph´at triˆe
’
n ´ap du
.
ng cho viˆe
.
c
d˘a
.
c ta
’
chu
.
o
.
ng tr`ınh hu
.
´o
.
ng
dˆo
´
i
tu
.
o
.
.
ng.
1. GI

ng
dˆo
´
i tu
.
o
.
.
ng l`a rˆa
´
t ph´u
.
c
ta
.
p [1, 5]. Nhiˆe
`
u nh`a nghiˆen c´u
.
u chı
’
ra su
.
.
cˆa
`
n thiˆe
´
t ph´at triˆe
’

’
u c´ach th´u
.
c lˆa
.
p
tr`ınh du
.
.
a trˆen l´y thuyˆe
´
t cu
’
a Hoare v`a He [2], d`ung v`ao viˆe
.
c xˆay du
.
.
ng mˆo
.
t c´ach
d´ung d˘a
´
n c´ac
chu
.
o
.
ng tr`ınh hu
.

cu
’
a ngˆon ng˜u
.
lˆa
.
p tr`ınh hu
.
´o
.
ng
dˆo
´
i tu
.
o
.
.
ng v´o
.
i c´ac l´o
.
p, t´ınh r˜o r`ang, liˆen kˆe
´
t
dˆo
.
ng, c´ac phu
.
o

’
u
du
.
o
.
.
c bo
’
qua ([2, 6]).
O
.
’
dˆay, viˆe
.
c khai b´ao l´o
.
p v`a c´ac lˆe
.
nh xem nhu
.
l`a c´ac thiˆe
´
t kˆe
´
. V´o
.
i c´ach tiˆe
´
p cˆa

´
n cu
’
a c´ac kiˆe
’
u d˜u
.
liˆe
.
u nguyˆen thu
’
y vˆa
˜
n nhˆa
.
n c´ac gi´a tri
.
tu
.
o
.
ng ´u
.
ng v´o
.
i kiˆe
’
u cu
’
a

c
t´ınh v´o
.
i t´ınh
dˆe
.
quy. Phu
.
o
.
ng th´u
.
c
du
.
o
.
.
c coi nhu
.
l`a thiˆe
´
t kˆe
´
v´o
.
i tˆa
.
p c´ac tham sˆo
´

di
.
nh
d´ung(well definedness) cu
’
a d˘a
.
c ta
’
. Trong tru
.
`o
.
ng ho
.
.
p chung, chu
.
o
.
ng tr`ınh
du
.
o
.
.
c mˆo h`ınh h´oa
b˘a
`
ng thiˆe

NH D
´
U
.
C, NGUY
ˆ
E
˜
N V
˘
AN VY
.
,
D
˘
A
.
NG V
˘
AN D
´
U
.
C
v`a thiˆe
´
t kˆe
´
D d´ong vai tr`o nhu
.

ng
d˘a
.
c ta
’
truyˆe
`
n thˆo
´
ng. Thˆong qua c´ac th`anh phˆa
`
n
dˆe
’
chı
’
r˜o t´ınh chˆa
´
t cu
’
a l´o
.
p v`a ´y ngh˜ıa c´ac phu
.
o
.
ng th´u
.
c cu
’

u tr´uc cu
’
a l´o
.
p v`a quan hˆe
.
cu
’
a ch´ung v´o
.
i nh˜u
.
ng l´o
.
p kh´ac.
Trong b`ai b´ao n`ay, ch´ung tˆoi
du
.
a ra mˆo
.
t c´ach xˆay du
.
.
ng
d˘a
.
c ta
’
lˆogic c´ac chu
.

.
´o
.
c hˆe
´
t x´et mˆo h`ınh
t´ınh to´an cu
’
a hˆe
.
thˆo
´
ng.
2. M
ˆ
O H
`
INH T
´
INH TO
´
AN
Mˆo
.
t chu
.
o
.
ng tr`ınh lˆe
.

.
ng tr`ınh.
• P
l`a tˆa
.
p to´an tu
.
’
x´ac
di
.
nh quan hˆe
.
gi˜u
.
a c´ac gi´a tri
.
kho
.
’
i ta
.
o cu
’
a c´ac biˆe
´
n trong chu
.
o
.

p(x)
du
.
o
.
.
c go
.
i l`a tiˆe
`
n
diˆe
`
u kiˆe
.
n v`a pha
’
i c´o gi´a tri
.
true tru
.
´o
.
c khi chu
.
o
.
ng tr`ınh b˘a
´
t

x

biˆe
’
u diˆe
˜
n
gi´a tri
.
kho
.
’
i
dˆa
`
u v`a kˆe
´
t th´uc cu
’
a biˆe
´
n
x
trong chu
.
o
.
ng tr`ınh.
ok
v`a

.
c k´ıch hoa
.
t ho
.
.
p
th´u
.
c
ok
l`a true, nˆe
´
u viˆe
.
c thu
.
.
c hiˆe
.
n chu
.
o
.
ng tr`ınh cuˆo
´
i c`ung th`anh cˆong
ok

l`a true. Ngu

h`ınh th´u
.
c h´oa h`anh vi cu
’
a chu
.
o
.
ng tr`ınh hu
.
´o
.
ng
dˆo
´
i tu
.
o
.
.
ng, mˆo h`ınh t´ınh to´an trong
b`ai n`ay c´o c´ac
d˘a
.
c tru
.
ng nhu
.
sau
dˆay:

di
.
a
phu
.
o
.
ng) m`a c`on ca
’
c´ac
dˆo
´
i tu
.
o
.
.
ng.
Dˆe
’
da
’
m ba
’
o truy cˆa
.
p c´ac biˆe
´
n, mˆo h`ınh cˆa
`

dˆo
´
i tu
.
o
.
.
ng c´o thˆe
’
n˘a
`
m trong l´o
.
p con bˆa
´
t k`y cu
’
a mˆo
.
t tˆo
’
ch´u
.
c
du
.
o
.
.
c khai b´ao. Nhu

a n´o.
Dˆe
’
hˆo
˜
tro
.
.
co
.
cˆa
´
u liˆen kˆe
´
t
dˆo
.
ng cu
’
a phu
.
o
.
ng th´u
.
c go
.
i, mˆo h`ınh s˜e lu
.
u gi˜u

.
c v`a c´ac lˆe
.
nh trong
pha
.
m vi m`a mˆo
˜
i biˆe
´
n ´u
.
ng v´o
.
i mˆo
.
t ba
’
n ghi ho
.
.
p th´u
.
c.
3. C˜ung nhu
.
trong c´ac ngˆon ng˜u
.
lˆe
.

´
i tu
.
o
.
.
ng c´o thˆe
’
ch´u
.
a nhiˆe
`
u thuˆo
.
c t´ınh cu
’
a n´o, v`a gi´a tri
.
c´ac thuˆo
.
c t´ınh
thu
.
`o
.
ng
du
.
o
.

.
o
.
.
ng v`a
nh˜u
.
ng gi´a tri
.
cu
’
a c´ac thuˆo
.
c t´ınh
d´o (c´o t´ınh dˆe
.
quy).
V`ı chu
.
o
.
ng tr`ınh hu
.
´o
.
ng
dˆo
´
i tu
.

.
ng trong
d´o chu
.
o
.
ng tr`ınh
du
.
o
.
.
c thi h`anh,
α
c´o thˆe
’
du
.
o
.
.
c chia 3 phˆa
`
n
nhu
.
sau:
1. Phˆa
`
n th´u

.
phˆa
.
n m`a ´anh xa
.
t`u
.
l´o
.
p t´o
.
i l´o
.
p cha cu
’
a n´o, t´u
.
c l`a
superclass(M ) =
N,
v´o
.
i
N
l`a l´o
.
p cha cu
’
a l´o
.

O H
`
INH DA
.
I S
ˆ
O
´
QUAN H
ˆ
E
.
CU
’
A H
ˆ
E
.
TH
ˆ
O
´
NG HU
.
´
O
.
NG
D
ˆ

0  i < n.
2. Phˆa
`
n th´u
.
2 mˆo ta
’
chi tiˆe
´
t cˆa
´
u tr´uc cu
’
a mˆo
˜
i l´o
.
p: v´o
.
i mˆo
˜
i l´o
.
p
N ∈
cname, n´o bao gˆo
`
m:
•
attribute(

: U
m
, c
m
}
trong d´o
U
i
v`a
c
i
d´ong vai tr`o l`a kiˆe
’
u v`a gi´a tri
.
kho
.
’
i
dˆa
`
u cu
’
a thuˆo
.
c t´ınh ai trong l´o
.
p
N
, v`a

o
.
ng th´u
.
c
du
.
o
.
.
c khai b´ao ho˘a
.
c kˆe
´
th`u
.
a bo
.
’
i
N :
{m
1
→ (x
1
: T
1,1
, y
1
: T

ng th´u
.
c
m
i
c´o
x
i
, y
i
v`a
z
i
tu
.
o
.
ng ´u
.
ng l`a gi´a tri
.
, kˆe
´
t qua
’
v`a gi´a tri
.
tham sˆo
´
kˆe

´
D
i
.
3. Phˆa
`
n th´u
.
3 nhˆa
.
n biˆe
´
t c´ac biˆe
´
n m`a ch´ung su
.
’
du
.
ng
du
.
o
.
.
c bo
.
’
i chu
.

biˆe
’
u diˆe
˜
n kiˆe
’
u cu
’
a biˆe
´
n
x
i
,
c´o thˆe
’
l`a mˆo
.
t trong sˆo
´
kiˆe
’
u d˜u
.
liˆe
.
u
do
.
n gia

locvar: Tˆa
.
p c´ac biˆe
´
n di
.
a phu
.
o
.
ng trong pha
.
m vi
{v
1
: T
1
, , v
m
: T
m
}.
•
visibleattr: Tˆa
.
p c´ac thuˆo
.
c t´ınh tu
.
`o

th`u
.
a) cu
’
a l´o
.
p.
Dˆe
’
thuˆa
.
n lo
.
.
i, ch´ung ta th`u
.
a nhˆa
.
n c´o 4 tˆa
.
p tˆen kh´ac nhau: tˆen biˆe
´
n, tˆen l´o
.
p, tˆen thuˆo
.
c t´ınh
v`a tˆen phu
.
o

.
o
.
.
ng th`ı gi´a tri
.
cu
’
a n´o s˜e l`a mˆo
.
t bˆo
.
gi´a
tri
.
cu
’
a c´ac thuˆo
.
c t´ınh v´o
.
i kiˆe
’
u hiˆe
.
n ta
.
i:
{myclass → M} ∪ {a → value | a ∈ attribue(M )}.
3. BI

.
p lˆe
.
cu
’
a biˆe
’
u th´u
.
c
e
, ta du
.
a ra x´ac nhˆa
.
n
D(e)
, n´o l`a d´ung trong
tru
.
`o
.
ng ho
.
.
p m`a biˆe
’
u th´u
.
c

u n´o d˜a biˆe
´
t trong chu
.
o
.
ng tr`ınh.
D(x) df x ∈ (alphabet ∪ locvar).
K´y hiˆe
.
u null biˆe
’
u diˆe
˜
n mˆo
.
t dˆo
´
i tu
.
o
.
.
ng x´ac
di
.
nh d´ung.
D(null) df true, type(null) df NULL,
o
.

nh d´ung nˆe
´
u l´o
.
p
N
d˜a du
.
o
.
.
c khai b´ao.
D(newN) df N ∈ cname.
N´o chı
’
ra mˆo
.
t dˆo
´
i tu
.
o
.
.
ng m´o
.
i cu
’
a l´o
.

AN VY
.
,
D
˘
A
.
NG V
˘
AN D
´
U
.
C
Kiˆe
’
u thu
.
’
nghiˆe
.
m (test)
e
is
N
l`a biˆe
’
u th´u
.
c (lˆogic) x´ac

Gi´a tri
.
cu
’
a biˆe
’
u th´u
.
c
du
.
o
.
.
c x´ac
di
.
nh r˜o b˘a
`
ng gi´a tri
.
cu
’
a
e
l`a dˆo
´
i tu
.
o

.
.
ng kh´ac null trong l´o
.
p con cu
’
a
N
D((N)e) df D(e is N)
∧
(e = null)
∧
(e(myclass)  N), (N)e df e.
Kiˆe
’
u cu
’
a
(N)e
l`a l´o
.
p
N : type((N )e) df N.
Thuˆo
.
c t´ınh lu
.
.
a cho
.

∧
(e = null)
∧
(e(myclass).a) ∈ visibleattr,
e.a df
e(a), type(e.a) df type(e(myclass).a).
Thuˆo
.
c t´ınh cˆa
.
p nhˆa
.
t
(e; a : f)
l`a x´ac di
.
nh d´ung v´o
.
i
diˆe
`
u kiˆe
.
n l`a
e.a
l`a hiˆe
’
n hiˆe
.
n v`a kiˆe

.
cu
’
a n´o c´o thˆe
’
thu nhˆa
.
n du
.
o
.
.
c t`u
.
gi´a tri
.
cu
’
a
e
b˘a
`
ng c´ach thay dˆo
’
i gi´a tri
.
cu
’
a thuˆo
.

(type(f ) = B).
Biˆe
´
n self c´o thˆe
’
chı
’
du
.
o
.
.
c tham kha
’
o trong
di
.
nh ngh˜ıa cu
’
a c´ac phu
.
o
.
ng th´u
.
c, v`a
du
.
o
.

tro
.
.
viˆe
.
c xˆay du
.
.
ng chu
.
o
.
ng tr`ınh hu
.
´o
.
ng
dˆo
´
i tu
.
o
.
.
ng tiˆeu biˆe
’
u
[3].
c ::= |skip | chaos | c  b  c | cΠc | c; c | b ∗ c | varx : T | endx | le := e | o.m(e).
O

’
vˆe
´
tr´ai cu
’
a
ph´ep g´an v`a c´o da
.
ng
le ::= x|le.a
v´o
.
i
x
l`a biˆe
´
n do
.
n c`on
a
l`a thuˆo
.
c t´ınh cu
’
a dˆo
´
i tu
.
o
.

n): Cho
P
v`a
Q
l`a c´ac thiˆe
´
t kˆe
´
.
P  b  Q
chu
.
o
.
ng tr`ınh thu
.
.
c hiˆe
.
n
P
nˆe
´
u gi´a tri
.
b
l`a true, ngu
.
o
.

TH
ˆ
O
´
NG HU
.
´
O
.
NG
D
ˆ
O
´
I TU
.
O
.
.
NG
265
P  b  Q df
(D(b)
∧
type(b) = B) → (P
∧
b ∨ Q
∧
¬b).
Cho

’
thu
.
.
c hiˆe
.
n nˆe
´
u
b
i
l`a true. Khi mo
.
i
b
i
l`a false th`ı khˆong x´ac di
.
nh (chaos).
non-determinism (khˆong tiˆe
`
n
di
.
nh): Cho
P
v`a
Q
l`a c´ac thiˆe
´

c
Q,
nhu
.
ng s˜e khˆong
du
.
o
.
.
c cho
.
n tru
.
´o
.
c:
P ΠQ df P V Q.
composition (cˆa
´
u th`anh): Cho
P
v`a
Q
l`a c´ac thiˆe
´
t kˆe
´
, th`anh phˆa
`

c, khi
P
kˆe
´
t th´uc th`ı
Q
s˜e b˘a
´
t dˆa
`
u,
tra
.
ng th´ai kˆe
´
t th´uc cu
’
a
P
l`a ph`u ho
.
.
p cho tra
.
ng th´ai b˘a
´
t
dˆa
`
u cu

n, k´y hiˆe
.
u
b ∗ P
: ngh˜ıa l`a
P
du
.
o
.
.
c
thu
.
.
c hiˆe
.
n ch`u
.
ng n`ao
b
c`on l`a true tru
.
´o
.
c mˆo
˜
i lˆa
`
n l˘a

c t´ınh
le.a
cu
’
a dˆo
´
i tu
.
o
.
.
ng
le,
dˆo
´
i tu
.
o
.
.
ng v´o
.
i kiˆe
’
u khuˆon mˆa
˜
u
(N)le.
Khai b´ao biˆe
´

= {v}  locvar),
o
.
’
dˆay
{v}  locvar
biˆe
’
u diˆe
˜
n tˆa
.
p locvar sau khi d˜a loa
.
i bo
’
biˆe
´
n
v.
Diˆe
`
u d´o gia
’
i th´ıch r˘a
`
ng:
nh˜u
.
ng r`ang buˆo

.
c. Chu
.
o
.
ng tr`ınh
O.m(v, r, vr)
g´an c´ac tham biˆe
´
n hiˆe
.
n ta
.
i
v
v`a
vr
c´ac gi´a tri
.
ch´ınh th´u
.
c v`a gi´a tri
.
tham biˆe
´
n
kˆe
´
t qua
’

’
a phu
.
o
.
ng th´u
.
c
m.
Sau khi n´o kˆe
´
t th´uc, c´ac gi´a tri
.
kˆe
´
t qua
’
v`a gi´a tri
.
tham sˆo
´
kˆe
´
t qua
’
cu
’
a
m
du


var self : N, x, T 1, y : T2, z : T 3;
self, x, z := O, v, r, vr;
N.m
O, v, r, vr := self, y, z;
end self, x, y, z;






N  type(O) ∧ m ∈ meth(N)}fi.
O
.
’
dˆay:
• x, y
v`a
z
l`a gi´a tri
.
, kˆe
´
t qua
’
v`a gi´a tri
.
tham biˆe
´

´
liˆen kˆe
´
t v´o
.
i
phu
.
o
.
ng th´u
.
c
m
cu
’
a l´o
.
p
N.
•
self gi´a tri
.
tham sˆo
´
kˆe
´
t qua
’
tu

.
t
dˆo
.
ng hiˆe
.
n ta
.
i r`ang buˆo
.
c v´o
.
i
dˆo
´
i tu
.
o
.
.
ng
O.
266
NGUY
ˆ
E
˜
N MA
.
NH D

5.1. Khai b´ao l´o
.
p
Bank
name
address
withdraw(ID, amount)
getBalance(ID, res)
newAcount(name, amount)
Account
aID: int
balance: int
withdraw(amount)
getBalance()
CA
withdraw(amount)
SA
withdraw(amount)
Bank
name
address
withdraw(ID, amount)
getBalance(ID, res)
newAcount(name, amount)
Bank
name
address
withdraw(ID, amount)
getBalance(ID, res)
newAcount(name, amount)

.
p, t´ınh x´ac
di
.
nh d´ung cu
’
a ch´ung [2].
Mˆo
.
t chu
.
o
.
ng tr`ınh hu
.
´o
.
ng
dˆo
´
i tu
.
o
.
.
ng c´o thˆe
’
du
.
o

i lˆe
.
nh
P
biˆe
’
u diˆe
˜
n phu
.
o
.
ng th´u
.
c main cu
’
a chu
.
o
.
ng
tr`ınh. Viˆe
.
c khai b´ao l´o
.
p cdecls c´o thˆe
’
theo ngˆon ng˜u
.
tu

pub:
v
1
: V
1
, , v
k
: V
k
;
meth:
m
1
(x
11
: T
11
, y
12
: T
12
, z
13
: T
13
){P
1
};

m

.
c khai b´ao v`a
M
l`a l´o
.
p cha cu
’
a n´o. Nˆe
´
u khˆong c´o private th`ı l´o
.
p
N
du
.
o
.
.
c khai b´ao ngˆa
`
m
di
.
nh kiˆe
’
u public. Phˆa
`
n pri di
.
nh ngh˜ıa c´ac c´ac thuˆo

di
.
nh ngh˜ıa c´ac thuˆo
.
c t´ınh chung (public) cho l´o
.
p N. Phˆa
`
n meth khai b´ao c´ac phu
.
o
.
ng th´u
.
c
cu
’
a l´o
.
p
N,
trong d´o
m
1
, m
2
, , m

l`a c´ac phu
.

, kˆe
´
t qua
’
, gi´a tri
.
tham biˆe
´
n kˆe
´
t qua
’
v`a phˆa
`
n thˆan cu
’
a phu
.
o
.
ng th´u
.
c
m
i
.
V´ı du
.
: X´et hˆe
.

.
p con l`a Current Account (CA) v`a Saving Account (SA).
Viˆe
.
c khai b´ao l´o
.
p Account
du
.
o
.
.
c chı
’
ra bo
.
’
i declAccount nhu
.
sau:
class Account
pro: aID: int, balance: int;
meth:
getBalance(0,
b
: int, 0)
{ b := balance };
withdraw(x : int, 0, 0) { balance  x  balance’ = balance - x};
M
ˆ

O
´
I TU
.
O
.
.
NG
267
end Account
Viˆe
.
c khai b´ao declCA cu
’
a CA nhu
.
sau:
class CA extends Account
meth: withdraw(x: int, 0, 0) { balance := balance - x};
end CA
Viˆe
.
c khai b´ao declSA cu
’
a SA nhu
.
sau:
class SA extends Account
meth: withdraw(x: int, 0, 0) { skip  (balance < x) (balance := balance -x)};
end SA

.
.
c chı
’
ra bo
.
’
i WD(cdecl) khi tho
’
a m˜an
c´ac
diˆe
`
u kiˆe
.
n sau dˆay [2, 3]: a) N v`a M l`a kh´ac biˆe
.
t. b) Tˆen c´ac thuˆo
.
c t´ınh l`a kh´ac nhau. c)
Nh˜u
.
ng gi´a tri
.
kho
.
’
i
dˆa
`

c l`a kh´ac nhau. e) C´ac tham sˆo
´
cu
’
a mo
.
i phu
.
o
.
ng th´u
.
c l`a
kh´ac nhau.
Su
.
.
khai b´ao l´o
.
p cdecl
dˆe
’
bˆo
’
sung thˆong tin cˆa
´
u tr´uc cu
’
a l´o
.




alphabet

= alphabet
∧
cname

= {N }
∧
superclass

= {N → M }
∧
pri’ = {N → {t
1
: T
1
, c
1
, , (t
i
: T
i
, c
i
)}
∧
pro

∧
meth

= {N → {(m
1
→ (x
11
: T
11
, y
12
: T
12
, z
13
: T
13
, p
1
), ,
(m

→ (x
1
: T
1
, y
2
: T
2

.
’
c´ac thuˆo
.
c t´ınh
d˜a khai b´ao cu
’
a
l´o
.
p N, t`u
.
c´ac tˆa
.
p gi´a tri
.
cu
’
a attribute(N) thu nhˆa
.
n
du
.
o
.
.
c ho`an to`an quan hˆe
.
v´o
.

.
´o
.
c khi quan hˆe
.
phu
.
thuˆo
.
c gi˜u
.
a c´ac l´o
.
p theo l´y thuyˆe
´
t. Nhu
.
kˆe
´
t qua
’
, biˆe
´
n lˆogic
meth(N ) liˆen kˆe
´
t mˆo
˜
i phu
.

i phˆa
`
n khai b´ao.
268
NGUY
ˆ
E
˜
N MA
.
NH D
´
U
.
C, NGUY
ˆ
E
˜
N V
˘
AN VY
.
,
D
˘
A
.
NG V
˘
AN D

du
.
o
.
.
c chı
’
ra bo
.
’
i thiˆe
´
t kˆe
´
sau:
declAccount = true 


cname

= {Account}
∧
pro

= {Account → {aID : int, balance : int}}
∧
meth

= {Account → {getBalance → (0, b : int, 0, b := balance),
withdraw → (x : int, 0, 0, balance  x  balance − x)}}

a declSA l`a nhu
.
sau:


cname

= {SA}
∧
superclass

= {SA → Account}
∧
declSA = true  meth

= {Account →
{withdraw → (x : int, 0, 0, skip  (balance < x)  balance := balance − x}; }}


5.2. Th`anh phˆa
`
n cˆa
´
u tr´uc cu
’
a l´o
.
p
Sau dˆay ta xem x´et th`anh phˆa
`

´
u th`anh cu
’
a mˆo
.
t
sˆo
´
l´o
.
p:
cdecls ≡ cdecl
1
; cdecl
2
; ; cdecl
k
Th`anh phˆa
`
n cˆa
´
u tr´uc l´o
.
p khai b´ao
do
.
n gia
’
n l`a thˆem v`ao nˆo
.

.
p trong pha
.
m vi cu
’
a n´o. N´o c´o thˆe
’
du
.
o
.
.
c x´ac
di
.
nh bo
.
’
i kˆe
´
t ho
.
.
p song song nhu
.
sau [2]: (cdecl1; cdecl2) df cdecl1
M
cdecl2. O
.
’

, m

)
v`a thiˆe
´
t kˆe
´
M kˆe
´
t ho
.
.
p v´o
.
i c´ac
da
.
i lu
.
o
.
.
ng ra m1 v`a m2 cu
’
a X v`a Y t´o
.
i
da
.
i lu




alphabet

= alphabet1 ∪ alphabet2
∧
cname

= cname1 ∪ cname2
∧
superclass

= superclass1 ∩ superclass2
∧
pri

= pri
1
∪ pri
2
∧
pro

= pro
1
∪ pro
2
∧
pub

trˆen, ta thˆa
´
y r˘a
`
ng khˆong c´o viˆe
.
c khai b´ao la
.
i l´o
.
p trong phˆa
`
n
khai b´ao cu
’
a hˆe
.
thˆo
´
ng Bank. Tru
.
´o
.
c hˆe
´
t, ta t´ınh declAccount v`a declCA:
M
ˆ
O H
`

I TU
.
O
.
.
NG
269
declAccount; declCA = true 






cname

= {Account, CA}
∧
superclass

= {CA → Account}
∧
pro

= {Account{aID : int, balance : int}}
∧
meth

= {Account{getBalance(0, b : int, 0, b := balance)},
withdraw → (x : int, 0, 0, b ≥ x  balance








cname

= {Account, CA, SA}
∧
superclass

= {CA → Account, SA → Account}
∧
pro

= {Account{aID : int, balance : int}}
∧
meth

= {Account → {getBalance → (0, b : int, 0, b := balance),
withdraw → (x : int, 0, 0, b ≥ x  balance

:= balance − x)},
CA → {withdraw → (x : int, 0, 0, balance := balance − x)}
SA → {withdraw → (x : int, 0, 0, skip  (balance < x)  balance := balance − x)}}




















cname

= {Account, CA, SABank}
∧
superclass

= {CA → Account, SA → Account}
∧
pri

= {Bank → cname : string, address : string, A : set(Account)}
∧
pro

















T`u
.
mˆo h`ınh tu
.
o
.
ng tu
.
.
nhu
.
trˆen, He Jifeng v`a c´ac cˆo
.
ng su
.

ˆ
O
´
K
ˆ
E
´
T QUA
’
Trˆen dˆay, ch´ung tˆoi d˜a tr`ınh b`ay ng˜u
.
ngh˜ıa c´ac quan hˆe
.
da
.
i sˆo
´
cho d˘a
.
c ta
’
hˆe
.
thˆo
´
ng
hu
.
´o
.

ng l`a
mˆo
.
t c´ach mˆo ta
’
ch´ınh x´ac giˆo
´
ng nhu
.
ba
’
n sao trong ngˆon ng˜u
.
lˆe
.
nh. Do
d´o hˆa
`
u hˆe
´
t c´ac luˆa
.
t
da
.
i sˆo
´
d˜a du
.
o

N MA
.
NH D
´
U
.
C, NGUY
ˆ
E
˜
N V
˘
AN VY
.
,
D
˘
A
.
NG V
˘
AN D
´
U
.
C
chu
.
o
.

thˆo
´
ng l`a c´ac
dˆo
´
i tu
.
o
.
.
ng giˆo
´
ng nhu
.
c´ac luˆa
.
t co
.
ba
’
n
du
.
o
.
.
c thiˆe
´
t kˆe
´

o
.
.
c ph´at triˆe
’
n du
.
.
a v`ao mˆo
.
t ngˆon ng˜u
.
hu
.
´o
.
ng
dˆo
´
i tu
.
o
.
.
ng. Viˆe
.
c
xu
.
’

’
truyˆe
`
n thˆo
´
ng. C´ac to´an tu
.
’
chu
.
o
.
ng tr`ınh
du
.
o
.
.
c xu
.
’
l´y ch´ınh x´ac nhu
.
l`a ba
’
n sao trong ngˆon
ng˜u
.
r`ang buˆo
.

du
.
o
.
.
c cho
d˘a
.
c ta
’
thiˆe
´
t kˆe
´
chu
.
o
.
ng tr`ınh hu
.
´o
.
ng
dˆo
´
i tu
.
o
.
.

.
’
du
.
ng
dˆe
’
h`ınh th´u
.
c h´oa
liˆen kˆe
´
t c´ac mˆo h`ınh ca su
.
’
du
.
ng (use case) v`a mˆo h`ınh l´o
.
p trong UML. N´o c˜ung c´o thˆe
’
su
.
’
du
.
ng nhu
.
l`a co
.

.
.
ng.
C´ac
d˘a
.
c ta
’
trong ngˆon ng˜u
.
n`ay dˆe
˜
d`ang
du
.
o
.
.
c viˆe
´
t v`a hiˆe
’
u tu
.
o
.
ng tu
.
.
nhu

`
AI LI
ˆ
E
.
U THAM KHA
’
O
[1] Booch, G., Rumbaugh, J. and Jacobson, I.,
The Unified Modeling Language User Guide
,
Addison-Wesley, 1999.
[2] C.A.R. Hoare and He Jifeng,
Unifing Theories of Programming
, Prentice Hall, 1998.
[3] He Jifeng, Zhiming Liu and Li Xiaohan, A Relational Model for Object-Oriented Pro-
gramming, “Technical report UNU/IIST No.231, UNU/IIST: International Institute for
software technology”, the United Nations University, Macau, May 2001.
[4] He Jifeng, Li Xiaohan and Zhiming Liu, rCOS: Refinement Caclculus for Object Sys-
tems, Technical report UNU/IIST No.322, UNU/IIST: International Institute for soft-
ware technology, the United Nations University, Macau, May 2005.
[5] Ivar Jacopson, Gray Booch and James Rumbaugh,
The Unified Software Development
Process
, Addision-Wesley, 2000.
[6] P. America, F.de Boer, Reasoning about dynamically evolving process structures,
For-
mal Aspect of Computing
(6) (1994) 269—316.
[7] Rational Rose Corp., Rational Rose 2002, />Nhˆa