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

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

1. 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
2. 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
3. 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 tốn h c và các kí hi u đ ha
   ðc t hình th c (formal)  kí hi u tốn h c • ngơn ng đc t • ngơn ng lp trình 6 3
4. ðc t hình th c hay khơng hình th c ?
   ðc t hình th c  chính xác (tố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
5. 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
6. 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
7. 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
8. 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
9. 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
10. 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
11. 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
12. Mng Petri
    Ví d t2 t2 khi t2 đưc v ưt qua 23 Mng Petri Ví d 24 12
13. 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
14. Mng Petri
    Ví d 1: mơ t ho t đng an tồ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 tồ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
15. 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
16. 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
17. 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
18. 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
19. ð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
20. 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
21. 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
22. 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
23. 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