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

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