Bài giảng Nhập môn công nghệ phần mềm - Chương 4: Các kỹ thuật đặc tả - Nguyễn Thanh Bình

 Các k  thu t ñc t 
 (4)
 Nguy n Thanh Bình
 Khoa Công ngh Thôngtin
 Tr ưng ði h c Bách khoa
 ði h c ðà Nng
Ni dung

 Khái ni m ñc t 

 Ti 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 
 mt 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 ñon khác nhau c a ti n trình ph n 
 mm:
  ðc t  yêu c u (requirement specification)
 • s th ng nh t gi a nh ng ng ưi s  dng 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  dng mô-ñun
4
 2
Ti sao ph i ñc t  ?

 Hp ñng
  s th ng nh t gi a ng ưi s  dng vàngưi 
 phát tri n s n ph m

 Hp th c hóa
  sn 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  dng vàngưi phát tri n
  gi a nh ng ng ưi phát tri n

 Tái s  dng
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ó cu trúc
  các kí hi u ñ ha

 ðc t  na 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 ñ ha

 ðc t  hình th c (formal)
  kí hi u toán h c
 • ngôn ng ñc t 
 • ngôn ng  lp 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)
  hp 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 dng

 ðc t  không hình th c
  d hi u, d  s dng
  mm d 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 ñon s m c a ti n 
 trình phát tri n

 hn ch  li trong phát tri n ph n m m

 ng d ng ch  yu trong phát tri n các h 
 th ng “quan tr ng” (critical systems)
  h th ng ñiu 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 
dng ñ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
  Mng Petri
  ðiu ki n tr ưc và sau
  Ki u tr u t ưng
  ðc t  Z
10
 5
Máy tr ng thái h u h n
(state machine)

 mô t  các lu ng ñiu khi n

 bi u di n d ng ñ th 

 bao g m
  tp h p các tr ng thái S (các nút c a ñ th )
  tp h p các d  li u vào I (các nhãn c a các 
 cung)
  tp h p các chuy n ti p T : S x I → S (các 
 cung cóhưng ca ñ th )
 • khi có mt d  li u vào, m t tr ng thái chuy n sang 
 mt 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 Bm s 
 thúc S sai
 Thông báo 
 Quay s 
 quay s  sai
 Sñ úng
 Kt n i
 Máy b n Kt 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à sn xu t, m t 
 nhà tiêu th  và mt kho hàng ch  ch a ñưc nhi u 
 nh t 2 s n ph m
  Nhà sn xu t có 2 tr ng thái
 • P1: không s n xu t
 • P2: ñangsn xu t
  Nhà tiêu th  có 2 tr ng thái
 • C1: có sn ph m ñ tiêu th 
 • C2: không có sn 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
 Sn xu t Ly t  kho
 P1 P2 C1 C2
 Gi vào kho
 Tiêu th 
 Gi vào kho Gi vào kho
 0 1 2
 Ly t  kho Ly 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
  cn 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  kt h p các thành ph n
 Gi vào kho Gi vào kho
 Sn xu t Sn xu t
 Sn xu t Ly t  kho Ly t  kho
 Tiêu th  Tiêu th 
 Tiêu th 
 Ly t  kho Ly t  kho
 Tiêu th  Tiêu th 
 Tiêu th 
 Sn xu t Sn xu t
 Sn xu t
 Gi vào kho Gi 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
  hn 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
Mng Petri
(Petri nets)

 thích hp ñ mô t  các h  th ng không 
 ñng b  vi nh ng ho t ñng ñng th i

 mô t  lu ng ñiu khi n c a h  th ng

 ñ xu t t năm 1962 b i Carl Adam

 Có hai lo i
  mng Petri (c ñin)
  mng Petri m  rng
18
 9
Mng Petri

 Gm các ph n t 
  mt t p h p hu hn các nút ()
  mt t p h p hu hn các chuy n ti p ()
  mt t p h p hu hn các cung (→)
 • các cung ni các nút v i các chuy n ti p ho c 
 ng ưc l i
  mi nút có th  ch a m t ho c nhi u th  ()
19
Mng Petri

 Ví d
 t2
 t1 p2
 p1 t3 p4
 p3
20
 10
Mng Petri

 Mng Petri ñưc ñnh ngh ĩa b i s ñ ánh d u các nút 
 ca nó

 Vi c ñánh d u các nút ñưc ti n hành theo nguyên t c 
 sau:
  mi chuy n ti p có các nút vào và các nút ra
  nu t t c  các nút vào c a m t chuy n ti p có ít nh t 
 mt th , thì chuy n ti p này là có th  vưt qua ñưc,
  nu chuy n ti p này ñưc th c hi n thì tt c  các nút 
 vào c a chuy n ti p s  b ly ñi m t th , và mt th 
 sñưc thêm vào t t c  các nút ra c a chuy n ti p
  nu 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
Mng 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
Mng Petri

 Ví d
 t2 t2
 khi t2 ñưc v ưt qua
23
Mng Petri
Ví d
24
 12
Mng Petri

 Ví d 1: mô t  ho t ñng c a ñèn giao thông
 red
 yr
 rg yellow
 gy
25 green
Mng 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
 Mng 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
 Mng Petri

 Ví d 1: mô t  ho t ñng an toàn và hp lý c a 2 ñ èn 
 giao thông
 red1 red2
 safe2
 yr1 yr2
 rg1 yellow1 rg2
 yellow2
 gy1 gy2
 safe1
 28 green1 green2
 14
 Mng Petri
 
 Ví d 2: mô t  chu k ỳ sng c a m t ng ưi
 tr  con
 dy thì
 cưi thanh niên
 có v có ch ng ly hôn
 29 ch t ch t
 Mng 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
 Mng 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
 Mng 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
 Mng Petri
 
 Ví d 5
  H th ng c n mô t  bao g m m t nhà sn xu t, m t 
 nhà tiêu th  và mt kho hàng ch  ch a ñưc nhi u 
 nh t 2 s n ph m
  Nhà sn xu t có 2 tr ng thái
 • P1: không s n xu t
 • P2: ñangsn xu t
  Nhà tiêu th  có 2 tr ng thái
 • C1: có sn ph m ñ tiêu th 
 • C2: không có sn 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
 Mng Petri

 Ví d 5: mô t  tách r i m i thành ph n
 Sn xu t Ly t  kho
 P1 P2 C1 C2
 Gi vào kho Tiêu th 
 Gi vào kho Gi vào kho
 0 1 2
 Ly t  kho Ly t  kho
 34
 17
 Mng Petri

 Ví d 5: mô t  kt h p các thành ph n
 Sn xu t
 P1 Gi vào kho
 P2 Gi vào kho
 Ly t  kho 2
 0 1
 Ly t  kho
 C1
 C2
 Tiêu th 
 35
 ðiu 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 dng ngôn ng  phi hình th c, hình th c 
 ho c ngôn ng  lp trình ññc t  các ñiu ki n
 36
 18
ðiu 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  ca 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
ðiu ki n tr ưc và sau

 Bài t p: ñc t  các hàm
 1. Sp x p m t danh sách các s nguyên
 2. ðo ng ưc các ph n t  ca 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 ñó  mt 
 mc tr u t ưng ñc l p v i cách cài ñt d  li u b i 
 ngôn ng  lp trình
 
 ðc t  mt 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  dng 
 • 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
mt thao tác không có tham s  là mt h ng s 
mt giá tr  ca ki u tr u t ưng ñnh ngh ĩa ñưc bi u di n b i kí t “_”
 40
 20
 Ki u tr u t ưng
 
 Ví d 2: ñc t  ki u tr u t ưng Vector
 sort Boolean
 operations
 true : →→→ Boolean
 false : →→→ Boolean
 ¬¬¬ _ :Boolean →→→ Boolean
 _ ∧∧∧ _ : Boolean x Boolean →→→ Boolean
 _ ∨∨∨ _ : Boolean x Boolean →→→ Boolean
mt thao tác không có tham s  là mt h ng s 
mt giá tr  ca ki u tr u t ưng ñnh ngh ĩa ñưc bi u di n b i kí t “_”
 41
 Ki u tr u t ưng
 
 Ví d 2: ñc t  ki u tr u t ưng Vector
 sort Vector
 imports Integer, Element, Boolean
 operations
 vect : Integer x Integer →→→ Vector
 init : Vector x Integer →→→ Boolean
 ith : Vector x Integer →→→ Element
 change-ith : Vector x Integer x Element →→→ Vector
 supborder : Vector →→→ Integer
 infborder : Vector →→→ Integer
 42
 21
Ki u tr u t ưng

 Ví d 2: ñc t  ki u tr u t ưng Vector
  các thao tác trên ki u ch ñưc ñnh ngh ĩa 
 mà không ch  ra ng  ngh ĩa c a nó
 • tc là ý ngh ĩa c a thao tác
  s dng các tiên ñññnh ngh ĩa ng 
 ngh ĩa c a các thao tác
 • dùng t  khóa axioms
  ñnh ngh ĩa các ràng bu c mà mt thao tác 
 ñưc ñnh ngh ĩa
 • dùng t  khóa precondition
43
Ki u tr u t ưng

 Ví d 2: ñc t  ki u tr u t ưng Vector
 precondition
 ith (v, i) is-defined-ifonlyif
 infborder (v) ≤≤≤ i ≤≤≤ supborder (v) &&& init (v,i) = true
 axioms
 infborder (v) ≤≤≤ i ≤≤≤ supborder (v) ⇒⇒⇒ ith (change-ith (v, i, e), i) = e
 infborder (v) ≤≤≤ i ≤≤≤ supborder (v) &&& infborder (v) ≤≤≤ j ≤≤≤ supborder (v) &&& i ≠≠≠ j ⇒⇒⇒
 ith (change-ith (v, i, e), j) = ith (v, j)
 init (vect (i, j), k) = false
 infborder (v) ≤≤≤ i ≤≤≤ supborder (v) ⇒⇒⇒ init (change-ith (v, i, e), i) = true
 infborder (v) ≤≤≤ i ≤≤≤ supborder (v) &&& i ≠≠≠ j ⇒⇒⇒ init (change-ith (v, i, e), j) = init (v, j)
 infborder (vect (i, j)) = i
 infborder (change-ith (v, i, e)) = infborder (v)
 supborder (vect (i, j)) = j
 supborder (change-ith (v, i, e)) = supborder (v)
 with
 v: Vector; i, j, k: Integer; e: Element
44
 22
Ki u tr u t ưng

 Bài t p
  ðc t  ki u tr u t ưng cây nh  phân
  ðc t  ki u tr u t ưng tp h p
45
 23