LOGO

Đặc tả hình thức

Design by contract

Nguyễn Thị Minh Tuyền

Nguyễn Thị Minh Tuyền 1

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)

Supplier(Hãng hàng không) §  Obligation

§  Obligation

•  Đưa hành khách đến

đích. §  Benefit

•  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

•  Không cần đợi các 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

6 Nguyễn Thị Minh Tuyền Đặc tả hình thức

/*@ 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

7 Nguyễn Thị Minh Tuyền Đặ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;

ensures size == s && elems != null && top = -1; @*/

/*@ requires s > 0; 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 {

\result == elems[\old(top)];@*/

private Object[] elems; private int top, size; /*@ requires !isEmpty(); ensures top == \old(top) - 1 && 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 Đặc tả hình thức

LOGO