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

Nội dung chương 7 trình bày đến người học những vấn đề liên quan đến "Mô hình động trong Alloy", cụ thể như: Các mô hình tĩnh, mô hình hóa chuyển đổi trạng thái, signature mang tính chất tĩnh, các chuỗi trạng thái, biểu diễn một chuyển đổi,. | LOGO Đặc tả hình thức Mô hình động trong Alloy Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1 Các mô hình tĩnh v  Trong các buổi học trước §   định nghĩa các mô hình dựa vào tập hợp và quan hệ v  Một instance của mô hình là một tập các giá trị thỏa mãn các ràng buộc được định nghĩa bởi multiplicity, fact, Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức Các mô hình tĩnh Person = {Matt, Sue} Man = {Matt} Woman = {Sue} Married = {} spouse = {} children = {} siblings = {} Person = {Matt, Sue} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {} siblings = {} Person = {Matt, Sue, Sean} Man = {Matt} Woman = {Sue} Married = {Matt, Sue} spouse = {(Matt,Sue), (Sue,Matt)} children = {(Matt,Sean), (Sue,Sean)} siblings = {} Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức Mô hình động v  Các mô hình tĩnh cho phép mô tả trạng thái hợp lệ của một hệ thống động. v  Ta cũng có thể mô tả các chuyển đổi hợp lệ giữa các trạng thái. v  Ví dụ: §   Một người được sinh ra trước khi họ cưới §   Một người kết hôn trước khi có con §   Một người là con cho đến khi họ chết Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức Ví dụ abstract sig Person { children: set Person, siblings: set Person } sig Man, Woman extends Person {} sig Married in Person { spouse: one Married } Nguyễn Thị Minh Tuyền 5 Đặc tả hình .