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

Bài giảng Đặc tả hình thức: Chương 9 cung cấp cho người học các kiến thức: Từ mô hình đến cài đặt, design by contract (DBC), ý tưởng cơ bản, ngôn ngữ đặc tả hay ngôn ngữ lập trình, công cụ hỗ trợ,...
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 9 - Nguyễn Thị Minh Tuyền 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