Giáo trình Đặc tả hình thức - Chương 9: Design by contract - Nguyễn Thị Minh Tuyền

Nội dung text: Giáo trình Đặc tả hình thức - Chương 9: Design by contract - Nguyễn Thị Minh Tuyền

1. LOGO Đặc tả hình thức Design by contract Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1
2. Từ mô hình đến cài đặt v Alloy là một phương tiện để thiết kế hệ thống và diễn giải các thuộc tính. v Ta cần các thiết kế hệ thống này để cải thiện chất lượng của việc cài đặt. v Làm thế nào để chuyển đổi các thông tin thiết kế này thành mã nguồn? § Thông tin tĩnh ( multiplicity, invariant ) § Thông tin về các thao tác (điều kiện trước, điều kiện sau, frame condition, ) Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
3. Design by contract (DBC) v Là một phương pháp chú trọng vào việc mô tả chính xác về ngữ nghĩa interface § không chỉ về cú pháp, ví dụ như signature § mà còn cả về các hành vi, ví dụ như hiệu ứng việc triệu gọi một phương thức. v Được hỗ trợ bằng công cụ § cho phép các thuộc tính ngữ nghĩa của thiết kế (mô hình) được chuyển tải thành mã nguồn. § hỗ trợ một số hình thức thẩm định các thuộc tính đó. Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
4. Ý tưởng cơ bản v Phần mềm được xem là § một hệ thống của các component giao tiếp với nhau § tất cả các tương tác đều dựa vào ràng buộc (contract) v Ràng buộc có tính hai chiều § cả hai phần được ràng buộc lẫn nhau. Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức
5. Ràng buộc v Hai phần của một ràng buộc: § Supplier thực hiện một tác vụ § Client yêu cầu tác vụ đó phải được thực hiện. v Mỗi phần § có các obligation. § nhận một số benefit. v Ràng buộc đặc tả các obligation và các benefit đó. Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
6. Air travel Client(Hành khách) Supplier(Hãng hàng không) § Obligation § Obligation • Check in 30 phút trước • Đưa hành khách đến khi máy bay cất cánh đích. • Ít hơn 3 kiện hành lý § Benefit • Trả tiền vé • Không cần đợi các § Benefit hành khách đi trễ • Không cần thiết phải • đến đích lưu trữ số lượng hành lý • Nhận tiền Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
7. /*@ requires x >= 0.0; @ ensures JMLDouble.approximatelyEqualTo(x, @ \result * \result, eps); @*/ public static double sqrt(double x) { } Obligation Benefit Client Chuyển một số Lấy xấp xỉ căn bậc không âm x hai của x Supplier Tính toán và trả về Giả sử rằng tham căn bậc hai của số đầu vào là một số không âm Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
8. Ràng buộc v Đặc tả cái gì phải làm § các ràng buộc được cài đặt độc lập nhau v Có thể được áp dụng cho phần mềm sử dụng § Điều kiện trước § Điều kiện sau § Frame condition § Bất biến Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
9. Ví dụ Class Flight { /*@ requires time < this.takeoff – 30 && l.number < 3 && p in this.ticketed ensures \result = this.destination @*/ Destination takeFlight(Person p, Luggage l) { } } Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
10. Ngôn ngữ đặc tả hay ngôn ngữ lập trình v Tại sao không phải là cả hai? v Phương pháp tinh chỉnh § Thay vì chỉ phát triển các signature § Phát triển đặc tả ràng buộc § Phân tích tính nhất quán client-supplier § Thêm vào các chi tiết cài đặt § Kiểm tra rằng mã nguồn thỏa mãn ràng buộc v Tiến trình tự nhiên từ thiết kế đến mã nguồn. Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
11. Ví dụ Class Mystack { private Object[] elems; private int top, size; public MyStack (int s) { } public void push (Object obj) { } public Object pop() { } public boolean isEmpty() { } public boolean isFull() { } } Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
12. /*@ invariant top >= -1 && top < size; @*/ Class Mystack { private Object[] elems; private int top, size; } Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
13. Class Mystack { private Object[] elems; private int top, size; /*@ requires s > 0; ensures size == s && elems != null && top = -1; @*/ public MyStack (int s) { } } Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức
14. Class Mystack { private Object[] elems; private int top, size; /*@ requires !isFull() && obj != null; ensures top == \old(top) + 1 && elems[top] == obj;@*/ public void push (Object obj) { } public boolean isFull() { } } Nguyễn Thị Minh Tuyền 14 Đặc tả hình thức
15. Class Mystack { private Object[] elems; private int top, size; /*@ requires !isEmpty(); ensures top == \old(top) - 1 && \result == elems[\old(top)];@*/ public Object pop() { } public boolean isEmpty() { } } Nguyễn Thị Minh Tuyền 15 Đặc tả hình thức
16. Class Mystack { private Object[] elems; private int top, size; /*@ ensures \result top == -1; @*/ public boolean isEmpty() { } } Nguyễn Thị Minh Tuyền 16 Đặc tả hình thức
17. Class Mystack { private Object[] elems; private int top, size; /*@ ensures \result top == size – 1; @*/ public boolean isFull() { } } Nguyễn Thị Minh Tuyền 17 Đặc tả hình thức
18. Ví dụ 2 import java.util.Vector; public interface Company { public Vector getEmployees(); public Vector getRooms(); public void hire(Employee e); public void move(Employee e, Room r); public boolean roomsAvailable(); } public interface Employee{ public boolean hasOffice(); } Nguyễn Thị Minh Tuyền 18 Đặc tả hình thức
19. import java.util.Vector; public interface Company { public Vector getEmployees(); public Vector getRooms(); public boolean roomsAvailable(); /* Contract for hire(Employee e) */ /*@ requires e != null; requires !getEmployees().contains(e); // do not employ twice requires !e.hasOffice(); // does not own an office somewhere else requires roomsAvailable(); // there must be an office left ensures getEmployees().contains(e); // added to list of employees ensures getRooms().contains(e.getOffice()); // assign one of our offices ensures e.hasOffice(); // office assigned @*/ public void hire(Employee e); } Nguyễn Thị Minh Tuyền 19 Đặc tả hình thức
20. Công cụ hỗ trợ v Jtest(Jcontract) § Sản phẩm thương mại v iContract § Phần mềm miễn phí, nhưng cần nhiều công cụ hỗ trợ v JML § dự án nghiên cứu § có vài công cụ hỗ trợ miễn phí v Nguyễn Thị Minh Tuyền 20 Đặc tả hình thức
21. Design by Contract trong môn học này v Tập trung vào Java và sử dụng § JML như là một đặc tả § ESC/Java 2 là công cụ kiểm tra chính Nguyễn Thị Minh Tuyền 21 Đặc tả hình thức