Luận văn tốt nghiệp: Tìm hiểu công nghệ Design by Contact và xây dựng công cụ hỗ trợ cho C#

TRƯỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN<br /> KHOA CÔNG NGHỆ THÔNG TIN<br /> BỘ MÔN CÔNG NGHỆ PHẦN MỀM<br /> <br /> LÊ TRẦN HOÀNG NGUYÊN – 0112103<br /> NGUYỄN BÁCH KHOA - 0112140<br /> <br /> TÌM HIỂU CÔNG NGHỆ<br /> DESIGN BY CONTRACT VÀ XÂY DỰNG<br /> CÔNG CỤ HỖ TRỢ CHO C#<br /> KHÓA LUẬN CỬ NHÂN TIN HỌC<br /> <br /> GIÁO VIÊN HƯỚNG DẪN<br /> Th.s: NGUYỄN ĐÔNG HÀ<br /> <br /> NIÊN KHÓA 2001 – 2005<br /> <br /> Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#<br /> <br /> LỜI CẢM ƠN<br /> Đầu tiên, xin chân thành cảm ơn cô Nguyễn Đông Hà đã trực tiếp hướng<br /> dẫn cũng như cung cấp tài liệu để chúng em có thể tiếp cận và tìm hiểu về công<br /> nghệ Design By Contract hữu ích này.<br /> Bên cạnh đó, xin đồng gửi lời cảm ơn đến các thầy cô của bộ môn Công<br /> nghệ Phần mềm Nâng cao đã tạo điều kiện cho chúng em dành nhiều thời gian<br /> nghiên cứu đề tài này.<br /> Cuối cùng, quả là một điều thiếu sót nếu không kể đến sự ủng hộ to lớn về<br /> mặt tinh thần cũng như sự giúp đỡ tận tình của gia đình, bạn bè, đặc biệt là bạn<br /> Nguyễn Lương Ngọc Minh và Nguyễn Ngọc Khánh.<br /> Xin chân thành cảm ơn tất cả, những người đã góp phần giúp cho luận văn<br /> này được hoàn thành.<br /> Thành phố Hồ Chí Minh,<br /> Tháng 7, 2005.<br /> <br /> 2<br /> <br /> Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#<br /> <br /> MỤC LỤC<br /> LỜI NÓI ĐẦU<br /> <br /> 7<br /> <br /> TỔNG QUAN<br /> <br /> 8<br /> <br /> Chương 1: Giới thiệu về Eiffel<br /> <br /> 9<br /> <br /> 1.1.<br /> <br /> Giới thiệu<br /> <br /> 9<br /> <br /> 1.2.<br /> <br /> Design By Contract trong Eiffel<br /> <br /> 10<br /> <br /> 1.3.<br /> <br /> EiffelStudio<br /> <br /> 10<br /> <br /> 1.3.1. Giao diện<br /> <br /> 11<br /> <br /> 1.3.2. Các thao tác căn bản trên EiffelStudio<br /> <br /> 11<br /> <br /> Chương 2: Một số cơ chế mang lại tính đáng tin cậy cho phần mềm<br /> <br /> 17<br /> <br /> Chương 3: Tính đúng đắn của phần mềm<br /> <br /> 18<br /> <br /> Chương 4: Biểu diễn một đặc tả<br /> <br /> 20<br /> <br /> 4.1.<br /> <br /> Những công thức của tính đúng đắn<br /> <br /> 20<br /> <br /> 4.2.<br /> <br /> Những điều kiện yếu và mạnh<br /> <br /> 22<br /> <br /> Chương 5: Giới thiệu về sự xác nhận trong văn bản của phần mềm<br /> <br /> 24<br /> <br /> Chương 6: Tiền điều kiện và hậu điều kiện<br /> <br /> 25<br /> <br /> 6.1.<br /> <br /> Lớp ngăn xếp<br /> <br /> 25<br /> <br /> 6.2.<br /> <br /> Tiền điều kiện<br /> <br /> 28<br /> <br /> 6.3.<br /> <br /> Hậu điều kiện<br /> <br /> 28<br /> <br /> Chương 7: Giao ước cho tính đáng tin cậy của phần mềm<br /> 7.1.<br /> <br /> 7.2.<br /> hơn<br /> 7.3.<br /> <br /> 29<br /> <br /> Quyền lợi và nghĩa vụ<br /> <br /> 29<br /> <br /> 7.1.1. Những quyền lợi<br /> <br /> 30<br /> <br /> 7.1.2. Những nghĩa vụ<br /> <br /> 30<br /> <br /> Nghệ thuật của sự tin cậy phần mềm: kiểm tra ít hơn, bảo đảm nhiều<br /> 31<br /> Những xác nhận không phải là một cơ chế kiểm tra đầu vào<br /> <br /> 3<br /> <br /> 33<br /> <br /> Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#<br /> <br /> Chương 8: Làm việc với những xác nhận<br /> <br /> 35<br /> <br /> 8.1.<br /> <br /> Lớp stack<br /> <br /> 35<br /> <br /> 8.2.<br /> <br /> Mệnh lệnh và yêu cầu<br /> <br /> 38<br /> <br /> 8.3.<br /> <br /> Lưu ý về những cấu trúc rỗng<br /> <br /> 41<br /> <br /> 8.4.<br /> <br /> Thiết kế tiền điều kiện: tolerant hay demanding?<br /> <br /> 42<br /> <br /> 8.5.<br /> <br /> Một môđun tolerant<br /> <br /> 43<br /> <br /> Chương 9: Những điều kiện bất biến của lớp<br /> <br /> 47<br /> <br /> 9.1.<br /> <br /> Định nghĩa và ví dụ<br /> <br /> 48<br /> <br /> 9.2.<br /> <br /> Định dạng và các thuộc tính của điều kiện bất biến của lớp<br /> <br /> 49<br /> <br /> 9.3.<br /> <br /> Điều kiện bất biến thay đổi<br /> <br /> 51<br /> <br /> 9.4.<br /> <br /> Ai phải bảo quản điều kiện bất biến?<br /> <br /> 52<br /> <br /> 9.5.<br /> <br /> 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<br /> <br /> phần mềm<br /> 9.6.<br /> <br /> 53<br /> Những điều kiện bất biến và hợp đồng<br /> <br /> Chương 10: Khi nào một lớp là đúng?<br /> <br /> 54<br /> <br /> 56<br /> <br /> 10.1.<br /> <br /> Tính đúng đắn của một lớp<br /> <br /> 57<br /> <br /> 10.2.<br /> <br /> Vai trò của những thủ tục khởi tạo<br /> <br /> 60<br /> <br /> 10.3.<br /> <br /> Xem lại về mảng<br /> <br /> 60<br /> <br /> Chương 11: Kết nối với kiểu dữ liệu trừu tượng<br /> <br /> 62<br /> <br /> 11.1.<br /> <br /> So sánh đặc tính của lớp với những hàm ADT<br /> <br /> 63<br /> <br /> 11.2.<br /> <br /> Biểu diễn những tiên đề<br /> <br /> 64<br /> <br /> 11.3.<br /> <br /> Hàm trừu tượng<br /> <br /> 65<br /> <br /> 11.4.<br /> <br /> Cài đặt những điều kiện bất biến<br /> <br /> 66<br /> <br /> Chương 12: Một chỉ thị xác nhận<br /> <br /> 68<br /> <br /> Chương 13: Vòng lặp có điều kiện bất biến và điều kiện biến đổi<br /> <br /> 71<br /> <br /> 13.1.<br /> <br /> Vấn đề vòng lặp<br /> <br /> 71<br /> <br /> 13.2.<br /> <br /> Những vòng lặp đúng<br /> <br /> 71<br /> <br /> 13.3.<br /> <br /> Những thành phần của một vòng lặp đúng<br /> <br /> 72<br /> <br /> 13.4.<br /> <br /> Cú pháp của vòng lặp<br /> <br /> 74<br /> <br /> 4<br /> <br /> Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#<br /> <br /> Chương 14: Sử dụng những xác nhận<br /> <br /> 77<br /> <br /> 14.1.<br /> <br /> Những xác nhận như một công cụ để viết phần mềm chính xác<br /> <br /> 14.2.<br /> <br /> 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<br /> <br /> đối tượng<br /> <br /> 77<br /> <br /> 78<br /> <br /> Chương 15: Giới thiệu công cụ XC#<br /> <br /> 81<br /> <br /> 15.1.<br /> <br /> Giới thiệu<br /> <br /> 81<br /> <br /> 15.2.<br /> <br /> XC# hoạt động như thế nào<br /> <br /> 82<br /> <br /> 15.3.<br /> <br /> Khai báo các xác nhận<br /> <br /> 82<br /> <br /> 15.4.<br /> <br /> 15.3.1. Tiền điều kiện<br /> <br /> 82<br /> <br /> 15.3.2. Hậu điều kiện<br /> <br /> 83<br /> <br /> 15.3.3. Một số thuộc tính mà XC# qui ước sẵn<br /> <br /> 83<br /> <br /> Ví dụ lớp Stack<br /> <br /> 86<br /> <br /> Chương 16: Kết quả thực nghiệm: công cụ DCS<br /> <br /> 88<br /> <br /> 16.1.<br /> <br /> Nguyên lý làm việc<br /> <br /> 88<br /> <br /> 16.2.<br /> <br /> Thiết kế<br /> <br /> 94<br /> <br /> 16.2.1. Tổng thể<br /> <br /> 94<br /> <br /> 16.2.2. Chi tiết các lớp đối tượng<br /> <br /> 95<br /> <br /> 16.2.2.1 Màn hình Configuration<br /> <br /> 95<br /> <br /> 16.2.2.2 Lớp Connect<br /> <br /> 98<br /> <br /> 16.2.2.3 Lớp ProjectInfo<br /> <br /> 99<br /> <br /> 16.2.2.4 Lớp ClassInfo<br /> <br /> 101<br /> <br /> 16.2.2.5 Lớp FunctionInfo<br /> <br /> 104<br /> <br /> 16.2.2.6 Lớp Assertion<br /> <br /> 106<br /> <br /> 16.2.2.7 Lớp Extra<br /> <br /> 109<br /> <br /> KẾT LUẬN<br /> <br /> 111<br /> <br /> HƯỚNG PHÁT TRIỂN<br /> <br /> 112<br /> <br /> TÀI LIỆU THAM KHẢO<br /> <br /> 113<br /> <br /> Ý KIẾN CỦA GIÁO VIÊN PHẢN BIỆN<br /> <br /> 114<br /> <br /> 5<br /> <br />