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

Nội dung chương 12 trình bày đến người học những vấn đề liên quan đến "Giới thiệu về ESC/Java2 Thủ thuật và cạm bẫy", cụ thể như: Đặc tả thừa kế, Aliasing, Object invariants, giả thuyết không nhất quán, Exposed references, old, viết đặc tả thế nào,. | LOGO Đặc tả hình thức Giới thiệu về ESC/Java2 Thủ thuật và cạm bẫy 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 Nội dung 1.  Đặc tả thừa kế 2.  Aliasing 3.  Object invariants 4.  Giả thuyết không nhất quán 5.  Exposed references 6.  \old 7.  Viết đặc tả thế nào Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức Nội dung 1.  Đặc tả thừa kế 2.  Aliasing 3.  Object invariants 4.  Giả thuyết không nhất quán 5.  Exposed references 6.  \old 7.  Viết đặc tả thế nào Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức Behavioural subtyping v  Giả sử rằng Child mở rộng từ Parent §   Behavioural subtyping = các đối tượng từ lớp con Child ứng xử giống các đối tượng từ lớp cha Parent. §   Nguyên tắc: mã nguồn sẽ ứng xử như mong đợi nếu ta khai báo một đối tượng Child trong đó một đối tượng Parent đã được cài đặt như mong đợi. Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức Behavioural subtyping v  Một số ràng buộc bởi behavioural subtyping: §   Bất biến trong lớp con mạnh hơn bất biến trong lớp cha. §   Đối với mỗi phương thức: •  Điều kiện trước trong lớp con yếu hơn điều kiện trước trong lớp cha •  Điều kiện sau trong lớp con mạnh hơn điều kiện sau trong lớp cha. v  JML đạt được behavioural subtyping bằng kế thừa đặc tả: bất cứ lớp con nào cũng kế thừa đặc tả từ lớp cha của nó. 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
• Giới thiệu về ESC Java2
• Thủ thuật và cạm bẫy
• Đặc tả thừa kế
• Đặ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
• JML nâng cao
• 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ả
• Các trường model
• Đặc tả không hình thức
• 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ợ
• Cách sử dụng và thuộc tính
• Cấu trúc của ESC
• Các file đặc tả
• Đặ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 đồ