MỤC LỤC

LỜI NÓI ĐẦU 7

TỔNG QUAN 8

Chương 1: Giới thiệu về Eiffel 9

1.1. Giới thiệu 9

1.2. Design By Contract trong Eiffel 10

1.3. EiffelStudio 10

1.3.1. Giao diện 11

1.3.2. Các thao tác căn bản trên EiffelStudio 11

Chương 2: Một số cơ chế mang lại tính đáng tin cậy cho phần mềm 17

Chương 3: Tính đúng đắn của phần mềm 18

Chương 4: Biểu diễn một đặc tả 20

4.1. Những công thức của tính đúng đắn 20

4.2. Những điều kiện yếu và mạnh 22

Chương 5: Giới thiệu về sự xác nhận trong văn bản của phần mềm 24

Chương 6: Tiền điều kiện và hậu điều kiện 25

6.1. Lớp ngăn xếp 25

6.2. Tiền điều kiện 28

6.3. Hậu điều kiện 28

Chương 7: Giao ước cho tính đáng tin cậy của phần mềm 29

7.1. Quyền lợi và nghĩa vụ 29

7.1.1. Những quyền lợi 30

7.1.2. Những nghĩa vụ 30

7.2. Nghệ thuật của sự tin cậy phần mềm: kiểm tra ít hơn, bảo đảm nhiều

hơn 31

7.3. Những xác nhận không phải là một cơ chế kiểm tra đầu vào 33

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#

4

Chương 8: Làm việc với những xác nhận 35

8.1. Lớp stack 35

8.2. Mệnh lệnh và yêu cầu 38

8.3. Lưu ý về những cấu trúc rỗng 41

8.4. Thiết kế tiền điều kiện: tolerant hay demanding? 42

8.5. Một môđun tolerant 43

Chương 9: Những điều kiện bất biến của lớp 47

9.1. Định nghĩa và ví dụ 48

9.2. Định dạng và các thuộc tính của điều kiện bất biến của lớp 49

9.3. Điều kiện bất biến thay đổi 51

9.4. Ai phải bảo quản điều kiện bất biến? 52

9.5. Vai trò của những điều kiện bất biến của lớp trong kỹ thuật xây dựng

phần mềm 53

9.6. Những điều kiện bất biến và hợp đồng 54

Chương 10: Khi nào một lớp là đúng? 56

10.1. Tính đúng đắn của một lớp 57

10.2. Vai trò của những thủ tục khởi tạo 60

10.3. Xem lại về mảng 60

Chương 11: Kết nối với kiểu dữ liệu trừu tượng 62

11.1. So sánh đặc tính của lớp với những hàm ADT 63

11.2. Biểu diễn những tiên đề 64

11.3. Hàm trừu tượng 65

11.4. Cài đặt những điều kiện bất biến 66

Chương 12: Một chỉ thị xác nhận 68

Chương 13: Vòng lặp có điều kiện bất biến và điều kiện biến đổi 71

13.1. Vấn đề vòng lặp 71

13.2. Những vòng lặp đúng 71

13.3. Những thành phần của một vòng lặp đúng 72

13.4. Cú pháp của vòng lặp 74

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#

5

Chương 14: Sử dụng những xác nhận 77

14.1. Những xác nhận như một công cụ để viết phần mềm chính xác 77

14.2. Sử dụng những xác nhận cho việc viết tài liệu: thể rút gọn của một lớp

đối tượng 78

Chương 15: Giới thiệu công cụ XC# 81

15.1. Giới thiệu 81

15.2. XC# hoạt động như thế nào 82

15.3. Khai báo các xác nhận 82

15.3.1. Tiền điều kiện 82

15.3.2. Hậu điều kiện 83

15.3.3. Một số thuộc tính mà XC# qui ước sẵn 83

15.4. Ví dụ lớp Stack 86

Chương 16: Kết quả thực nghiệm: công cụ DCS 88

16.1. Nguyên lý làm việc 88

16.2. Thiết kế 94

16.2.1. Tổng thể 94

16.2.2. Chi tiết các lớp đối tượng 95

16.2.2.1 Màn hình Configuration 95

16.2.2.2 Lớp Connect 98

16.2.2.3 Lớp ProjectInfo 99

16.2.2.4 Lớp ClassInfo 101

16.2.2.5 Lớp FunctionInfo 104

16.2.2.6 Lớp Assertion 106

16.2.2.7 Lớp Extra 109

KẾT LUẬN 111

HƯỚNG PHÁT TRIỂN 112

TÀI LIỆU THAM KHẢO 113

Ý KIẾN CỦA GIÁO VIÊN PHẢN BIỆN 11