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

TRƯỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN KHOA CÔNG NGHỆ THÔNG TIN BỘ MÔN CÔNG NGHỆ PHẦN MỀM LÊ TRẦN HOÀNG NGUYÊN – 0112103 NGUYỄN BÁCH KHOA - 0112140 TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# KHÓA LUẬN CỬ NHÂN TIN HỌC GIÁO VIÊN HƯỚNG DẪN Th.s: NGUYỄN ĐÔNG HÀ NIÊN KHÓA 2001 – 2005 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 2 LỜI CẢM ƠN Đầu tiên, xin chân thành cảm ơn cô Nguyễn Đông Hà đã trực tiếp hướng 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 nghệ Design By Contract hữu ích này. 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 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 nghiên cứu đề tài này. 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ề 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 Nguyễn Lương Ngọc Minh và Nguyễn Ngọc Khánh. 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 này được hoàn thành. Thành phố Hồ Chí Minh, Tháng 7, 2005. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 3 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 114 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 6 BẢNG CÁC HÌNH VẼ Hình 1-1: Giao diện EiffelStudio ---------------------------------------------------------- 11 Hình 1-2: Thông báo khi lỗi xảy ra ở tiền điều kiện ------------------------------------ 14 Hình 1-3: Code gây ra lỗi ở tiền điều kiện ----------------------------------------------- 14 Hình 1-4: Thông báo khi lỗi xảy ra ở hậu điều kiện ------------------------------------ 15 Hình 1-5: Code gây ra lỗi ở hậu điều kiện ----------------------------------------------- 15 Hình 1-6: Thông báo khi lỗi xảy ra ở điều kiện bất biến ------------------------------- 16 Hình 1-7: Code gây ra lỗi ở điều kiện bất biến ------------------------------------------ 16 Hình 7-1: Sử dụng bộ lọc các module ---------------------------------------------------- 34 Hình 8-1: Stack được cài đặt bằng mảng ------------------------------------------------- 35 Hình 9-1: Thời gian tồn tại của một đối tượng ------------------------------------------ 50 Hình 10-1: Thời gian tồn tại của một đối tượng----------------------------------------- 58 Hình 11-1: Sự biến đổi giữa những đối tượng trừu tượng và cụ thể------------------ 65 Hình 11-2: Hai cài đặt của cùng một đối tượng trừu tượng---------------------------- 67 Hình 13-1: Một vòng lặp tính toán -------------------------------------------------------- 73 Hình 16-1: Sơ đồ thiết kế tổng thể -------------------------------------------------------- 94 Hình 16-2: Màn hình Configuration ------------------------------------------------------ 95 Hình 16-3: Chi tiết màn hình Configuration --------------------------------------------- 96 Hình 16-4: Lớp Connect -------------------------------------------------------------------- 98 Hình 16-5: Lớp ProjectInfo ---------------------------------------------------------------- 99 Hình 16-6: Lớp ClassInfo -----------------------------------------------------------------101 Hình 16-7: Lớp FunctionInfo -------------------------------------------------------------104 Hình 16-8: Lớp Assertion -----------------------------------------------------------------106 Hình 16-9: Lớp Extra ----------------------------------------------------------------------109 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 7 LỜI NÓI ĐẦU Trong ngành công nghệ thông tin, thay đổi là một tất yếu diễn ra hết sức thường xuyên mà ta phải chấp nhận và cố gắng điều chỉnh nó. Phần mềm này ra đời thay thế phần mềm khác là một điều vô cùng bình thường, dễ hiểu. Tại sao lại như thế? Bởi vì người sử dụng luôn mong muốn có được một phần mềm hữu ích. Tuy nhiên, dù phần mềm có thể đáp ứng những nhu cầu của người sử dụng trong thời gian hiện tại thì cũng không thể đảm bảo nó sẽ luôn được ưa chuộng. Để có thể tồn tại lâu dài, phần mềm phải thật sự chất lượng. Điều này đồng nghĩa với việc nó phải không ngừng được cập nhật. Mà ta cũng biết, phần mềm càng đúng đắn, đáng tin cậy và rõ ràng bao nhiêu thì công việc nâng cấp và phát triển nó càng dễ dàng bấy nhiêu. Do đó, có thể nói, một trong những tiêu chí của ngành công nghệ phần mềm mà bất kỳ thời đại nào, bất kỳ sản phẩm phần mềm nào cũng đều hướng đến là tính đáng tin cậy và đúng đắn. Xuất phát từ nhu cầu ấy, công nghệ Design By Contract đã ra đời nhằm giúp đảm bảo cho tính đáng tin cậy của phần mềm. Đó cũng chính là lý do mà chúng em đã chọn đề tài này. Với mục đích tìm hiểu công nghệ Design By Contract một cách khá kỹ lưỡng, chúng em đã tiếp cận nó bằng các tài liệu lý thuyết cũng như qua các công cụ có khả năng hỗ trợ Design By Contract cho các ngôn ngữ lập trình hiện đại. Không dừng ở đó, chúng em còn xây dựng một công cụ hỗ trợ công nghệ này cho C# với tên gọi là DCS (Design By Contract for C Sharp). Đối tượng và phạm vi nghiên cứu: ý tưởng chính của Design By Contract là lập một “hợp đồng” giữa một lớp đối tượng (supplier) và những khách hàng (client) của nó, tức là những lớp đối tượng khác gọi đến các phương thức của lớp này. Những client này phải bảo đảm một số điều kiện nhất định khi gọi một phương thức của một supplier gọi là tiền điều kiện (precondition); đáp lại, sau khi thực thi thủ tục, supplier phải đáp ứng một số điều kiện tương ứng gọi là hậu điều kiện (postcondition). Những điều kiện của hợp đồng sẽ được kiểm tra bởi trình biên dịch, và bất cứ sự vi phạm nào của phần mềm cũng sẽ được phát hiện. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 8 TỔNG QUAN Các hướng nghiên cứu đã có của một số tác giả: - Bertrand Meyer, tác giả của công nghệ Design By Contract và ngôn ngữ Eiffel, ngôn ngữ hỗ trợ hoàn toàn Design By Contract. Vấn đề tồn tại: Bởi vì đây là ngôn ngữ lập trình do chính tác giả của Design By Contract tạo ra nên hỗ trợ rất đầy đủ và rõ ràng cho công nghệ này, nhưng vấn đề ở đây là ngôn ngữ Eiffel còn xa lạ với người lập trình dù đã ra đời gần 10 năm, được ít người sử dụng ngôn ngữ này để phát triển phần mềm. - ResolveCorp và eXtensible C# (XC#), một Add-In hỗ trợ Design By Contract cho C#. Đây là một công cụ rất tốt, hỗ trợ đầy đủ Design By Contract cho C#. Tuy nhiên, công cụ này chỉ được sử dụng miễn phí một vài DLL và source code không mở. - Man Machine Systems và JMSAssert, công cụ hỗ trợ Design By Contract cho Java. Đây cũng là một công cụ tốt. Tuy nhiên, JMSAssert chỉ hỗ trợ biên dịch command line và sử dụng cho JDK từ 1.2 trở xuống, không thể tích hợp vào các môi trường hỗ trợ lập trình Java như JBuilder, Sun One Studio hay Eclipse. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 9 Chương 1: Giới thiệu về Eiffel 1.1. Giới thiệu Đầu tiên, chúng ta sẽ làm quen với phần mềm Eiffel trước khi tìm hiểu về công nghệ Design By Contract. Vì sao lại như vậy? Vì tất cả ví dụ dùng trong luận văn đều sử dụng cấu trúc của ngôn ngữ Eiffel. Còn những khái niệm nào mới được đề cập trong chương này sẽ được giải thích kỹ hơn trong các phần sau khi giới thiệu về Design By Contract Qua hơn 10 năm tồn tại, Eiffel hiện nay được coi là một trong những môi trường phát triển phần mềm tốt nhất. Trước sức mạnh to lớn của Eiffel trong lĩnh vực phần mềm thì dù muốn dù không, bạn cũng nên biết qua về nó. Vậy thực chất Eiffel là gì? Eiffel là khung làm việc trợ giúp cho việc suy nghĩ, thiết kế và thực thi phần mềm hướng đối tượng. Eiffel là một phương pháp, một ngôn ngữ hỗ trợ mô tả một cách hiệu quả và phát triển những hệ thống có chất lượng. Eiffel là ngôn ngữ thiết kế Vai trò của Eiffel còn hơn một ngôn ngữ lập trình. Những gì nó đem lại không chỉ giới hạn trong ngữ cảnh lập trình mà trải rộng khắp công việc phát triển phần mềm: phân tích, lên mô hình, viết đặc tả, thiết kế kiến trúc, thực hiện, bảo trì, làm tài liệu. Eiffel là một phương pháp. Eiffel dẫn đường các nhà phân tích và những nhà phát triển xuyên suốt tiến trình xây dựng một phần mềm. Phương pháp Eiffel tập trung cả về yếu tố sản phẩm và chất lượng, với những điểm nhấn: tính đáng tin cậy, tính tái sử dụng, tính mở rộng, tính khả dụng, tính bền vững. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 10 1.2. Design By Contract trong Eiffel Eiffel hỗ trợ rất nhiều tính năng: tiếp cận hướng đối tượng hoàn thiện, khả năng giao tiếp bên ngoài (có thể giao tiếp với các ngôn ngữ C, C++, Java,…), hỗ trợ vòng đời phần mềm bao gồm việc phân tích, thiết kế, thực thi và bảo trì, hỗ trợ Design By Contract, viết xác nhận, quản lý ngoại lệ… Design By Contract hầu như là vấn đề luôn được nhắc đến khi đề cập về Eiffel. Trong Eiffel, mỗi thành phần của hệ thống đều có thể được thực hiện theo một đặc tả tiên quyết về các thuộc tính trừu tượng của nó, liên quan đến những thao tác nội tại và những giao tác của nó với các thành phần khác. Eiffel thực thi một cách trực tiếp ý tưởng Design By Contract, một phương pháp làm nâng cao tính đáng tin cậy của phần mềm, cung cấp một nền tảng cho việc đặc tả, làm tài liệu và kiểm nghiệm phần mềm, cũng như việc quản lý các ngoại lệ và cách sử dụng kế thừa thích hợp. 1.3. EiffelStudio EiffelStudio là trình biên dịch của Eiffel. Ngoài ra, nó còn là một IDE rất mạnh với những tính năng độc nhất như: công cụ công nghệ đảo tích hợp, bộ máy phân tích mã nguồn định lượng. Tùy vào nhu cầu của mình, bạn có thể sử dụng EiffelStudio như một môi trường lập trình hoặc chỉ như một công cụ giúp mô hình hóa, xây dựng các mô tả hệ thống bao gồm các lớp trừu tượng mà không thực thi bằng công cụ Diagram hoặc kết hợp cả 2 khả năng để đạt đến hiệu quả cao nhất. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 11 1.3.1. Giao diện Hình 1-1: Giao diện EiffelStudio Giao diện làm việc của EiffelStudio có 4 khung chính: Features, Class, Clusters, Context. Để thuận tiện cho việc lập trình, các bạn có thể đóng bớt các khung cửa sổ đi. Tất cả các khung cửa sổ này đều có thể đóng lại ngọai trừ Class. 1.3.2. Các thao tác căn bản trên EiffelStudio Khởi động chương trình: Programs --> EiffelStudio Version --> EiffelStudio Chọn "Create a new project" > OK. Class view là khung làm việc chính của bạn. Sau khi lập trình xong, bạn có thể biên dịch và cho chạy chương trình bằng công cụ Compile (F7). Debug chương trình: F10, F11. Lưu project: File > Save. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 12 Biểu diễn Design By Contract trong Eiffel: Precondition: require boolean expressions Postcondition: ensure boolean expressions Class invariant: invariant boolean expressions Chỉ thị Check: check assertion_clause1 assertion_clause2 … assertion_clausen end Loop invariant, loop variant: from initialization until exit invariant inv variant Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 13 var loop body end Demo: Project stack STACK_CLASS: lớp stack chính, chứa các định nghĩa các thao tác trên stack. make: Hàm khởi tạo của stack. item: hàm lấy phần tử trên cùng stack. get(t): hàm lấy phần tử thứ t empty: kiểm tra stack có rỗng. full: kiểm tra stack có đầy put(x): thêm phần tử x vào stack remove: bỏ phần tử trên cùng stack TEST_CLASS: lớp chính(main), lớp gọi các hàm của lớp STACK_CLASS. Ta sẽ thử vài trường hợp cho thấy khả năng bắt lỗi của Eiffel. Lưu ý: Sau mỗi trường hợp hãy sửa lại code như ban đầu rồi mới thử tiếp trường hợp khác. Mở tập tin test_class.e. Chạy thử chương trình (F5). Chương trình khởi tạo stack gồm 8 phần tử từ 0 đến 7 và xuất stack. Stack được xuất ra màn hình. TH1: Lỗi xảy ra ở tiền điều kiện Sửa n:=8 thành n:=-8. Tại dòng if (n >= 0) then nhấn tổ hợp phím Ctrl-K. Tại dòng end --end if , nhấn tổ hợp phím Ctrl-K. Recompile (Shift-F7) và cho chạy lại chương trình (F5). Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 14 Xuất hiện thông báo ngoại lệ sau: Hình 1-2: Thông báo khi lỗi xảy ra ở tiền điều kiện và con trỏ dừng lại ở câu lệnh Hình 1-3: Code gây ra lỗi ở tiền điều kiện Nguyên nhân: Khi bạn gọi thủ tục a.make(n), do trước đó khởi tạo n là một số âm (=-8), client không đảm bảo contract, nên trong thủ tục make của lớp STACK_CLASS, thủ tục make kiểm tra không thỏa tiền điều kiện positive_capacity: n>=0, nó dừng lại và thông báo cho người lập trình biết. TH2: Lỗi xảy ra ở hậu điều kiện Trong lớp TEST_CLASS, tại thủ tục make, sửa như sau: Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 15 Capacity := n capacity := n-1 Recompile (Shift-F7) và cho chạy lại chương trình (F5). Xuất hiện thông báo ngoại lệ sau: Hình 1-4: Thông báo khi lỗi xảy ra ở hậu điều kiện và con trỏ dừng lại ở câu lệnh Hình 1-5: Code gây ra lỗi ở hậu điều kiện Nguyên nhân: Trước đó, ta gán capacity := n-1, hậu điều kiện lại yêu cầu capacity = n. TH3: Lỗi xảy ra ở điều kiện bất biến. Trong lớp TEST_CLASS, tại thủ tục make, thêm vào dòng sau: count:=-1 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 16 Chọn menu Project > Project Setting… Bỏ dấu check ở ensure. Đánh dấu check ở invariant. Hành động này nhằm bỏ qua chế độ kiểm lỗi ở hậu điều kiện. Ở đây chỉ muốn minh họa cho việc phát hiện lỗi ở điều kiện bất biến. Recompile (Shift-F7) và cho chạy lại chương trình (F5). Xuất hiện thông báo ngoại lệ sau: Hình 1-6: Thông báo khi lỗi xảy ra ở điều kiện bất biến và con trỏ dừng lại ở câu lệnh Hình 1-7: Code gây ra lỗi ở điều kiện bất biến Nguyên nhân: Trước đó, ta gán count := -1, điều kiện bất biến yêu cầu count>=0. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 17 Chương 2: Một số cơ chế mang lại tính đáng tin cậy cho phần mềm Trước hết, phải nói rằng kỹ thuật định nghĩa thuộc tính của một đối tượng gần như là có liên quan với cấu trúc của những hệ thống phần mềm. Những kiến trúc đơn giản, riêng biệt và có khả năng mở rộng sẽ giúp chúng ta đảm bảo tính đáng tin cậy của phần mềm dễ dàng hơn so với những cấu trúc vặn vẹo. Đặc biệt, cố gắng giới hạn sự liên quan giữa các môđun với nhau đến mức tối thiểu nhất sẽ là tiêu điểm cho việc thảo luận về tính riêng biệt. Điều này giúp ngăn chặn những rủi ro thông thường của tính đáng tin cậy, ví dụ như những biến toàn cục và việc định nghĩa những cơ chế liên lạc bị giới hạn, client và những mối quan hệ kế thừa. Nói đến chất lượng phần mềm thì không thể bỏ qua tính đáng tin cậy. Chúng ta cố gắng giữ cho những cấu trúc càng đơn giản càng tốt. Tuy rằng điều này vẫn chưa đủ đảm bảo cho tính đáng tin cậy của phần mềm, nhưng dù sao, nó cũng là một điều kiện cần thiết. Một điều kiện khác cũng cần thiết nữa là làm cho phần mềm của chúng ta tối ưu và dễ đọc. Văn bản phần mềm không những được viết một lần mà nó còn phải được đọc đi đọc lại và viết đi viết lại nhiều lần. Sự trong sáng và tính đơn giản của các câu chú thích là những yêu cầu cơ bản để nâng cao tính đáng tin cậy của phần mềm. Một vũ khí khác cũng rất cần thiết là việc quản lý bộ nhớ một cách tự động, đặc biệt là bộ thu gom rác (garbage collection). Bất kỳ hệ thống nào có khởi tạo và thao tác với cấu trúc dữ liệu động mà lại thực hiện thu hồi bộ nhớ bằng tay (tức là do người lập trình điều khiển) hoặc bộ nhớ không hề được thu hồi thì thật là nguy hiểm. Bộ thu gom rác không hề là một sự xa xỉ mà nó là thành phần thiết yếu để mở rộng tính đáng tin cậy cho bất kỳ một môi trường hướng đối tượng nào. Một kỹ thuật khác nữa mà cũng có thể là thiết yếu mà có liên quan đến genericity là static typing. Nếu không có những luật như thế thì chúng ta sẽ không kiểm soát được những lỗi xảy ra lúc run-time do quá trình gõ code gây nên. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 18 Tóm lại, tất cả những kỹ thuật này cung cấp một nền tảng cần thiết để ta có cái nhìn gần hơn về một hệ thống phần mềm đúng đắn và bền vững. Chương 3: Tính đúng đắn của phần mềm Giả sử có một người đưa cho bạn một chương trình C với 300 000 dòng lệnh và hỏi rằng nó có đúng không. Tôi nghĩ rằng rất có khả năng bạn thấy khó và thậm chí là không thể trả lời được. Tuy nhiên, nếu là một cố vấn viên, bạn hãy trả lời “Không” và sau đó tính một giá thật cao vì rất có thể bạn đúng. Thật sự, để có thể trả lời câu hỏi trên một cách đúng nghĩa, bạn không những cần phải lấy chương trình đó mà còn phải