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

Aliasing là nguồn gốc của mọi rắc rối phức tạp. Bài giảng Đặc tả hình thức: Chương 15 do Nguyễn Thị Minh Tuyền biên soạn sau đây sẽ giúp các bạn nắm rõ kiến thức về Aliasing, trường Ghost, các trường model,.! | 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 == 6; //@ invariant alarmTime != null; //@ invariant == 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 §   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 .