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

• Kỹ thuật lập trình
• Bài giảng Đặc tả hình thức
• Đặc tả hình thức
• Design by contract
• Ngôn ngữ đặc tả
• Công cụ hỗ trợ
• Đặc tả hàm
• Đặc tả đệ quy
• Đặc tả hàm tường minh
• Đặc tả hàm không tường minh
• Lập trình phần mềm
• Công nghệ phần mềm
• Đặc tả phần mềm
• Ngôn ngữ đặc tả hình thức
• Đặc tả yêu cầu phần mềm
• Bài giảng Đặc tả yêu cầu phần mềm
• Công nghệ phần mềm nâng cao
• Phân loại đặc tả yêu cầu phần mềm
• Đặc tả phi hình thức phần mềm
• Đặc tả hình thức phần mềm
• Mô hình Thế giới thực
• Quy trình công nghệ phần mềm
• Ngôn ngữ hình thức
• Thiết kế ở mức cao
• Đặc tả ở mức mã nguồn
• JML nâng cao
• Từ khóa chính trong JML
• Các tính năng nâng cao
• Đặc tả các ngoại lệ
• Thừa kế đặc tả
• Các trường model
• Đặc tả không hình thức
• Phép toán vị từ
• Cơ sở đặc tả hình thức
• Luật suy diễn
• Cơ sở toán học trong đặc tả hình thức
• Hệ thống phần mềm
• Lỗi phần mềm
• Ngôn ngữ và hệ thống
• Các ngôn ngữ đặc tả
• Kiểm tra mô hình
• Mô hình hóa dữ liệu
• Kiểu dữ liệu
• Đặc tả operation
• Dữ liệu kiểu mảng
• Kiểu đối tượng phức
• Kiểu tập hợp
• Giới thiệu về ESC Java2
• Cách sử dụng và thuộc tính
• Cấu trúc của ESC
• Các file đặc tả
• Thủ thuật và cạm bẫy
• Đặc tả thừa kế
• Đặc tả sử dụng ánh xạ
• Kiểu ánh xạ
• Ngôn ngữ đặc tả Z
• Phép toán trên giản đồ