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

LOGO<br /> <br /> Đặc tả hình thức<br /> JML nâng cao<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 /> v Aliasing<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Aliasing<br /> v Aliasing là nguồn gốc của mọi rắc rối<br /> phức tạp.<br /> v Lớp ArrayTimer minh họa cho điều<br /> này.<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> Ví dụ ArrayTimer<br /> v Sử dụng một mảng 6 số để biểu diễn<br /> giờ:phút:giây<br /> public class ArrayTimer{ <br /> char[] currentTime; <br /> char[] alarmTime; <br /> <br /> //@ invariant currentTime != null; <br /> //@ invariant currentTime.length == 6; <br /> //@ invariant alarmTime != null; <br /> //@ invariant alarmTime.length == 6; <br /> <br /> public void tick() { ... } <br /> <br /> public void setAlarm(...) { ... } <br /> }<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> Ví dụ ArrayTimer<br /> v Sẽ sai nếu các instance khác nhau của<br /> ArrayTimer cùng chia sẻ mảng<br /> alarmTime, nghĩa là<br /> §  o.alarmTime == o’.alarmTime<br /> §  cho o !=o’<br /> §  ESC/Java2 có thể chú ý đến điều này, sinh ra một<br /> cảnh báo đúng nhưng khó hiểu.<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />