LOGO
Đặc tả hình thức
Tuần 1: Giới thiệu
Nguyễn Thị Minh Tuyền
Nguyễn Thị Minh Tuyền 1
v Giảng viên lý thuyết: § Nguyễn Thị Minh Tuyền § FIT, trường ĐH Khoa học Tự nhiên tp Hồ Chí Minh § Email: ntmtuyen@fit.hcmus.edu.vn § Website: http://www.tuyennguyen.info/teaching.html
• Được cập nhật thường xuyên. v Giảng viên thực hành:
2 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Thông tin về môn học và tài liệu
v Không có giáo trình v Slide của môn này dựa vào slide của môn Formal Methods in Software Engineering của trường Đại học Iowa.
v Sách tham khảo về kiến thức logic
§ Logic in Computer Science. M. Huth and M. Ryan. Cambridge University Press, 2004 (2nd edition).
§ Handbook of Practical Logic and Automated Reasoning.
John Harrison. Intel Corporation, Portland, Oregon.
3 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Mục tiêu của môn học
v Tập trung vào đặc tả hình thức. v Giới thiệu thêm về phương pháp hình thức. v Hiểu được phương pháp hình thức hỗ trợ cho việc tạo ra các phần mềm có chất lượng cao như thế nào. v Học về mô hình hóa hình thức và các ngôn ngữ đặc
tả.
v Viết và hiểu các đặc tả yêu cầu hình thức. v Học về các phương pháp hình thức chính để kiểm
định phần mềm.
v Biết được sử dụng phương pháp hình thức nào và khi
nào.
v Sử dụng các công cụ tương tác và tự động để kiểm
định mô hình và mã nguồn.
4 Nguyễn Thị Minh Tuyền Đặc tả hình thức
v Nội dung chính của môn này tập trung vào thiết kế ngữ nghĩa ở mức cao và các thuộc tính ở mức mã nguồn.
v Nhấn mạnh và đặc tả dựa vào công cụ và các phương pháp thẩm định (validation methods)
5 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phần I: Thiết kế ở mức cao
v Kiến thức chung về logic v Ngôn ngữ Alloy
§ Là ngôn ngữ mô hình hóa đơn giản cho thiết kế phần mềm. § Dễ dàng phân tích tự động một cách hoàn chỉnh § Nhắm vào việc diễn đạt các hành vi và ràng buộc cấu trúc phức
tạp trong một hệ thống phần mềm.
§ Công cụ mô hình hóa trực quan sử dụng logic bậc nhất (first-order
logic).
§ Phân tích tự động dùng SAT solving.
v Sau khi học xong, SV sẽ biết
§ Thiết kế và mô hình hóa các hệ thống sử dụng ngôn ngữ Alloy § Kiểm tra mô hình và các thuộc tính của nó bằng Alloy Analyzer § Hiểu cái gì có thể và không thể diễn đạt được bằng Alloy.
6 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phần II: Đặc tả ở mức mã nguồn
v Một số ngôn ngữ đặc tả ở mức mã
nguồn: § JML (Java Modeling Language) (Java) § Dafny (C#) § Krakatoa (Java/C) § ACSL (ANSI/ISO C Specification Language)(C) § …
7 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Phần II: Đặc tả ở mức mã nguồn
v Ngôn ngữ : JML (Java)
§ Dựa vào mô hình thiết kế dựa vào ràng buộc (design by
contract).
§ Đặc tả được “nhúng” trong mã nguồn. § Nhiều công cụ kiểm thử có sẵn. v Sau khi học xong SV sẽ biết
§ Viết các ràng buộc và đặc tả hình thức dùng JML. § Hiểu mã nguồn và đặc tả được biểu diễn bằng logic như
thế nào.
§ Kiểm thử các thuộc tính hàm của chương trình bằng các
công cụ tự động.
8 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Đánh giá môn học
v Thực hành (30%). v Thi giữa kỳ (15%). v Thi cuối kỳ (60%). v Chuyên cần và tham gia xây dựng bài
giảng (10%).
9 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Quy định chung
v Tuân thủ nghiêm túc các nội quy và
quy định của Khoa và Trường.
v Không được vắng quá 3 buổi trên tổng
số các buổi học lý thuyết.
v Không gian lận trong quá trình làm
bài tập và trong thi cử.
v Nộp bài tập đúng thời hạn quy định § Trừ 15% bài tập cho mỗi ngày nộp trễ. § Nộp trễ trên 4 ngày => 0 điểm.
10 Đặc tả hình thức
Quy định của môn học
v Tắt điện thoại hoặc để điện thoại ở
chế độ im lặng.
v Không sử dụng điện thoại trong giờ
học.
v Không sử dụng máy tính bảng, máy tính xách tay và các thiết bị điện tử khác trong giờ học.
v Không ăn vặt trong lớp.
11 Đặc tả hình thức
