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

LOGO<br /> <br /> Đặc tả hình thức<br /> Giới thiệu về ESC/Java2<br /> Cảnh báo<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll<br /> <br /> 1<br /> <br /> Các loại cảnh báo ESC/Java2<br /> v Các cảnh báo ESC/Java2 thường rơi vào các<br /> mục sau:<br /> §  Cảnh báo về ngoại lệ khi thực thi (runtime exception)(Cast, Null,<br /> NegSize, IndexTooBig, IndexNegative, ZeroDiv, ArrayStore).<br /> •  Đây là các ngoại lệ khi thực thi phổ biến nhất gây ra bởi các<br /> vấn đề khi lập trình.<br /> •  Không chứa tất cả các ngoại lệ khi thực thi.<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Cast warning<br /> v Cảnh báo Cast xảy ra khi ESC/Java2 không<br /> thể kiểm tra rằng một ClassCastException sẽ<br /> không được đưa ra.<br /> public class CastWarning { <br /> public void m(Object o) { <br /> <br /> String s = (String)o; <br /> } <br /> } <br /> <br /> sinh ra<br /> -----------------------------------------------------------------------CastWarning.java:3: Warning: Possible type cast error (Cast)<br /> String s = (String)o;<br /> ˆ<br /> -----------------------------------------------------------------------Nguyễn Thị Minh Tuyền<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> Cast warning<br /> Nhưng sẽ OK nếu ta viết:<br /> public class CastWarningOK { <br /> public void m(Object o) { <br /> <br /> if (o instanceof String) { <br /> <br /> <br /> String s = (String)o; <br /> <br /> } <br /> } <br /> <br /> }<br /> Với đặc tả JML:<br /> public class CastWarningOK2 { <br /> //@ requires o instanceof String; <br /> public void m(Object o) { <br /> <br /> String s = (String)o; <br /> } <br /> } <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> Null warning<br /> v  Cảnh báo Null xảy ra khi ESC/Java2 không thể kiểm<br /> tra rằng NullPointerException sẽ không được đưa ra.<br /> public class NullWarning { <br /> public void m(Object o) { <br /> <br /> int i = o.hashCode(); <br /> } <br /> }<br /> Kết quả:<br /> -----------------------------------------------------------------------NullWarning.java:3: Warning: Possible null dereference (Null)<br /> int i = o.hashCode();<br /> ˆ<br /> -----------------------------------------------------------------------Sẽ OK nếu ta viết:<br /> public class NullWarningOK { <br /> public void m(/*@ non_null */ Object o) { <br /> <br /> int i = o.hashCode(); <br /> } <br /> } <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />