Xem mẫu

LOGO

Đặc tả hình thức
Design by contract

Nguyễn Thị Minh Tuyền

Nguyễn Thị Minh Tuyền

1

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, ...)

Nguyễn Thị Minh Tuyền

2

Đặ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 đó.

Nguyễn Thị Minh Tuyền

3

Đặ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.

Nguyễn Thị Minh Tuyền

4

Đặ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 đó.

Nguyễn Thị Minh Tuyền

5

Đặc tả hình thức

nguon tai.lieu . vn