Bài giảng Đặc tả hình thức - Chương mở đầu: Giới thiệu môn học - Vũ Thanh Nguyên

1Đặc tả hình thức Trường Đại học Công Nghệ Thông Tin, ĐHQG-HCM Khoa Công Nghệ Phần Mềm Giảng viên: PGS.TS. Vũ Thanh Nguyên 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 2Giới thiệu chung Mục tiêu môn học:  Cung cấp các kiến thức liên quan đến hướng tiếp cận xây dựng phần mềm dùng đặc tả hình thức.  Đặc tả hình thức là các kỹ thuật dựa trên nền tảng của toán học được áp dụng và hỗ trợ để xây dựng các hệ thống và phần mềm.  Môn học cung cấp cho sinh viên n giai đoạn triển khai.  Môn học bao gồm các chương liên quan đến các thành phần cơ sở trong đặc tả hình thức nói chung (Tâp họp, Hàm, Dãy,...), và cụ thể hơn trong các chương về đặc tả với VDM và Z.  Môn học giúp ích cho sinh viên hiểu và nắm bắt các phương pháp hình thức để có thể đặc tả và thực hiện thiết kế. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 3Giới thiệu chung  Số đơn vị học trình  4 đơn vị học trình (4 TC lý thuyết) Môn tiên quyết:  Nhập môn công nghệ phần mềm Môn học trước:  Tin học đại cương, cấu trúc dữ liệu và giải thuật, lập trình hướng đối tượng 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 4Tài liệu tham khảo về ngôn ngữ VDM Introduction to VDM M. Woodman & B. Heal McGraw-Hill, 1993. Software Development using VDM C. B. Jones Prentice-Hall, 1989. Ebook: ftp://ftp.cs.man.ac.uk/pub/ Practical Formal Methods with VDM D. Andrews & D. Ince McGraw-Hill, 1991. Case Studies in Systematic Software Development ISBN: 0131160885, C. B. Jones & R. C. F. Shaw, eds, Prentice-Hall, 1990. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 5Tài liệu tham khảo về ngôn ngữ VDM Using Z – Specification, Refinement, and Proof Jim Woodcook, Jim Davies University of Oxford Prentice Hall, 1996 ISBN 0-13-948472-8 Formal Specification and Documentation using Z: A Case Study Approach Prof. Jonathan Bowen Centre for Applied Formal Methods, London South Bank University International Thomson Computer Press (ITCP) Thomson Publishing ISBN 1-85032-230-9 An Introduction To Formal Specification With A and VDM Pro. D.Ince The Open University McGRAW HILL, 2004 ISBN 0-07-707907-8 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 6Tài liệu tham khảo về ngôn ngữ VDM The Construction Of Formal Specification. An Introduction to the Model- based and Algebraic Approaches Pro. D.Ince The Open University McGRAW HILL, 2004 ISBN 0-07-707735-0 Giáo trình lý thuyết đặc tả hình thức. Prof. Vu Thanh Nguyen Ms. Hầu Nguyễn Thành Nam Nhà xuất bản ĐHQG Tp.HCM, 2014 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 7Nội dung  Ch1. Giới thiệu về Đặc tả hình thức  Ch2. Cơ sở Toán học trong VDM  Ch3. Mô hình hóa dữ liệu, kiểu tập hợp  Ch4. Dữ liệu kiểu mảng, chuỗi  Ch5. Đặc tả hàm  Ch6. Kiểu đối tượng phức  Ch7. Kiểu ánh xạ  Ch8. Giới thiệu sơ lược về Z 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 8Nội dung #1 Chương 1. Giới thiệu về Đặc tả hình thức  Đặc tả hình thức và quy trình CNPM.  Giới thiệu về đặc tả hình thức  Một số khái niệm liên quan  Ngôn ngữ và đặc tả.  Ngôn ngữ  Ngôn ngữ hình thức  Một số ngôn ngữ đặc tả hình thức  Đặc tả và công nghệ phần mềm 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 9Nội dung #2 Chương 2. Cơ sở Toán học trong VDM  Lý thuyết tập hợp.  Định nghĩa, tính chất, kích thước  Tập hợp dạng tường minh  Phép hội, phép giao, phép hiệu, tích Descartes, số lượng phần tử, tập lũy thừa.  Một số tập hợp được định nghĩa sẵn  Xác định tập hợp thông qua tính chất  Mối quan hệ giũa tập và vị từ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 10 Nội dung #2 Chương 2. Cơ sở Toán học trong VDM  Logic mệnh đề và phép toán vị từ.  Logic mệnh đề  Mệnh đề và liên từ  Mệnh đề và vị từ  Các phép nối  Dạng mệnh đề  quy luật logic  Lượng tử  Luật suy diễn  Liên từ , , , , True và False 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 11 Nội dung #3 Chương 3. Giới thiệu về mô hình hóa kiểu tập hợp  Kiểu dữ liệu trong VDM.  Các tập hợp định nghĩa sẵn  Kiểu tập hợp  Mô hình hóa các phép toán  Đặc tả phép toán 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 12 Nội dung #4 Chương 4. Giới thiệu về kiểu số và kiểu mảng  Kiểu Số.  Các phép toán trên số  Miền xác định của số  Cardinality  Kiểu Mảng  Kiểu chuỗi  Các hàm và thao tác trên mảng/chuỗi  Sơ đồ các phép toán trên mảng 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 13 Nội dung #5 Chương 5. Tổng quan về đặc tả hàm  Tổng quan về hàm.  Một số khái niệm và định nghĩa  Các phép toán tổng quát trên ngôn ngữ VDM  Đặc tả hàm không tường minh  Định nghĩa  Các ưu điểm  Đặc tả hàm tường minh  Định nghĩa  Mối quan hệ giũa hàm tường minh và không tường minh 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 14 Nội dung #5 Chương 5. Tổng quan về đặc tả hàm  Cấu trúc điều khiển if-then-else  Cấu trúc Case  Sử dụng hàm phụ  Đặc tả đệ quy  Khai báo biến tạm bằng let-in 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 15 Nội dung #6 Chương 6. Kiểu đối tượng phức  Định nghĩa kiểu đối tượng phức  Cú pháp  Khởi tạo đối tượng phức  Hàm mk-TênKiểuĐốiTượngPhức  Ràng buột trên kiểu dữ liệu  Cập nhật đối tượng phức 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 16 Nội dung #7 Chương 7. Kiểu ánh xạ  Ánh xạ  Đơn ánh  Toàn ánh  Song ánh  Định nghĩa  Các hàm và thao tác trên ánh xạ  Đặc tả sử dụng ánh xạ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 17 Nội dung #8 Chương 8. Giới thiệu về ngôn ngữ Z  Tổng quan về đặc tả hình thức sử dụng ngôn ngữ Z  Những khái niệm cơ bản của ngôn ngữ Z Một số tài liệu về ngôn ngữ Z 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 18 Hình Thức Kiểm Tra Đánh Giá  Thi lý thuyết cuối kỳ: 70% điểm  Thi viết, không tham khảo tài liệu  Kiểm tra lên lớp, bài tập 30% điểm  Kiểm tra lên lớp 15% điểm  Bài tập 15% điểm  Điểm cộng  Đề tài tìm hiểu nâng cao, seminar  Ghi chú  Điểm Tổng kết môn học (tối đa là 10 điểm) được làm tròn lên đến 0.5. 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt