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,...
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 7 - Nguyễn Thị Minh TuyềnLOGOĐặc tả hình thứcMô hình động trong AlloyNguyễn Thị Minh TuyềnNguyễn Thị Minh Tuyền1Các mô hình tĩnhv 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ácgiá trị thỏa mãn các ràng buộc được địnhnghĩa bởi multiplicity, fact,..Nguyễn Thị Minh Tuyền2Đặc tả hình thứcCác mô hình tĩnhPerson = {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ền3Đặc tả hình thứcMô hình độngv Các mô hình tĩnh cho phép mô tả trạngthá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ợplệ 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ếtNguyễn Thị Minh Tuyền4Đặc tả hình thứcVí 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ền5Đặc tả hình thức