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

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