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
2
Giớ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.
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.

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
Toán rời rạc
3
Tài liệu tham khảo
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
Tài liệu tham khảo
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
5
Tài liệu tham khảo
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


6
Nộ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. Đặc tả các thao tác
Ch8. Kiểu ánh xạ
Ch9. Tính đúng đắn của phát biểu và luật chứng minh
Ch10. Giới thiệu sơ lược về Z