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

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

• 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 cảnh báo
• Các loại cảnh báo ESC Java2
• Deadlock warnings
• Đặ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ợ
• 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 đồ