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