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

Cùng nắm kiến thức trong chương này thông qua việc tìm hiểu các nội dung sau: Từ khóa chính trong JML, các tính năng nâng cao, đặc tả các ngoại lệ, ngoại lệ được cho phép bởi đặc tả, đặt ra luật cho ngoại lệ, hành vi ngoại lệ,... 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 Từ khóa chính trong JML v requires v ensures v signals v assignable v normal_behavior v invariant v non_null v pure v \old,

Thể loại Tài liệu miễn phí Kỹ thuật lập trình

Số trang 28

Ngày tạo 8/30/2018 5:43:37 AM +00:00

Loại tệp PDF

Kích thước

Tên tệp

Tải Bài giảng Đặc tả hình thức: Chương 14 - Nguyễn Thị... (.pdf)

Xem mẫu

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

Từ khóa chính trong JML
v requires
v ensures
v signals
v assignable
v normal_behavior
v invariant
v non_null
v pure
v \old, \forall, \exists, \result
Nguyễn Thị Minh Tuyền

2

Đặc tả hình thức

Các tính năng nâng cao
v Visibility
v Đặc tả các ngoại lệ
v Mệnh đề assignable và nhóm dữ liệu
v Aliasing
v Thừa kế đặc tả, ensuring behavioural
subtyping
v Các trường chỉ ở mức đặc tả: ghost và
model
v Ngữ nghĩa của invariant

Nguyễn Thị Minh Tuyền

3

Đặc tả hình thức

v Visibility

Nguyễn Thị Minh Tuyền

4

Đặc tả hình thức

Visibility
v JML áp dụng các quy tắt về visibility
tương tự như Java.
v Ví dụ:
public class Bag{
...
private int n;
//@ requires n > 0;
public int extractMin(){ ... }

không phải là kiểu hợp lệ, vì visibility
của phương thức extractMin là public
chỉ đến trường n có visibility là private.
Nguyễn Thị Minh Tuyền

5

Đặc tả hình thức

nguon tai.lieu . vn

Tin học văn phòng Đồ họa - Thiết kế - Flash Quản trị Web Cơ sở dữ liệu Quản trị mạng Kỹ thuật lập trình Hệ điều hành Phần cứng An ninh - Bảo mật Chứng chỉ quốc tế Thủ thuật máy tính Điện - Điện tử Kinh tế học Hoá học Xã hội học Môi trường