Bài giảng Đặc tả hình thức: Chương 13 - Nguyễn Thị Minh Tuyền

LOGO

Đặc tả hình thức
Giới thiệu về ESC/Java2
Cảnh báo

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

Các loại cảnh báo ESC/Java2
v Các cảnh báo ESC/Java2 thường rơi vào các
mục sau:
§  Cảnh báo về ngoại lệ khi thực thi (runtime exception)(Cast, Null,
NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore).
•  Đây là các ngoại lệ khi thực thi phổ biến nhất gây ra bởi các
vấn đề khi lập trình.
•  Không chứa tất cả các ngoại lệ khi thực thi.

Nguyễn Thị Minh Tuyền

2

Đặc tả hình thức

Cast warning
v Cảnh báo Cast xảy ra khi ESC/Java2 không
thể kiểm tra rằng một ClassCastException sẽ
không được đưa ra.
public class CastWarning {
public void m(Object o) {

String s = (String)o;
}
}

sinh ra
-----------------------------------------------------------------------CastWarning.java:3: Warning: Possible type cast error (Cast)
String s = (String)o;
ˆ
-----------------------------------------------------------------------Nguyễn Thị Minh Tuyền

3

Đặc tả hình thức

Cast warning
Nhưng sẽ OK nếu ta viết:
public class CastWarningOK {
public void m(Object o) {

if (o instanceof String) {


String s = (String)o;

}
}

}
Với đặc tả JML:
public class CastWarningOK2 {
//@ requires o instanceof String;
public void m(Object o) {

String s = (String)o;
}
}
Nguyễn Thị Minh Tuyền

4

Đặc tả hình thức

Null warning
v  Cảnh báo Null xảy ra khi ESC/Java2 không thể kiểm
tra rằng NullPointerException sẽ không được đưa ra.
public class NullWarning {
public void m(Object o) {

int i = o.hashCode();
}
}
Kết quả:
-----------------------------------------------------------------------NullWarning.java:3: Warning: Possible null dereference (Null)
int i = o.hashCode();
ˆ
-----------------------------------------------------------------------Sẽ OK nếu ta viết:
public class NullWarningOK {
public void m(/*@ non_null */ Object o) {

int i = o.hashCode();
}
}
Nguyễn Thị Minh Tuyền

5

Đặc tả hình thức