Tài liệu Giáo trình công nghệ phần mềm 4 kythuatdacta

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 Ví d 1 ð i ð t máy xu ng Nh c máy Th i gian ñ i k t thúc Âm m i quay s B ms S sai Quay s Thông báo 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 L y t kho S n xu t P2 P1 C2 C1 G i vào kho Tiêu th G i vào kho G i vào kho 1 0 L y t kho 2 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 <1, P1, C1> <0, P1, C1> G i vào kho S n xu t <2, P1, C1> G i vào kho S n xu t L y t kho S n xu t L y t kho Tiêu th Tiêu th Tiêu th <1, P2, C1> <0, P2, C1> L y t kho <1, P1, C2> <0, P1, C2> <2, P2, C1> L y t kho Tiêu th <2, P1, C2> Tiêu th Tiêu th S n xu t S n xu t G i vào kho 16 <0, P2, C2> S n xu t G i vào kho <1, P2, C2> <2, P2, C2> 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 yellow rg gy 25 green M ng Petri Ví d 1: mô t ho t ñ ng c a 2 ñèn giao thông red2 red1 yr1 yr2 yellow1 rg1 gy2 gy1 26 rg2 yellow2 green1 green2 13 M ng Petri Ví d 1: mô t ho t ñ ng an toàn c a 2 ñèn giao thông red2 red1 safe yr1 rg1 yr2 yellow1 yellow2 gy1 27 rg2 gy2 green2 green1 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 yr2 yr1 rg1 rg2 yellow1 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 29 ly hôn 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 send_mail read_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 2 P9 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 P8 t6 2 t7 P9 2 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 C1 P2 Tiêu th G i vào kho G i vào kho G i vào kho 1 0 L y t kho C2 2 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 L y t kho 0 2 L y t kho 1 C1 G i vào kho 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 post ∀i, 1 ≤ i ≤ n, a[i] ≤ a[i+1] 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. 2. 3. S p x p m t danh sách các s nguyên ð o ngư c các ph n t c a m t danh sách ð 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 false ¬_ _∧_ _∨_ : → Boolean : → 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