Bài giảng Công nghệ phần mềm: Chương 4 - Nguyễn Thanh Bình

1 Các kỹ thuật ñặc Thanh Bình Khoa Công ngh ệ Thông ðại học Bách khoa ðại học ðà 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 niệm ñặc tả � ðặc tả � ñị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 ñề 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 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 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 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 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ử loại các kỹ thuật ñặc tả � ðặc tả phi hình thức 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 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 kí hiệu toán học • ngôn ngữ ñặc tả • ngôn ngữ lập 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ềm dẻo � thiếu sự chính xác � nhập 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 hệ thống ñiều khiển � hệ thống nhúng � hệ thống thời gian phí phát triển khi sử dụng ñặc tả hình 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 � ðặc tả trạng thái hữu 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 trạng thái hữu hạn � Ví dụ 1 ðặt máy xuốngðặt máy xuống ðợi Quay số Kết nối ðổ thoại Âm mời quay số Nhấc máy Thời gian ñợi kết bận Thuê bao ñược gọi nhấc báo quay số sai Số ñúng Số sai Bấm số Kết nối 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 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 P1 P2 Sản xuất Gửi vào kho C1 C2 Tiêu thụ Lấy từ kho 0 1 Lấy từ từ kho Gửi vào kho Gửi vào trạng thái hữu hạn � Giải pháp 1 � không mô tả ñược sự hoạt ñộng cần mô tả sự hoạt ñộng kết hợp các thành phần của hệ 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 Lấy từ kho Gửi vào kho Tiêu thụ Tiêu thụ Sản xuất Sản xuất <0, P2, C2> <0, P2, C1> <0, P1, C2> <0, P1, C1> Tiêu thụ Tiêu thụ Sản xuất Sản xuất <1, P2, C2> <1, P2, C1> <1, P1, C2> <1, P1, C1> Tiêu thụ Tiêu thụ Sản xuất Sản xuất <2, P2, C2> <2, P2, C1> <2, P1, C2> <2, P1, C1> Lấy từ kho Gửi vào kho Lấy từ kho Gửi vào kho Lấy từ 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 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ở 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ẻ Petri � Ví 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 Petri � Ví dụ t1 t2 t1 không th ể vượt qua ñược t2 có th ể vượt qua t3 ñược vượt qua hoặc t4 ñược vượt Petri � Ví dụ khi t2 ñược vượt Petri Ví Petri � Ví dụ 1: mô tả hoạt ñộng của ñèn giao Petri � Ví dụ 1: mô tả hoạt ñộng của 2 ñèn giao Petri � Ví dụ 1: mô tả hoạt ñộng an toàn của 2 ñèn giao Petri � Ví dụ 1: mô tả hoạt ñộng an toàn và hợp lý của 2 ñèn giao Petri � Ví dụ 2: mô tả chu kỳ sống của một niên trẻ con có vợ có hôn chết Petri � Ví dụ 3: viết thư và ñọc 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ư Petri � Ví dụ 4: tình huống nghẽn Petri � Ví dụ 4: giải pháp chố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 Petri � Ví dụ 5: mô tả tách rời mỗi thành xuất Gửi vào từ vào kho 1 2 Gửi vào kho Lấy từ khoLấy từ từ kho Mạng Petri � Ví dụ 5: mô tả kết hợp các thành phần Lấy từ kho Gửi vào kho Gửi vào 1 kiện trước và ñượ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 � : ñặc tả các ràng buộc trên các tham số trước khi hàm ñược thực thi � : ñặ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 trước và sau � Ví dụ: ñặc tả hàm tìm 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] ≤ result = (∃i, 1 ≤ i ≤ n, a[i] = 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ố trừu 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 các thao tác trên trên kiểu trừu tượng • dùng từ khóa trừu tượng � Ví dụ 1: ñặc tả kiểu trừu tượng : →→→→ : →→→→ _ : Boolean →→→→ Boolean _ ∧∧∧∧ _ : Boolean x Boolean →→→→ Boolean _ ∨∨∨∨ _ : Boolean x Boolean →→→→ 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ự trừu tượng � Ví dụ 2: ñặc tả kiểu trừu tượng : →→→→ : →→→→ _ : Boolean →→→→ Boolean _ ∧∧∧∧ _ : Boolean x Boolean →→→→ Boolean _ ∨∨∨∨ _ : Boolean x Boolean →→→→ 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ự trừu tượng � Ví dụ 2: ñặc tả kiểu trừu tượng Integer, Element, : Integer x Integer →→→→ : Vector x Integer →→→→ : Vector x Integer →→→→ : Vector x Integer x Element →→→→ : Vector →→→→ : Vector →→→→ 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ó • tức là ý nghĩa của thao tác � sử dụng 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à một thao tác ñược ñịnh nghĩa • dùng từ khóa trừu tượng � Ví dụ 2: ñặc tả kiểu trừu tượng i) ≤≤≤≤ i ≤≤≤≤ &&&& init(v,i) = ≤≤≤≤ i ≤≤≤≤ ⇒⇒⇒⇒ i, e), i) = ≤≤≤≤ i ≤≤≤≤ &&&& ≤≤≤≤ j ≤≤≤≤ &&&& i ≠≠≠≠ j i, e), j) = ith(v, j), k) = ≤≤≤≤ i ≤≤≤≤ ⇒⇒⇒⇒ i, e), i) = ≤≤≤≤ i ≤≤≤≤ &&&& i ≠≠≠≠ j ⇒⇒⇒⇒ i, e), j) = init(v, j)) = i, e)) = j)) = i, e)) = Vector; i, j, k: Integer; e: 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 tập hợp