Xem mẫu

LOGO

Đặc tả hình thức
JML nâng cao

Nguyễn Thị Minh Tuyền

Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll

1

v Aliasing

Nguyễn Thị Minh Tuyền

2

Đặc tả hình thức

Aliasing
v Aliasing là nguồn gốc của mọi rắc rối
phức tạp.
v Lớp ArrayTimer minh họa cho điều
này.

Nguyễn Thị Minh Tuyền

3

Đặc tả hình thức

Ví dụ ArrayTimer
v Sử dụng một mảng 6 số để biểu diễn
giờ:phút:giây
public class ArrayTimer{
char[] currentTime;
char[] alarmTime;

//@ invariant currentTime != null;
//@ invariant currentTime.length == 6;
//@ invariant alarmTime != null;
//@ invariant alarmTime.length == 6;

public void tick() { ... }

public void setAlarm(...) { ... }
}
Nguyễn Thị Minh Tuyền

4

Đặc tả hình thức

Ví dụ ArrayTimer
v Sẽ sai nếu các instance khác nhau của
ArrayTimer cùng chia sẻ mảng
alarmTime, nghĩa là
§  o.alarmTime == o’.alarmTime
§  cho o !=o’
§  ESC/Java2 có thể chú ý đến điều này, sinh ra một
cảnh báo đúng nhưng khó hiểu.

Nguyễn Thị Minh Tuyền

5

Đặc tả hình thức

nguon tai.lieu . vn