TAILIEUCHUNG - 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 .

• Kỹ thuật lập trình
• Bài giảng Đặc tả hình thức
• Đặc tả hình thức
• JML nâng cao
• Các trường model
• Đặc tả không hình thức
• Đặc tả hàm
• Đặc tả đệ quy
• Đặc tả hàm tường minh
• Đặc tả hàm không tường minh
• Lập trình phần mềm
• Công nghệ phần mềm
• Đặc tả phần mềm
• Ngôn ngữ đặc tả hình thức
• Đặc tả yêu cầu phần mềm
• Bài giảng Đặc tả yêu cầu phần mềm
• Công nghệ phần mềm nâng cao
• Phân loại đặc tả yêu cầu phần mềm
• Đặc tả phi hình thức phần mềm
• Đặc tả hình thức phần mềm
• Mô hình Thế giới thực
• Quy trình công nghệ phần mềm
• Ngôn ngữ hình thức
• Thiết kế ở mức cao
• Đặc tả ở mức mã nguồn
• Từ khóa chính trong JML
• Các tính năng nâng cao
• Đặc tả các ngoại lệ
• Thừa kế đặc tả
• Phép toán vị từ
• Cơ sở đặc tả hình thức
• Luật suy diễn
• Cơ sở toán học trong đặc tả hình thức
• Hệ thống phần mềm
• Lỗi phần mềm
• Ngôn ngữ và hệ thống
• Các ngôn ngữ đặc tả
• Kiểm tra mô hình
• Mô hình hóa dữ liệu
• Kiểu dữ liệu
• Đặc tả operation
• Dữ liệu kiểu mảng
• Kiểu đối tượng phức
• Kiểu tập hợp
• Design by contract
• Ngôn ngữ đặc tả
• Công cụ hỗ trợ
• Giới thiệu về ESC Java2
• Cách sử dụng và thuộc tính
• Cấu trúc của ESC
• Các file đặc tả
• Thủ thuật và cạm bẫy
• Đặc tả thừa kế
• Đặc tả sử dụng ánh xạ
• Kiểu ánh xạ
• Ngôn ngữ đặc tả Z
• Phép toán trên giản đồ