CHƯƠNG I: MỞ ĐẦU.. 1

I.1 GIỚI THIỆU CHUNG.. 2

I.1.1 Mục tiêu của môn học:2

I.2 MỘT SỐ KHÁI NIỆM CƠ BẢN:2

I.2.1 Các phương pháp hình thức (formal methods):2

I.2.2 Đặc tả (specification):2

I.2.3 Đặc tả hình thức (formal specification):3

I.3 LỊCH SỬ RA ĐỜI VÀ PHÁT TRIỂN CỦA ĐẶC TẢ HÌNH THỨC:4

I.4 ĐẶC TẢ VÀ QUY TRÌNH CÔNG NGHỆ PHẦN MỀM... 5

I.4.1 Quy trình chung:5

I.4.1.1 Phân tích. 5

I.4.1.2 Thiết kế. 6

I.4.1.3 Kiểm chứng. 6

I.4.2 Ứng dụng của đặc tả. 6

I.4.3 Đặc tả với ngôn ngữ toán học. 6

Chuong II.1 Logic mệnh đề :2

II.1.1 Mệnh đề :2

II.1.2 Các phép toán trên mệnh đề:2

II.1.2.1 Phép phủ định :2

II.1.2.2 Phép nối liền (phép VÀ) :2

II.1.2.3 Phép nối rời ( phép HOẶC) :3

II.1.2.4 Phép kéo theo :3

II.1.2.5 Phép kéo theo 2 chiều :3

II.1.3 Dạng mệnh đề. 4

II.1.4 Tương đương logic:4

II.1.5 Hệ quả logic:5

II.1.6 Các nguyên tắc thay thế:5

II.1.7 Các quy luật logic:5

II.1.8 Các quy tắc suy diễn :8

II.2 LOGIC VỊ TỪ.. 9

II.2.1 Vị từ:9

II.2.2 Lượng từ:9

II.3 LÝ THUYẾT TẬP HỢP. 10

II.4 BÀI TẬP CUỐI CHƯƠNG   11

Chuong III.1 ĐẶC TẢ KIỂU DỮ LIỆU.. 2

III.2 ĐẶC TẢ HÀM... 3

III.2.1 Cú pháp chung khi đặc tả hàm (dùng ngôn ngữ toán học) :3

III.2.2 Ví dụ 1:3

III.2.3 Ví dụ 2. 4

III.3 ĐẶC TẢ ĐỆ QUY.. 5

III.4 CÁC QUY TẮC TÍNH TOÁN.. 6

III.5 CÁC SƠ ĐỒ TRẠNG THÁI. 7

III.6 CÁC ĐỐI TƯỢNG HÌNH HỌC.. 8

III.7 CÁC RÀNG BUỘC.. 10

III.7.1 Ràng buộc trên kiểu dữ liệu. 10

III.7.2 Ràng buộc trên sơ đồ logic. 12

III.8 BÀI TẬP ÁP DỤNG.. 14

CHƯƠNG IV: ĐẶC TẢ VÀ TÍNH ĐÚNG ĐẮN CỦA HÀM... 1

IV.1 CÁC PHƯƠNG PHÁP KIỂM TRA TÍNH ĐÚNG ĐẮN.. 2

IV.1.1 Đặt vấn đề. 2

IV.1.2 Kiểm tra động. 2

IV.1.3 Kiểm tra tĩnh. 3

IV.2 CHỨNG MINH VỚI CÁC LUẬT SUY DIỄN.. 3

IV.2.1 Mở đầu. 3

IV.2.2 Các luật suy diễn. 4

IV.2.2.1 Các luật suy diễn trên phép phủ định (Ø)4

IV.2.2.2 Các luật suy diễn trên phép hội (Ú)4

IV.2.2.3 Các luật suy diễn trên phép tuyển (Ù)5

IV.2.2.4 Các luật suy diễn trên phép kéo theo (Þ)6

IV.2.3 Chứng minh luật suy diễn. 6

IV.2.3.1 Dạng thức :6

IV.2.3.2 Ví dụ. 6

IV.3 BÀI TẬP ÁP DỤNG   7

Chuong 5

V.1 Giới thiệu. 2

V.2 Các thành phần của ngôn ngữ. 2

V.2.1 Logic toán học. 2

V.2.1.1 Logic mệnh đề. 2

V.2.1.2 Logic vị từ. 2

V.2.2 Lý thuyết tập hợp. 4

V.2.3 Hàm và quan hệ. 5

V.2.3.1 Quan hệ 2 ngôi5

V.2.3.2 Miền xác định và miền giá trị5

V.2.3.3 Hàm.. 5

V.2.3.4 Hàm riêng phần. 5

V.2.3.5 Hàm toàn phần. 5

V.3 Giản đồ (schemas)6

V.3.1 Giới thiệu chung. 6

V.3.2 Định nghĩa. 6

V.3.3 Toán tử đặt tên. 7

V.3.4 Giản đồ tương đương. 7

V.3.5 Một số ghi chú. 7

V.3.6 Giản đồ được sử dụng như 1 kiểu dữ liệu. 8

V.3.7 Giản đồ được sử dụng trong các khai báo. 9

V.3.8 Giản đồ được sử dụng trong các biểu thức lượng từ. 10

V.3.9 Giản đồ được sử dụng như 1 vị từ. 10

V.3.10 Dạng chuẩn của 1 giản đồ. 10

V.3.11 Đặt lại tên các thành phần trong giản đồ. 11

V.4 Các phép toán trên giản đồ. 12

V.4.1 Phép nối liền (Conjunction)12

V.4.2 Phép đổi tên (Decoration)13

V.4.3 Phép nối rời (Disjunction)14

V.4.4 Phép phủ định (Negation)14

V.4.5 Phép lượng từ hóa. 15

V.5 Bài tập áp dụng. 15