Xem mẫu
- Các k thu t ñ c t
(4)
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
N i dung
Khái ni m ñ c t
T i sao ph i ñ c t ?
Phân lo i các k thu t ñ c t
Các k thu t ñ c t
2
1
- Khái ni m ñ c t
ð c t (specification)
ñ nh nghĩa m t h th ng, mô-ñun hay
m t s n ph m c n ph i làm cái gì
không mô t nó ph i làm như th nào
mô t nh ng tính ch t c a v n ñ
ñ t ra
không mô t nh ng tính ch t c a gi i
pháp cho v n ñ ñó
3
Khái ni m ñ c t
ð c t là ho t ñ ng ñư c ti n hành trong
các giai ño n khác nhau c a ti n trình ph n
m m:
ð c t yêu c u (requirement specification)
• s th ng nh t gi a nh ng ngư i s d ng tương
lai và nh ng ngư i thi t k
ð c t ki n trúc h th ng (system architect
specification)
• s th ng nh t gi a nh ng ngư i thi t k và
nh ng ngư i cài ñ t
ð c t môñun (module specification)
• s th ng nh t gi a nh ng ngư i l p trình cài ñ t
mô-ñun và nh ng ngư i l p trình s d ng mô-ñun
4
2
- T i sao ph i ñ c t ?
H p ñ ng
s th ng nh t gi a ngư i s d ng và ngư i
phát tri n s n ph m
H p th c hóa
s n ph m làm ra ph i th c hi n chính xác
nh ng gì mong mu n
Trao ñ i
gi a ngư i s d ng và ngư i phát tri n
gi a nh ng ngư i phát tri n
Tái s d ng
5
Phân lo i các k thu t ñ c t
ð c t phi hình th c (informal)
ngôn ng t nhiên t do
ngôn ng t nhiên có c u trúc
các kí hi u ñ h a
ð c t n a hình th c (semi-informal)
tr n l n c ngôn ng t nhiên, các kí hi u toán h c và
các kí hi u ñ h a
ð c t hình th c (formal)
kí hi u toán h c
• ngôn ng ñ c t
• ngôn ng l p trình
6
3
- ð c t hình th c hay không
hình th c ?
ð c t hình th c
chính xác (toán h c)
h p th c hóa hình th c (công c hóa)
công c trao ñ i: khó ñ c, khó hi u
khó s d ng
ð c t không hình th c
d hi u, d s d ng
m md o
thi u s chính xác
nh p nh ng
7
ng d ng ñ c t hình th c
ng d ng trong các giai ño n s m c a ti n
trình phát tri n
h n ch l i trong phát tri n ph n m m
ng d ng ch y u trong phát tri n các h
th ng “quan tr ng” (critical systems)
h th ng ñi u khi n
h th ng nhúng
h th ng th i gian th c
8
4
- Chi phí phát tri n khi s
d ng ñ c t hình th c
9
Các k thu t ñ c t
Trình bày m t s k thu t
Máy tr ng thái h u h n
M ng Petri
ði u ki n trư c và sau
Ki u tr u tư ng
ð ct Z
10
5
- Máy tr ng thái h u h n
(state machine)
mô t các lu ng ñi u khi n
bi u di n d ng ñ th
bao g m
t p h p các tr ng thái S (các nút c a ñ th )
t p h p các d li u vào I (các nhãn c a các
cung)
t p h p các chuy n ti p T : S x I → S (các
cung có hư ng c a ñ th )
• khi có m t d li u vào, m t tr ng thái chuy n sang
m t tr ng thái khác
11
Máy tr ng thái h u h n
ð t máy xu ng ð i ð t máy xu ng
Ví d 1 Nh c máy
Âm m i quay
s
Th i gian ñ i k t B ms
thúc
S sai
Thông báo
Quay s quay s sai
S ñúng
K tn i
Máy b n K t n i ñư c
ð chuông
Thuê bao ñư c g i nh c máy
12 ðàm tho i
6
- Máy tr ng thái h u h n
Ví d 2
H th ng c n mô t bao g m m t nhà s n xu t, m t
nhà tiêu th và m t kho hàng ch ch a ñư c nhi u
nh t 2 s n ph m
Nhà s n xu t có 2 tr ng thái
• P1: không s n xu t
• P2: ñang s n xu t
Nhà tiêu th có 2 tr ng thái
• C1: có s n ph m ñ tiêu th
• C2: không có s n ph m ñ tiêu th
Nhà kho có 3 tr ng thái
• ch a 0 s n ph m
• ch a 1 s n ph m
• ch a 2 s n ph m
13
Máy tr ng thái h u h n
Gi i pháp 1: mô t tách r i các thành ph n
S n xu t L y t kho
P1 P2 C1 C2
G i vào kho
Tiêu th
G i vào kho G i vào kho
0 1 2
L y t kho L y t kho
14
7
- Máy tr ng thái h u h n
Gi i pháp 1
không mô t ñư c s ho t ñ ng h
th ng
c n mô t s ho t ñ ng k t h p các
thành ph n c a h th ng
15
Máy tr ng thái h u h n
Gi i pháp 2: mô t k t h p các thành ph n
G i vào kho G i vào kho
S n xu t S n xu t
S n xu t L y t kho L y t kho
Tiêu th Tiêu th
Tiêu th
L y t kho L y t kho
Tiêu th Tiêu th
Tiêu th
S n xu t S n xu t
S n xu t
G i vào kho G i vào kho
16
8
- Máy tr ng thái h u h n
Gi i pháp 2
mô t ñư c ho t ñ ng c a h th ng
s tr ng thái l n
bi u di n h th ng ph c t p
h n ch khi ñ c t nh ng h th ng không
ñ ng b
o các thành ph n c a h th ng ho t ñ ng song
song ho c c nh tranh
17
M ng Petri
(Petri nets)
thích h p ñ mô t các h th ng không
ñ ng b v i nh ng ho t ñ ng ñ ng th i
mô t lu ng ñi u khi n c a h th ng
ñ xu t t năm 1962 b i Carl Adam
Có hai lo i
m ng Petri (c ñi n)
m ng Petri m r ng
18
9
- M ng Petri
G m các ph n t
m t t p h p h u h n các nút ( )
m t t p h p h u h n các chuy n ti p ( )
m t t p h p h u h n các cung (→)
• các cung n i các nút v i các chuy n ti p ho c
ngư c l i
m i nút có th ch a m t ho c nhi u th ( )
19
M ng Petri
Ví d
t2
t1 p2
p1 t3 p4
p3
20
10
- M ng Petri
M ng Petri ñư c ñ nh nghĩa b i s ñánh d u các nút
c a nó
Vi c ñánh d u các nút ñư c ti n hành theo nguyên t c
sau:
m i chuy n ti p có các nút vào và các nút ra
n u t t c các nút vào c a m t chuy n ti p có ít nh t
m t th , thì chuy n ti p này là có th vư t qua ñư c,
n u chuy n ti p này ñư c th c hi n thì t t c các nút
vào c a chuy n ti p s b l y ñi m t th , và m t th
s ñư c thêm vào t t c các nút ra c a chuy n ti p
n u nhi u chuy n ti p là có th vư t qua thì ch n
chuy n ti p nào cũng ñư c
21
M ng Petri
Ví d
t1 t2
t1 không th vư t qua ñư c t2 có th vư t qua ñư c
t3
ho c t3 ñư c vư t qua
ho c t4 ñư c vư t qua
22 t4
11
- M ng Petri
Ví d
t2 t2
khi t2 ñư c vư t qua
23
M ng Petri
Ví d
24
12
- M ng Petri
Ví d 1: mô t ho t ñ ng c a ñèn giao thông
red
yr
rg yellow
gy
25 green
M ng Petri
Ví d 1: mô t ho t ñ ng c a 2 ñèn giao thông
red1 red2
yr1 yr2
rg1 yellow1 yellow2 rg2
gy1 gy2
26
green1 green2
13
- M ng Petri
Ví d 1: mô t ho t ñ ng an toàn c a 2 ñèn giao thông
red1 red2
safe
yr1 yr2
rg1 yellow1 yellow2 rg2
gy1 gy2
27
green1 green2
M ng Petri
Ví d 1: mô t ho t ñ ng an toàn và h p lý c a 2 ñèn
giao thông
red1 red2
safe2
yr1 yr2
rg1 yellow1 rg2
yellow2
gy1 gy2
safe1
28 green1 green2
14
- M ng Petri
Ví d 2: mô t chu kỳ s ng c a m t ngư i
tr con
d y thì
cư i thanh niên
có v có ch ng ly hôn
29 ch t ch t
M ng Petri
Ví d 3: vi t thư và ñ c thư
begin receive_mail
mail_box
rest rest
type_mail read_mail
send_mail ready
Mô t trư ng h p 1 ngư i vi t và 2 ngư i ñ c ?
Mô t trư ng h p h p thư nh n ch ch a nhi u nh t 3 thư ?
30
15
- M ng Petri
Ví d 4: tình hu ng ngh n (dead-lock)
P1 P2
P3
t1 t2
P4 P5
t3 t4
P7
P6
t5 t6
P8 P9
2 2
t7 t8
31
M ng Petri
Ví d 4: gi i pháp ch ng ngh n
P1 P2
P3
t1 t2
P4 P5
t3 t4
2 2
P7
P6
t5 t6
P8 P9
2 2
t7 t8
32
16
- M ng Petri
Ví d 5
H th ng c n mô t bao g m m t nhà s n xu t, m t
nhà tiêu th và m t kho hàng ch ch a ñư c nhi u
nh t 2 s n ph m
Nhà s n xu t có 2 tr ng thái
• P1: không s n xu t
• P2: ñang s n xu t
Nhà tiêu th có 2 tr ng thái
• C1: có s n ph m ñ tiêu th
• C2: không có s n ph m ñ tiêu th
Nhà kho có 3 tr ng thái
• ch a 0 s n ph m
• ch a 1 s n ph m
• ch a 2 s n ph m
33
M ng Petri
Ví d 5: mô t tách r i m i thành ph n
S n xu t L y t kho
P1 P2 C1 C2
G i vào kho Tiêu th
G i vào kho G i vào kho
0 1 2
L y t kho L y t kho
34
17
- M ng Petri
Ví d 5: mô t k t h p các thành ph n
S n xu t
P1 G i vào kho
P2 G i vào kho
L y t kho
2
0 1
L y t kho
C1
C2
Tiêu th
35
ði u ki n trư c và sau
(pre/post condition)
ñư c dùng ñ ñ c t các hàm ho c mô-ñun
ñ c t các tính ch t c a d li u trư c và sau khi th c
hi n hàm
pre-condiition: ñ c t các ràng bu c trên các tham
s trư c khi hàm ñư c th c thi
post-condition: ñ c t các ràng bu c trên các tham
s sau khi hàm ñư c th c thi
có th s d ng ngôn ng phi hình th c, hình th c
ho c ngôn ng l p trình ñ ñ c t các ñi u ki n
36
18
- ði u ki n trư c và sau
Ví d : ñ c t hàm tìm ki m
function search ( a : danh sách ph n t ki u K,
size : s phân t c a dánh sách,
e : ph n t ki u K,
result : Boolean )
pre ∀i, 1 ≤ i ≤ n, a[i] ≤ a[i+1]
post result = (∃i, 1 ≤ i ≤ n, a[i] = e)
37
ði u ki n trư c và sau
Bài t p: ñ c t các hàm
1. S p x p m t danh sách các s nguyên
2. ð o ngư c các ph n t c a m t danh
sách
3. ð m s ph n t có giá tr e trong m t danh
sách các s nguyên
38
19
- Ki u tr u tư ng
(abstract types)
Mô t d li u và các thao tác trên d li u ñó m t
m c tr u tư ng ñ c l p v i cách cài ñ t d li u b i
ngôn ng l p trình
ð c t m t ki u tr u tư ng g m:
tên c a ki u tr u tư ng
• dùng t khóa sort
khai báo các ki u tr u tư ng ñã t n t i ñư c s d ng
• dùng t khóa imports
các thao tác trên trên ki u tr u tư ng
• dùng t khóa operations
39
Ki u tr u tư ng
Ví d 1: ñ c t ki u tr u tư ng Boolean
sort Boolean
operations
true : → Boolean
false : → Boolean
¬_ : Boolean → Boolean
_∧_ : Boolean x Boolean → Boolean
_∨_ : Boolean x Boolean → Boolean
m t thao tác không có tham s là m t h ng s
m t giá tr c a ki u tr u tư ng ñ nh nghĩa ñư c bi u di n b i kí t “_”
40
20
nguon tai.lieu . vn
