LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
Giới thiệu về Alloy
Nguyễn Thị Minh Tuyền 1
Đặc tả hình thức
Nội dung
v Nguyên tử và quan hệ
v Signature và Field
v Các phép toán
2
Nguyễn Thị Minh Tuyền
Đặ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/
3
Nguyễn Thị Minh Tuyền
Đặ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.
4
Nguyễn Thị Minh Tuyền
Đặ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
5
Nguyễn Thị Minh Tuyền