Các kỹ thuật đặc tả

Phát triểnKhi một đặc tả hình thức đã được phát triển xong, đặc tả đó có thể được sử dụng làm một hướng dẫn trong quá trình hệ thống thực được phát triển (nghĩa là được hiện thực hóa trong phần mềm và/hoặc phần cứng). Ví dụ: Nếu đặc tả hình thức là một ngữ nghĩa hoạt động, hành vi được quan sát của hệ thống thực sẽ có thể được so sánh với hành vi trong đặc tả (chính đặc tả cũng nên chạy được hoặc giả lập được). Thêm vào đó, các lệnh hoạt động của đặc tả có thể thích hợp cho việc dịch thẳng mã chạy được.Nếu đặc tả hình thức là một ngữ nghĩa tiên đề, các tiền điều kiện và hậu điều kiện của đặc tả có thể trở thành các assertionIf the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become khẳng định (assertion') trong mã chạy được

pdf23 trang | Chia sẻ: tlsuongmuoi | Lượt xem: 2427 | Lượt tải: 0download
Bạn đang xem trước 20 trang tài liệu Các kỹ thuật đặc tả, để xem tài liệu hoàn chỉnh bạn click vào nút DOWNLOAD ở trên
1Cá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 2 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ả 23 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 ñề ñó 4 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 35 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 6 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 47 ðặ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ềm dẻo  thiếu sự chính xác  nhập nhằng 8 Ứ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 59 Chi phí phát triển khi sử dụng ñặc tả hình thức 10 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  ðặc tả Z 611 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 12 Máy 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 ðổ chuông ðàm thoại Âm mời quay số Nhấc máy Thời gian ñợi kết thúc Máy bận Thuê bao ñược gọi nhấc máy Thông báo quay số sai Số ñúng Số sai Bấm số Kết nối ñược 713 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 14 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 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ừ kho 2 Lấy từ kho Gửi vào kho Gửi vào kho 815 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 16 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 Lấy từ kho Gửi vào kho Tiêu thụ Tiêu thụ Sản xuất Sản xuất Tiêu thụ Tiêu thụ Sản xuất Sản xuất Tiêu thụ Tiêu thụ Sản xuất Sản xuất Lấy từ kho Gửi vào kho Lấy từ kho Gửi vào kho Lấy từ kho 917 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 18 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 10 19 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ẻ () 20 Mạng Petri  Ví dụ t2 p1 p2 p3 p4t3 t1 11 21 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 22 Mạng Petri  Ví dụ t1 t2 t1 không thể vượt qua ñược t2 có thể vượt qua ñược t3 t4 hoặc t3 ñược vượt qua hoặc t4 ñược vượt qua 12 23 Mạng Petri  Ví dụ khi t2 ñược vượt qua t2t2 24 Mạng Petri Ví dụ 13 25 Mạng Petri  Ví dụ 1: mô tả hoạt ñộng của ñèn giao thông rg red yellow green yr gy 26 Mạng Petri  Ví dụ 1: mô tả hoạt ñộng của 2 ñèn giao thông rg1 red1 yellow1 green1 yr1 gy1 rg2 red2 yellow2 green2 yr2 gy2 14 27 Mạng Petri  Ví dụ 1: mô tả hoạt ñộng an toàn của 2 ñèn giao thông rg1 red1 yellow1 green1 yr1 gy1 rg2 red2 yellow2 green2 yr2 gy2 safe 28 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 rg1 red1 yellow1 green1 yr1 gy1 rg2 red2 yellow2 green2 yr2 gy2 safe2 safe1 15 29 Mạng Petri  Ví dụ 2: mô tả chu kỳ sống của một người thanh niên trẻ con có vợ có chồng dậy thì cưới ly hôn chết chết 30 Mạng Petri  Ví dụ 3: viết thư và ñọc thư rest mail_box receive_mail type_mail ready rest begin send_mail read_mail 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ư ? 16 31 Mạng Petri  Ví dụ 4: tình huống nghẽn (dead-lock) 22 P6 P4 P3 P1 P8 t1 t3 t5 t7 P7 P5 P2 P9 t2 t4 t6 t8 32 22 Mạng Petri  Ví dụ 4: giải pháp chống nghẽn 22 P6 P4 P3 P1 P8 t1 t3 t5 t7 P7 P5 P2 P9 t2 t4 t6 t8 17 33 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 34 Mạng Petri  Ví dụ 5: mô tả tách rời mỗi thành phần P1 Sản xuất Gửi vào kho P2 Lấy từ kho C1 Tiêu thụ C2 0 Gửi vào kho 1 2 Gửi vào kho Lấy từ khoLấy từ kho 18 35 Lấy 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 khoP1 Sản xuất P2 0 1 2 C2 C1 Tiêu thụ 36 ð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 19 37 ð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) 38 ð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 20 39 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 40 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ự “_” 21 41 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 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ự “_” 42 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 22 43 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ó • 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 precondition 44 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 23 45 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 tập hợp

Các file đính kèm theo tài liệu này:

  • pdfCác kỹ thuật đặc tã.pdf