LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
Design by contract
Nguyễn Thị Minh Tuyền 1
Đặc tả hình thức
Từ mô hình đến cài đặt
v Alloy là một phương tiện để thiết kế
hệ thống và diễn giải các thuộc tính.
v Ta cần các thiết kế hệ thống này để
cải thiện chất lượng của việc cài đặt.
v Làm thế nào để chuyển đổi các thông
tin thiết kế này thành mã nguồn?
§ Thông tin tĩnh ( multiplicity, invariant...)
§ Thông tin về các thao tác (điều kiện trước, điều kiện
sau, frame condition, ...)
2
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Design by contract (DBC)
v Là một phương pháp chú trọng vào
việc mô tả chính xác về ngữ nghĩa
interface
§ không chỉ về cú pháp, ví dụ như signature
§ mà còn cả về các hành vi, ví dụ như hiệu ứng việc
triệu gọi một phương thức.
v Được hỗ trợ bằng công cụ
§ cho phép các thuộc tính ngữ nghĩa của thiết kế (mô
hình) được chuyển tải thành mã nguồn.
§ hỗ trợ một số hình thức thẩm định các thuộc tính đó.
3
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Ý tưởng cơ bản
v Phần mềm được xem là
§ một hệ thống của các component giao tiếp với nhau
§ tất cả các tương tác đều dựa vào ràng buộc
(contract)
v Ràng buộc có tính hai chiều
§ cả hai phần được ràng buộc lẫn nhau.
4
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Ràng buộc
v Hai phần của một ràng buộc:
§ Supplier thực hiện một tác vụ
§ Client yêu cầu tác vụ đó phải được thực hiện.
v Mỗi phần
§ có các obligation.
§ nhận một số benefit.
v Ràng buộc đặc tả các obligation và
các benefit đó.
5
Nguyễn Thị Minh Tuyền