Xem mẫu
- ð c t Z (5)
Nguy n Thanh Bình
Khoa Công ngh Thông tin
Trư ng ð i h c Bách khoa
ð i h c ðà N ng
Gi i thi u
ñư c ñ xu t b i Jean René Abrial ð ih c
Oxford
ngôn ng ñ c t hình th c ñư c s d ng r ng rãi
nh t
d a trên lý thuy t t p h p
ký hi u toán h c
s d ng các sơ ñ (schema)
d hi u
2
1
- Gi i thi u
G m b n thành ph n cơ b n
các ki u d li u (types)
• d a trên khái ni m t p h p
các sơ ñ tr ng thái (state schemas)
• mô t các bi n và ràng bu c trên các bi n
các sơ ñ thao tác (operation schemas)
• mô t các thao tác (thay ñ i tr ng thái)
các toán t sơ ñ (schema operations)
• ñ nh nghĩa các sơ ñ m i t các sơ ñ ñã có
3
Ki u d li u
m i ki u d li u là m t t p h p các ph n t
Ví d
{true, false} : ki u lô-gíc
N: ki u s t nhiên
Z: ki u s nguyên
R: ki u s th c
{red, blue, green}
4
2
- Ki u d li u
Các phép toán trên t p h p
H i: A∪B
Giao: A∩B
Hi u: A⁄B
T p con: A⊆B
T p các t p con: P A
• ví d : P {a, b} = {{}, {a}, {b}, {a, b}}
5
Ki u d li u
m t s ki u d li u cơ b n ñã ñư c ñ nh
nghĩa trư c
ki u s nguyên Z
ki u s t nhiên N
ki u s th c R
...
có th ñ nh nghĩa các ki u d li u m i
ANSWER == yes | no
[PERSON]
• s d ng c p ký hi u [ và ] ñ ñ nh nghĩa ki u cơ
b nm i
6
3
- Ki u d li u
Khai báo ki u
x:T
• x là ph n t c a t p T
Ví d
• x:R
• n:N
• 3:N
• red : {red, blue, green}
7
V t
M t v t (predicate) ñư c s d ng ñ ñ nh
nghĩa các tính ch t c a bi n/giá tr
Ví d
x>0
π∈R
8
4
- V t
Có th s d ng các toán t lô-gíc ñ ñ nh nghĩa các v
t ph c t p
Và: A∧B
Ho c: A∨B
Ph ñ nh: ¬A
Kéo theo: A⇒B
Ví d
(x > y) ∧ (y > 0)
(x > 10) ∨ (x = 1)
(x > 0) ) ⇒ x/x = 1
(¬ (x ∈ S)) ∨ (x ∈ T)
9
V t
Các toán t khác
(∀x : T • A)
• A ñúng v i m i x thu c T
• Ví d : (∀x : N • x - x =0)
(∃x : T • A)
• A ñúng v i m t s giá tr x thu c T
• Ví d : (∃x : R • x + x = 4)
{x : T | A}
• bi u di n các ph n t x c a T th a mãn A
• Ví d : N = {x : Z | x ≥ 0}
10
5
- Sơ ñ tr ng thái
C u trúc sơ ñ tr ng thái g m
tên sơ ñ
khai báo bi n
ñ nh nghĩa v t
11
Sơ ñ tr ng thái
ð c t Z ch a
các bi n tr ng thái
kh i gán bi n
các thao tác trên các bi n
bi n tr ng thái có th có các b t bi n
• ñi u ki n mà luôn ñúng, bi u di n b i các v t
12
6
- Sơ ñ thao tác
Kh i gán bi n
Khai báo thao tác trên bi n
kí hi u ∆ bi u di n bi n tr ng thái b thay ñ i b i thao
tác
kí hi u ‘ (d u nháy ñơn) bi u di n giá tr m i c a bi n
13
Sơ ñ thao tác
Thao tác có th có các tham s vào và ra
tên tham s vào k t thúc b i kí t “?”
tên tham s ra k t thúc b i kí t “!”
14
7
- Sơ ñ thao tác
Kí hi u Ξ mô t thao tác không th thay ñ i
bi n tr ng thái
15
Ví d 1
ð c t h th ng ghi nh n các nhân viên vào/ra tòa
nhà làm vi c
Ki u d li u [Staff] là ki u cơ b n m i c a h th ng
Tr ng thái c a h th ng bao g m
• t p h p các ngư i s d ng h th ng user
• t p h p các nhân viên ñang vào in
• t p h p các nhân viên ñang ra out
b t bi n c a h th ng
16
8
- Ví d 1
ð c t thao tác ghi nh n m t nhân viên vào
17
Ví d 1
ð c t thao tác ghi nh n m t nhân viên ra
18
9
- Ví d 1
ð c t thao tác ki m tra m t nhân viên vào hay ra
Thao tác này cho k t qu là ph n t c a ki u
QueryReply == is_in | is_out
ð c t thao tác
19
Ví d 1
Kh i t o h th ng
20
10
- Ví d 1
Tóm l i
Sơ ñ tr ng thái: các thành ph n/ñ i tư ng
c a h th ng
B t bi n: ràng bu c gi a các ñ i tư ng
Các sơ ñ thao tác
• ði u ki n trên các tham s vào
• Quan h gi a tr ng thái trư c và sau
• Tham s k t qu
Kh i gán
21
Ví d 1
Hãy ñ c t các thao tác
Register: thêm vào m t nhân viên m i
QueryIn: cho bi t nh ng nhân viên ñang
vào/làm vi c
22
11
- Toán t sơ ñ
Các sơ ñ có th ñư c k t h p ñ t o ra
các sơ ñ m i
Các toán t sơ ñ
Và: ∧
Ho c: ∨
23
Toán t sơ ñ
Các sơ ñ ñã có
T o các sơ ñ m i
Schema3 == Schema1 ∧ Schema2
Schema4 == Schema1 ∨ Schema2
24
12
- Ví d 1 (ti p)
C i ti n thao tác StaffQuery
Thao tác StaffQuery chưa ñ c t trư ng h p
l i
• name? ∉ users
25
Ví d 1 (ti p)
C i ti n thao tác StaffQuery
ð c t l i ki u QueryReply
QueryReply == is_in | is_out | not_registered
Khi ñó
RobustStaffQuery == StaffQuery ∨ BadStaffQuery
26
13
- Ví d 1 (ti p)
C i ti n thao tác CheckIn
M r ng thao tác cho trư ng h p ghi nh n thành công
27
Ví d 1 (ti p)
C i ti n thao tác CheckIn
M r ng thao tác cho trư ng h p ghi nh n thành
công
Khi ñó
GoodCheckIn == CheckIn ∧ Success
28
14
- Ví d 1 (ti p)
C i ti n thao tác CheckIn
X lý thêm hai trư ng h p l i
1. name? ñã ñư c ghi nh n
2. name? chưa ñư c ñăng ký
29
Ví d 1 (ti p)
C i ti n thao tác CheckIn
X lý thêm hai trư ng h p l i
30
15
- Ví d 1 (ti p)
C i ti n thao tác CheckIn
Khi ñó
CheckInReply == ok | already_in | not_registered
RobustCheckIn == GoodCheckIn
∨ BadCheckIn1
∨ BadCheckIn2
31
Quan h
C p ph n t có th t ñư c bi u
di n
(x, y)
Tích ð -các c a hai ki u T1 và T2
T1 x T2
(x, y) : T1 x T2
32
16
- Quan h
Quan h (relation) là t p các c p
ph n t có th t
Ví d :
33
Quan h
Có th ký hi u quan h
T ↔ S == P (T x S)
directory : Person ↔ Number
Ánh x
c p ph n t có th t (x, y) có th vi t
• Ví d
Lưu ý
kí hi u ↔ dành cho ki u
kí hi u dành cho giá tr
34
17
- Quan h
Domain và Range
t p h p các thành ph n th nh t trong m t quan h
ñư c g i là domain (mi n)
• kí hi u: dom
• ví d :
dom(directory) = {mary, john, jim, jane}
t p h p các thành ph n th hai trong m t quan h
ñư c g i là range
• kí hi u: ran
• ví d :
ran(directory) = {287373, 398620, 829483, 493028}
35
Quan h
Phép tr mi n (domain subtraction)
ký hi u:
bi u di n quan h R v i các ph n t
trong mi n S ñã b lo i b
Nghĩa là:
36
18
- Quan h
Phép tr mi n (domain subtraction)
Ví d :
Khi ñó:
37
Ví d 2
ð c t danh b ñi n tho i g m tên ngư i và
s ñi n tho i
S d ng ki u cơ b n
[Person, Phone]
ð c t tr ng thái h th ng
38
19
- Ví d 2
Kh i t o h th ng
Thêm m t s ñi n tho i
39
Ví d 2
có th c i ti n ?
Tìm s ñi n tho i c a m t ngư i
Tìm tên theo s ñi n tho i
40
20
nguon tai.lieu . vn
