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

Bài giảng Đặc tả hình thức: Chương 3 do Nguyễn Thị Minh Tuyền biên soạn nhằm mục đích phục vụ cho việc giảng dạy. Nội dung bài giảng gồm Nguyên tử và quan hệ, signature và Field, các phép toán,...Mời các bạn cung tham khảo!
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 3 - Nguyễn Thị Minh Tuyền LOGO Đặc tả hình thức Giới thiệu về Alloy Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1 Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức Tài liệu tham khảo v Sách tham khảo: §  Software Abstractions: Logic, Language, and Analysis, Revised edition, Daniel Jackson, 2012 v Tải phần mềm + tài liệu + ví dụ mẫu: §  http://alloy.mit.edu/alloy/ Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức v Alloy chỉ là một trong các phương pháp phân tích và mô hình hóa theo hướng trừu tượng hóa phần mềm. §  B, OCL (Object Constraint Language), VDM (Vienna Development Method), Z. v Điểm chung: §  Cung cấp những khái niệm về trừu tượng hóa phần mềm một cách ngắn gọn và trực tiếp hơn so với các ngôn ngữ lập trình. §  Dựa vào cấu trúc toán học cổ điển: tập hợp và quan hệ §  Mô tả hành vi (behavior) theo kiểu khai báo. §  Sử dụng các ràng buộc. Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức Một số điểm khác nhau v B §  Khái niệm của nó hơi giống ngôn ngữ lập trình trừu tượng hơn là ngôn ngữ đặc tả. v OCL §  Rất khác về mặt cú pháp v B, VDM và Z được thiết kế thiên về chứng minh (proof) hơn là phân tích đơn giản. v B, VDM và Z diễn đạt tốt hơn Alloy §  Cấu trúc của Alloy chỉ hỗ trợ logic bậc nhất (first order logic) §  Các ngôn ngữ khác hỗ trợ cả cấu trúc bậc cao và cả quantification nữa. v Alloy hỗ trợ kém về số nguyên và chuỗi Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức