Đặc tả hình thức - Design by contract - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền Design by contract Nguyễn Thị Minh Tuyền 1 Đặc tả hình thức 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, ...) 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 đó. 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ý 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. 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 đó. 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức Air travel Client(Hành khách) §  Obligation •  Check in 30 phút trước khi máy bay cất cánh •  Ít hơn 3 kiện hành lý •  Trả tiền vé §  Benefit •  đến đích 6 Nguyễn Thị Minh Tuyền Supplier(Hãng hàng không) §  Obligation •  Đưa hành khách đến đích. §  Benefit •  Không cần đợi các hành khách đi trễ •  Không cần thiết phải lưu trữ số lượng hành lý •  Nhận tiền Đặc tả hình thức 7 Nguyễn Thị Minh Tuyền /*@ 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ố không âm x Lấy xấp xỉ căn bậc hai của x Supplier Tính toán và trả về căn bậc hai của một số Giả sử rằng tham số đầu vào là không âm Đặc tả hình thức 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 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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) {} } 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 10 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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() { ... } } 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức /*@ invariant top >= -1 && top < size; @*/ Class Mystack { private Object[] elems; private int top, size; } 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức Class Mystack { private Object[] elems; private int top, size; /*@ requires s > 0; ensures size == s && elems != null && top = -1; @*/ public MyStack (int s) { } } 13 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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() { ... } } 14 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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() { ... } } 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức Class Mystack { private Object[] elems; private int top, size; /*@ ensures \result top == -1; @*/ public boolean isEmpty() { ... } } 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức Class Mystack { private Object[] elems; private int top, size; /*@ ensures \result top == size – 1; @*/ public boolean isFull() { ... } } 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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(); .... } 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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); } 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 ... 20 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 21 Nguyễn Thị Minh Tuyền LOGO