Khóa luận Tìm hiểu công nghệ design by contract và xây dựng công cụ hỗ trợ cho C#

ư 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 lấy cả lời diễn giải về những gì mà chương trình đó làm được hay ta gọi chúng là những đặc tả của chương trình. Có những chú thích giống nhau cũng chẳng sao, dĩ nhiên, khi đó ta không để ý đến kích thước của chương trình. Ví dụ, câu lệnh x := y+1 không đúng cũng không sai. Vì đúng hay sai chỉ có ý nghĩa khi xét trong quan hệ của nó với một lời chú dẫn, tức là cái mà người ta mong đợi có được sau khi thực hiện câu lệnh hay ít ra thì cũng là sự ảnh hưởng đến trạng thái của các biến trong chương trình. Do đó, câu lệnh trên sẽ đúng với đặc tả: “Điều này đảm bảo cho x và y có giá trị khác nhau” nhưng nó sẽ sai với đặc tả: “Điều này đảm bảo rằng x có giá trị âm” (giả sử các thực thể có kiểu số nguyên. Như vậy, x có thể có kết quả không âm sau khi gán. Điều đó tùy thuộc vào giá trị của y). Ví dụ này nhằm minh họa cho khái niệm “tính đúng đắn” được trình bày bên dưới: Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 19 Tính đúng đắn của phần mềm Tính đúng đắn là một khái niệm quan hệ Một hệ thống phần mềm hay một thành phần phần mềm thì không đúng cũng không sai. Nó chỉ đúng hay sai khi có liên quan với một đặc tả nào đó. Nói một cách chính xác, ta không thảo luận những thành phần phần mềm có đúng hay không, mà là thảo luận chúng có phù hợp với những đặc tả của chúng hay không. Do đó, thuật ngữ “tính đúng đắn” không được dùng cho những thành phần phần mềm, mà nó được dùng cho từng cặp, mỗi cặp bao gồm một thành phần phần mềm và một đặc tả. Trong phần này, ta sẽ biết cách biểu diễn những đặc tả thông qua một xác nhận (assertion) để giúp ta xác nhận tính đúng đắn của phần mềm. Điều này cho thấy kết quả của việc viết những đặc tả là một bước đầu tiên quan trọng để đảm bảo rằng phần mềm thật sự đúng. Việc viết những xác nhận cùng lúc hoặc đúng ra là trước khi viết phần mềm sẽ mang lại những lợi ích tuyệt vời như sau: − Sản xuất được phần mềm đúng với khi bắt đầu vì nó được thiết kế đúng. Ích lợi này đã được Harlan D.Mills (một trong những người khởi đầu đề xướng việc lập trình có cấu trúc “Structured Programming”) trình bày vào năm 1970 trong quyển sách “How to write correct programs and know it” (có nghĩa là “Làm thế nào để viết được những chương trình đúng và biết được nó đúng”). “Biết” ở đây có nghĩa là trang bị cho phần mềm những đối số khi ta viết nó nhằm hiển thị tính đúng đắn của nó. − Có được sự hiểu biết tốt hơn về vấn đề và những cách giải quyết cuối cùng của nó. − Việc thực hiện các tài liệu cho phần mềm dễ dàng. Chúng ta sẽ thấy được ở phần sau rằng những xác nhận sẽ đóng một vai trò trung tâm trong việc hướng đối tượng đến gần tài liệu. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 20 − Cung cấp một căn bản cho việc kiểm tra và debug hệ thống. Trong những phần còn lại chúng ta sẽ tìm hiểu những ứng dụng này. Trong C, C++ và một số ngôn ngữ khác (dưới sự chỉ đạo của Algol W), ta có thể viết một câu lệnh đóng vai trò một xác nhận để kiểm tra một tình trạng nào đó có được giữ ở một trạng thái nào đó như mong muốn hay không khi thực thi phần mềm, và chương trình sẽ không được thực thi nếu nó không thoả. Mặc dù như thế cũng có thể làm được những gì mà ta muốn, nhưng việc làm vậy chỉ tượng trưng cho một phần nhỏ của việc sử dụng những lời xác nhận trong phương pháp hướng đối tượng. Do đó, nếu giống như nhiều người phát triển phần mềm khác thì bạn sẽ quen với những câu lệnh như thế nhưng lại không thấy được bức tranh toàn cảnh. Hầu hết tất cả những khái niệm được bàn ở đây đều sẽ mới lạ với bạn. Chương 4: Biểu diễn một đặc tả Chúng ta có thể trở lại nhận xét trước với hình ảnh một ký hiệu toán học đơn giản được mượn từ lý thuyết của việc kiểm tra một chương trình hình thức và những lý do quý giá để lập luận về tính đúng đắn của các thành phần phần mềm. 4.1. Những công thức của tính đúng đắn Giả sử A thực hiện một vài thao tác (ví dụ A là một câu lệnh hay thân của một thủ tục). Một công thức của tính đúng đắn là một cách biểu diễn theo dạng sau: {P} A {Q} Ý nghĩa của công thức tính đúng đắn {P} A {Q} Bất kỳ thi hành nào của A, bắt đầu ở trạng thái P thì sẽ kết thúc với trạng thái Q Những công thức của tính đúng đắn (còn được gọi là bộ ba Hoare) là một ký hiệu toán học, không phải là một khái niệm lập trình; chúng không phải là một trong Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 21 số những ngôn ngữ phần mềm mà chỉ được thiết kế nhằm giúp cho việc thể hiện những thuộc tính của các thành phần phần mềm. Trong {P} A {Q}, A biểu thị cho một thao tác, P và Q là những thuộc tính của những thực thể khác nhau có liên quan hay còn được gọi là những xác nhận (chúng ta sẽ định nghĩa từ “xác nhận” (“assertion”) một cách chính xác hơn ở phần sau). Trong hai xác nhận này, P được gọi là tiền điều kiện (precondition) và Q được gọi là hậu điều kiện (postcondition). Ví dụ, ta có một công thức bình thường của tính đúng đắn như sau với giả sử rằng x là một số nguyên: {x>=9} x := x+5 {x>=13} Công thức tính đúng đắn được sử dụng để đánh giá tính đúng đắn của phần mềm. Điều đó cũng có nghĩa là tính đúng đắn chỉ được xét đến khi nó gắn với một đặc tả nào đó. Như vậy, khi thảo luận về tính đúng đắn của phần mềm, ta không nói đến những thành phần phần mềm riêng lẻ A, mà nó là bộ ba bao gồm một thành phần phần mềm A, một tiền điều kiện P và một hậu điều kiện Q. Mục đích duy nhất của việc này là thiết lập kết quả cho những công thức tính đúng đắn {P} A {Q}. Trong ví dụ trên, con số 13 ở hậu điều kiện không phải là lỗi do in ấn hay gõ phím! Giả sử thực hiện đúng phép tính trên số nguyên ở công thức trên: với điều kiện x>=9 là đúng trước câu lệnh, x>=13 sẽ đúng sau khi thực hiện câu lệnh. Tuy nhiên, ta thấy được nhiều điều thú vị hơn: − Với một tiền điều kiện như vậy, hậu điều kiện hay nhất phải là điều kiện mạnh nhất, và trong trường hợp này là x>=14. − Còn với hậu điều kiện đã đưa ra thì tiền điều kiện hay nhất phải là tiền điều kiện yếu nhất, ở đây là x>=8. Từ một công thức đã cho, ta luôn có thể có được một công thức khác bằng cách mở rộng tiền điều kiện hay nới lỏng đi hậu điều kiện. Bây giờ, ta sẽ cùng nhau xem xét nhiều hơn về những khái niệm “mạnh hơn” và “yếu hơn” là thế nào. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 22 4.2. Những điều kiện yếu và mạnh Một cách để xem xét đặc tả theo dạng {P} A {Q} là xem nó như một mô tả các công việc cho A. Điều này cũng giống như có một mục quảng cáo tuyển người trên báo đăng rằng “Cần tuyển một người có khả năng thực hiện công việc A khi A có trạng thái bắt đầu là P, và sau khi A được hoàn tất thì nó phải thỏa mãn Q”. Giả sử, một người bạn của bạn đang kiếm việc và tình cờ đọc được những quảng cáo tương tự như thế này, tất cả lương và lợi ích của chúng đều như nhau, chỉ có điều là chúng khác nhau ở những cái P và Q. Cũng giống như nhiều người, bạn của bạn thì lười nhác, có thể nói rằng, anh ta muốn có một công việc dễ nhất. Và anh ta hỏi ý kiến bạn là nên chọn công việc nào. Trong trường hợp này, bạn sẽ khuyên anh ấy thế nào? Trước hết, với P: bạn khuyên anh ta nên chọn một công việc với tiền điều kiện yếu hay mạnh? Câu hỏi tương tự cho hậu điều kiện Q. Bạn hãy suy nghĩ và chọn cho mình một quyết định trước khi xem câu trả lời ở phần dưới. Trước hết, ta nói về tiền điều kiện. Từ quan điểm của người làm công tương lai, tức là người sẽ thực hiện công việc A, tiền điều kiện P định nghĩa những trường hợp mà ta sẽ phải thực hiện công việc. Do đó, một P mạnh là tốt, vì P càng mạnh thì các trường hợp bạn phải thực hiện A càng được giới hạn. Như vậy, P càng mạnh thì càng dễ cho người làm công. Và tuyệt vời nhất là khi kẻ làm công chẳng phải làm gì cả tức là hắn ta là kẻ ăn không ngồi rồi. Điều này xảy ra khi công việc A được định nghĩa bởi: Công thức 1 {False} A {} Trong trường hợp này, hậu điều kiện không cần thiết phải đề cập bởi dù nó có là gì thì cũng không có ảnh hưởng. Nếu có bao giờ bạn thấy một mục tuyển người như vậy thì đừng mất công đọc hậu điều kiện mà hãy chớp lấy công việc đó Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 23 ngay lập tức. Tiền điều kiện False là sự xác nhận mạnh nhất có thể vì nó không bao giờ thỏa mãn một trạng thái nào cả. Bất cứ yêu cầu nào để thực thi A cũng sẽ không đúng, và lỗi không nằm ở trách nhiệm của A mà là ở người yêu cầu hay khách hàng (client) bởi nó đã không xem xét bất cứ tiền điều kiện nào cần đến. Dù cho A có làm hay không làm gì đi nữa thì nó cũng luôn đúng với đặc tả. Còn với hậu điều kiện Q, tình trạng bị đảo ngược. Một hậu điều kiện mạnh là một tin xấu: nó chỉ ra rằng bạn phải mang lại nhiều kết quả hơn. Q càng yếu, càng tốt cho người làm thuê. Thực tế, công việc ăn không ngồi rồi tốt nhì trên thế giới là công việc được định nghĩa mà không chú ý đến tiền điều kiện: Công thức 2 {} A {True} Hậu điều kiện True là một xác nhận yếu nhất vì nó thỏa mãn mọi trường hợp. Khái niệm “mạnh hơn” hay “yếu hơn” được định nghĩa một cách hình thức từ logic: P1 được gọi là mạnh hơn P2, và P2 yếu hơn P1 nếu P1 bao hàm P2 và chúng không bằng nhau. Khi mọi lời xác nhận bao hàm True, và False bao hàm mọi xác nhận thì thật là hợp lý để nói rằng True như là yếu nhất và False như là mạnh nhất với tất cả xác nhận có thể. Đến đây, có một câu hỏi được đặt ra: “Tại sao công thức 2 là công việc tốt nhì trên thế giới?” Câu trả lời chính là một điểm tinh tế trong phần định nghĩa ý nghĩa của công thức {P}A{Q}: sự kết thúc. Định nghĩa nói rằng sự thực thi phải kết thúc trong tình trạng thoả Q miễn là khi bắt đầu nó thoả P. Với công thức 1, không có trường hợp nào thoả P. Do đó, A là gì cũng không thành vấn đề, ngay cả nó là một đoạn code mà khi thi hành, chương trình sẽ bị rơi vào một vòng lặp không điểm dừng hay là sẽ gây hỏng máy cũng chẳng sao. Vì dù A là gì thì cũng đúng với đặc tả của nó. Tuy nhiên, với công thức 2, vấn đề là ở trạng thái kết thúc, nó không cần thoả mãn bất kỳ thuộc tính đặc biệt nào nhưng trạng thái kết thúc phải được đảm bảo là có tồn tại. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 24 Những đọc giả mà đã quen với lý thuyết khoa học máy tính hay những kỹ thuật chứng minh lập trình sẽ thấy rằng công thức {P} A {Q} dùng ở đây ám chỉ toàn bộ tính đúng đắn, bao gồm cả sự kết thúc ... nếu không được thì gán giá trị cho error. -- Không có tiền điều kiện! do if empty then error := Underflow else check representation /= Void end representation.remove error := 0 end Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 47 ensure error_code_if_impossible: (old empty) = (error = Underflow) no_error_if_possible: (not old empty) = (error = 0) not_full_if_no_error: (error = 0) implies not full one_fewer_item_if_no_error: (error = 0) implies count = old count – 1 end feature {NONE} – Cài đặt representation: STACK2 [G] -- Cài đặt của stack (không được bảo vệ) capacity: INTEGER -- Số phần tử tối đa của stack end -- class STACK3 Ví dụ trên đã cho ta thấy sự nặng nề của một lớp dùng cách tiếp cận tolerant. Đây là một minh chứng cho thấy tolerant sẽ dẫn đến một phần mềm phức tạp và không cần thiết. Ngược lại, với demanding, theo tinh thần của Design By Contract, sẽ giúp những client trong phát hiện lỗi trong tất cả các trường hợp theo cách tốt nhất. Chương 9: Những điều kiện bất biến của lớp Tiền điều kiện và hậu điều kiện mô tả những thuộc tính của những thủ tục riêng biệt. Điều này cũng cần thiết cho việc biểu diễn những thuộc tính toàn cục của những thể hiện (instance) của một lớp vì chúng phải được lưu giữ trong tất cả thủ tục. Những thuộc tính như thế sẽ tạo nên điều kiện bất biến của lớp (class invariant). Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 48 Chúng giữ những thuộc tính ngữ nghĩa sâu hơn và mô tả những ràng buộc toàn vẹn của một lớp. 9.1. Định nghĩa và ví dụ Xem lại phần cài đặt ngăn xếp (stack) bằng cách sử dụng mảng mà không có sự bảo đảm (STACK2) class STACK2 [G] creation make feature make, empty, full, item, put, remove capacity: INTEGER count: INTEGER feature {NONE} –- Cài đặt representation: ARRAY [G] end Những thuộc tính của lớp bao gồm: representation kiểu mảng, capacity và count kiểu số nguyên tạo nên một stack tượng trưng. Mặc dù những tiền điều kiện và hậu điều kiện của thủ tục được đưa ra trước đây có thể biểu diễn một vài thuộc tính ngữ nghĩa của stack nhưng chúng thất bại trong việc biểu diễn tính nhất quán khi các thuộc tính liên kết với nhau. Ví dụ, count luôn luôn có giá trị từ 0 đến capacity: 0 <= count; count <= capacity (điều này cũng hàm ý rằng capacity >= 0), và capacity là kích thước của mảng: capacity = representation.capacity Một điều kiện bất biến của lớp (class invariant) cũng như là một xác nhận, biểu diễn những ràng buộc nhất quán chung được dùng cho mọi thể hiện của lớp. Nó khác với tiền điều kiện và hậu điều kiện là những cái chỉ mô tả cho những thủ tục riêng biệt. Sự xác nhận ở trên chỉ liên quan đến những thuộc tính. Những điều kiện bất biến cũng có thể biểu diễn mối quan hệ ngữ nghĩa giữa những hàm với nhau hay Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 49 giữa những hàm với những thuộc tính. Ví dụ, điều kiện bất biến của STACK2 có thể mô tả sự liên quan giữa thuộc tính empty và count như sau: empty = (count = 0) Trong ví dụ này, xác nhận về điều kiện bất biến liên quan đến một thuộc tính và một hàm. Nó không riêng là việc lặp lại xác nhận ở hậu điều kiện của hàm (empty). Một xác nhận sẽ trở nên hữu ích hơn nếu nó có liên quan đến nhiều thuộc tính như ví dụ trên hoặc nhiều hơn một hàm. Tiếp theo, ta có một ví dụ tiêu biểu khác. Liên quan đến khái niệm tài khoản ngân hàng, ta giả sử có một lớp là BANK_ACCOUNT có các đặc tính như deposits_list, withdrawals_list và balance. Lúc đó, điều kiện bất biến của lớp này có thể là một mệnh đề như sau: consistent_balance: deposits_list.total – withdrawals_list.total = balance Hàm total cho biết giá trị tích lũy của danh sách những hoạt động (số tiền gửi hay số tiền rút). Ví dụ trên cho thấy tình trạng nhất quán giữa những giá trị có thể truy cập thông qua các thuộc tính deposits_list, withdrawals_list và balance. 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 Về mặt cú pháp, một điều kiện bất biến của lớp là một xác nhận, nằm trong phần invariant, sau phần feature và trước end. class STACK4[G] creation As in STACK2 ... feature ... As in STACK2 ... invariant count_non_negative: 0 <= count count_bounded: count <= capacity Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 50 consistent_with_array_size: capacity = representation.capacity empty_if_no_elements: empty = (count = 0) item_at_top: (count > 0) implies (representation item (count) = item) end Một điều kiện bất biến của lớp C là một bộ những xác nhận mà mỗi thể hiện của C sẽ thoả mãn tất cả những thời điểm bền vững (stable times). Những thời điểm bền vững là những thời điểm mà tại đây, thể hiện của lớp trong tình trạng có thể quan sát được: + Khi khởi tạo thể hiện, tức là sau khi thực thi !!a hoặc là !!a.make(), a có kiểu là lớp C. + Trước và sau mỗi khi yêu cầu một thủ tục r của lớp thông qua lời gọi a.r(). Hình vẽ sau sẽ chỉ ra thời gian tồn tại của một đối tượng Hình 9-1: Thời gian tồn tại của một đối tượng Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 51 Vào lúc bắt đầu, tức là bên trái hình Hình 8-1, đối tượng không tồn tại. Đối tượng được sinh ra bởi câu lệnh !!a hay !!a.make() hoặc là do một clone. Sau đó, client sử dụng đối tượng thông qua các tham chiếu đến a có dạng a.f() với f là một tính năng của lớp sinh ra đối tượng. Và từ đó, đối tượng tồn tại ít nhất là cho đến khi việc thi hành kết thúc. Điều kiện bất biến là một thuộc tính đặc thù của những trạng thái được biểu diễn bởi những ô vuông màu xám trong hình Hình 8-1 (Ví dụ: S1). Những thời điểm bền vững (stable times) trong hình trên là những chỗ mà đối tượng có thể thấy được từ bên ngoài, nghĩa là client có thể áp dụng một tính năng nào đó cho nó, bao gồm: + Trạng thái kết quả của việc tạo một đối tượng (trong hình là S1). + Những trạng thái ngay trước và sau khi client thực hiện một lời gọi có dạng a.some_routine(). 9.3. Điều kiện bất biến thay đổi Tuy có tên là điều kiện bất biến nhưng nó cũng không cần phải thoả mãn hết tại mọi thời điểm mặc dù trong ví dụ STACK4, nó vẫn đúng sau khi được khởi tạo. Trong những trường hợp tổng quát hơn, việc một thủ tục g vào lúc ban đầu vì cố thực hiện những mục đích của mình - tức là cố đạt được hậu điều kiện – mà có thể làm hủy đi điều kiện bất biến trong quá trình này (cũng như con người, việc cố gắng làm một cái gì đó hữu ích có thể phá vỡ trật tự đã được thiết lập của mọi thứ); nhưng sau đó, ở giai đoạn thực thi tiếp theo, thủ tục này không vi phạm quá nhiều điều kiện bất biến vốn có là hoàn toàn được chấp nhận. Trong vài tình trạng tức thời, ví dụ như trong những tình trạng được đánh dấu trên hình Hình 8-1, điều kiện bất biến sẽ không thể giữ được. Tuy nhiên, điều này vẫn có thể chấp nhận được miễn là thủ tục sẽ thiết lập lại điều kiện bất biến trước khi kết thúc việc thực thi của nó. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 52 9.4. Ai phải bảo quản điều kiện bất biến? Những lời gọi đủ điều kiện, có dạng là a.f(), thực hiện nhân danh cho một client, là những cái duy nhất luôn phải được bắt đầu và rời khỏi trong trạng thái thoả mãn điều kiện bất biến; không có quy định nào cho những lời gọi không đủ điều kiện có dạng f() thực thi trực tiếp bởi những client nhưng chỉ phục vụ như những công cụ hỗ trợ cho việc tiến hành những cái cần thiết của một lời gọi đủ điều kiện. Do đó, việc bắt buộc duy trì điều kiện bất biến chỉ được áp dụng cho những tính năng được xuất khẩu (export) ra ngoài hoặc là theo cách chung chung hoặc là có sự lựa chọn; một tính năng bí mật mà không client nào được sử dụng là tính năng mà không bị điều kiện bất biến nào ảnh hưởng. Sau đây là quy định định nghĩa chính xác khi nào một xác nhận được coi là một điều kiện bất biến đúng của một lớp: Quy định của điều kiện bất biến Một xác nhận I sẽ là một điều kiện bất biến đúng của một lớp C nếu và chỉ nếu nó thoả 2 điều kiện: + E1: Mọi thủ tục khởi tạo của C , khi được áp dụng cho những đối số thoả mãn tiền điều kiện của nó trong trạng thái những thuộc tính có giá trị mặc định, đều sẽ dẫn đến trạng thái thoả mãn I. + E2: Mọi thủ tục được export ra khỏi lớp, khi được áp dụng cho những đối số và một trạng thái thoả mãn cả I lẫn tiền điều kiện của thủ tục, đều sẽ dẫn đến trạng thái thoả mãn I. Chú ý, trong luật này: + Mọi lớp được coi như có một thủ tục khởi tạo, và được định nghĩa là null nếu nó không được chỉ định tường minh. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 53 + Trạng thái của một đối tượng được định nghĩa bởi tất cả những trường của nó (tức là những giá trị của các thuộc tính của lớp ứng với một thể hiện cụ thể). + Tiền điều kiện của thủ tục có thể liên quan đến trạng thái đầu tiên và những đối số. + Hậu điều kiện có thể liên quan đến trạng thái cuối, trạng thái đầu (thông qua khái niệm old) và trong trường hợp là hàm thì giá trị trả về (nếu có) được định nghĩa trước bởi thực thể Result. + Điều kiện bất biến có thể chỉ liên quan đến trạng thái. Những xác nhận có thể là những hàm nhưng những hàm như vậy là một tham chiếu gián tiếp đến các thuộc tính tức các trạng thái. Ta có thể dùng quy định về điều kiện bất biến như một cơ sở để trả lời câu hỏi: “Sẽ có ý nghĩa gì nếu điều kiện bất biến gây xâm phạm trong tiến trình thực thi của hệ thống?” Trước đây, chúng ta đã thấy rằng những dấu hiệu xâm phạm của một tiền điều kiện là một lỗi (một “bug”) ở khách hàng, còn xâm phạm ở hậu điều kiện là do lỗi ở người cung cấp. Thật ra, những điều kiện bất biến cũng là những hậu điều kiện. Chính thuộc tính này giúp ta biết được những gì sẽ nhận được. 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 Thuộc tính E2 chỉ ra rằng chúng ta có thể xem điều kiện bất biến là phần được thêm vào một cách không tường minh cho cả tiền và hậu điều kiện của mỗi thủ tục được export ra ngoài. Do đó, về nguyên tắc, khái niệm điều kiện bất biến là không cần thiết vì không có nó ta vẫn làm việc tốt hoặc là chỉ việc mở rộng tiền và hậu điều kiện của tất cả thủ tục trong lớp là được. Tuy nhiên, không phải vậy. Dù việc có thêm điều kiện bất biến làm phức tạp những văn bản thủ tục, nhưng quan trọng hơn, ý nghĩa sâu xa của điều kiện bất biến là nó vượt khỏi những thủ tục riêng và được áp dụng cho cả một lớp. Thật sự, điều kiện bất biến không chỉ dùng để phục vụ cho những thủ tục viết trong lớp mà còn có thể sử dụng được khi ta có nhu cầu thêm mới sau đó. Vì vậy, điều kiện bất biến có Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 54 thể kiểm soát được cả những phần mở rộng của lớp. Điều này sẽ được thể hiện rõ trong những quy định về việc kế thừa. Trong phát triển phần mềm, sự thay đổi là một điều tất yếu mà chúng ta phải chấp nhận, chỉ là ta phải cố gắng điều chỉnh nó. Một vài lĩnh vực của hệ thống phần mềm như những thành phần riêng biệt, những lớp có thể thay đổi nhanh hơn những cái khác. Đặc biệt, việc thêm vào, bớt đi hay thay đổi những đặc tính là một hiện tượng thường xuyên và bình thường. Trong quá trình dễ thay đổi này, việc cứ bám mãi vào những thuộc tính mặc dù nó có thể thay đổi sẽ gây khó khăn cho việc đảm bảo toàn bộ hệ thống được duy trì vĩnh viễn. Nhưng với điều kiện bất biến, nó không gây khó khăn cho ta khi muốn thay đổi vì chúng giữ những ràng buộc ngữ nghĩa cơ bản được áp dụng cho một lớp. Ví dụ STACK2 đã minh họa được những ý kiến cơ bản, nhưng để đánh giá được toàn bộ những ích lợi của điều kiện bất biến thì ta phải theo dõi thêm những ví dụ tiếp theo. Khái niệm về điều kiện bất biến là một trong số những khái niệm nổi trội nhất mà ta học được từ phương pháp hướng đối tượng. Chỉ khi nào ta kế thừa những điều kiện bất biến (của một lớp do chính mình viết) hay đọc và hiểu nó (từ một lớp của người khác) thì ta mới có thể thực sự cảm nhận được lớp đó là gì. 9.6. Những điều kiện bất biến và hợp đồng Những điều kiện bất biến sẽ được hiểu rõ hơn khi đưa nó vào ngữ cảnh hợp đồng. Những hợp đồng giữa người với nhau thường liên quan đến những quy tắc chung được áp dụng cho mọi khế ước của một mục nào đó; ví dụ như những quy định về việc phân chia vùng của thành phố được áp dụng cho tất cả hợp đồng xây dựng nhà. Những điều kiện bất biến cũng đóng vai trò như thế trong hợp đồng phần mềm: điều kiện bất biến của một lớp ảnh hưởng đến tất cả hợp đồng giữa một thủ tục của một lớp và một đối tượng sử dụng lớp đó. Trong phần trên, ta xem những điều kiện bất biến như một cái gì đó được thêm vào cho tiền và hậu điều kiện của mọi thủ tục được export ra ngoài. Coi body là phần thân của thủ tục (là tập hợp những câu lệnh trong phần do), pre là tiền điều Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 55 kiện, post là hậu điều kiện và INV là điều kiện bất biến của lớp. Khi ấy, yêu cầu về tính đúng đắn trong thủ tục có thể được biểu diễn thông qua những khái niệm đã được giới thiệu trước đây là: {INV and pre} body {INV and post} (Câu lệnh trên có nghĩa là: bất cứ sự thi hành nào trong phần body, bắt đầu với bất kỳ trạng thái nào của INV và pre thì sẽ kết thúc trong trạng thái thoả mãn INV và post) Như vậy, có một câu hỏi dành cho người cung cấp tức người đã viết phần body: điều kiện bất biến là những tin tốt hay xấu, nó làm cho công việc dễ hơn hay khó hơn? Để trả lời được điều này thì bạn phải hiểu được ý nghĩa của cuộc thảo luận đầu tiên về ý nghĩa của tiền và hậu điều kiện đối với người làm công và người làm chủ. Thực chất, điều kiện bất biến cũng vậy. Nó có thể là tin tốt mà cũng có thể là tin xấu. Đối với người xin việc lười biếng, họ muốn có một tiền điều kiện mạnh và một hậu điều kiện yếu. Ở đây, thêm INV vào làm cho tiền và hậu điều kiện mạnh hơn hoặc ít nhất cũng là bằng với ban đầu. Cái này xuất phát từ quy tắc logic: a và b luôn luôn hàm ý a, điều này có thể nói là nó mạnh hơn hay bằng a. Vì vậy, nếu bạn chịu trách nhiệm thực hiện phần body, thì điều kiện bất biến sẽ: + Làm cho công việc của bạn dễ hơn nếu thêm vào tiền điều kiện pre vì trạng thái đầu tiên còn phải thỏa mãn thêm INV. Như vậy, sẽ giới hạn hơn những trường hợp có thể gặp phải. + Làm cho công việc của bạn khó hơn nếu thêm vào hậu điều kiện chính thức post vì bạn phải bảo đảm trạng thái cuối còn phải thoả mãn thêm INV. Những ý kiến này là đáng tin với cách nhìn điều kiện bất biến là một tình trạng nhất quán chung được dùng cho lớp như một tổng thể. Do đó, nó cũng được dùng cho tất cả các thủ tục của lớp. Khi là tác giả của một thủ tục như thế, bạn sẽ thấy có lợi khi điều kiện này đúng vào lúc bắt đầu thủ tục, nhưng bạn phải bảo đảm Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 56 rằng thủ tục sẽ thoả mãn điều kiện này một lần nữa lúc kết thúc để thủ tục tiếp theo thực thi trên cùng một đối tượng lại thấy việc này là có lợi lần nữa. Trong lớp BANK_ACCOUNT ở trên, mệnh đề điều kiện bất biến: deposits_list.total – withdrawals_list.total = balance là một ví dụ tốt. Nếu bạn phải thêm một thủ tục vào lớp, mệnh đề này đảm bảo những đặc tính deposits_list, withdrawals_list và balance có những giá trị nhất quán. Vì vậy, bạn không cần kiểm tra thuộc tính này (và như thế, sau khi xem, chúng ta cũng không phải kiểm tra nó). Nhưng nó cũng có nghĩa là bạn phải viết thủ tục, để mà, với bất cứ cái gì khác nó làm, nó cũng sẽ rời khỏi đối tượng trong trạng thái thỏa mãn thuộc tính này lần nữa . Do thế, thủ tục withdraw dùng để ghi một thao tác rút tiền sẽ không chỉ cập nhật withdrawals_list mà nó cũng phải cập nhật giá trị của balance nếu balance là một thuộc tính để lấy số tiền gửi vào tài khoản và khôi phục lại điều kiện bất biến, bảo đảm bất kỳ thủ tục nào khác được gọi sau đó của cùng một đối tượng cũng sẽ có thể thi hành dễ dàng. Không chỉ là một thuộc tính mà balance còn có thể là một hàm mà trong đó nó sẽ tính toán và trả về giá trị của: deposits_list.total – withdrawals_list.total Trong trường hợp này, thủ tục withdraw không cần làm bất cứ gì đặc biệt để có thể duy trì điều kiện bất biến. Khả năng chuyển đổi giữa hai khả năng này mà không làm ảnh hưởng đến khách hàng là một minh họa của nguyên tắc truy cập đồng bộ (uniform access). Ví dụ này chỉ ra rằng những điều kiện bất biến của lớp như một phương tiện vận chuyển đối với phần mềm một cách lịch thiệp cũng như nếu bạn sử dụng một loại tài nguyên chia sẻ thì bạn phải đưa nó lại cho người khác sau mỗi lần sử dụng. Chương 10: Khi nào một lớp là đúng? Phần này giúp chúng ta tiếp cận với những lý thuyết cơ bản. Ngay cả là đọc lần đầu tiên thì bạn cũng có thể tiếp cận được với những ý tưởng sẽ được trình bày Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 57 sắp tới vì nó tập trung vào những điểm chính yếu và rất quý báu khi sử dụng phương pháp kế thừa. 10.1. Tính đúng đắn của một lớp Với những tiền điều kiện, hậu điều kiện và điều kiện bất biến, ta có thể định nghĩa một cách chính xác một lớp đúng đắn là thế nào. Thật ra, cơ sở để định nghĩa tính đúng đắn của một lớp đã được trình bày ngay từ đầu luận văn: một lớp, giống như bất kỳ một thành phần phần mềm nào khác, chỉ có thể được đánh giá là đúng hay không đúng khi nó gắn liền với một đặc tả nào đó. Như vậy, những tiền điều kiện, hậu điều kiện và điều kiện bất biến chính là những thông tin mà ta có thể thêm vào phần đặc tả của lớp. Điều này cung cấp một cơ sở mà dựa vào đó, ta có thể đánh giá tính đúng đắn: một lớp là đúng nếu và chỉ nếu những cài đặt của nó trong thân của thường trình phù hợp với những tiền điều kiện, hậu điều kiện và điều kiện bất biến. Khái niệm {P}A{Q} được giới thiệu từ đầu giúp cho việc biểu diễn điều này được chính xác. Hãy nhớ ý nghĩa của một công thức đúng đắn là: bất cứ khi nào A được thực thi trong trạng thái thỏa P thì sự thực thi này sẽ kết thúc trong trạng thái thỏa Q. Coi C là một lớp, INV là những điều kiện bất biến của lớp. Với mọi thường trình r của lớp, gọi prer(xr) và postr(xr) là tiền điều kiện và hậu điều kiện của nó, xr là những tham số có thể của r, mà cả tiền điều kiện và hậu điều kiện đều có thể trỏ đến. (Nếu trong phần thường trình, cả tiền điều kiện hoặc hậu điều kiện đều thiếu thì prer hoặc postr là True). Gọi Bodyr là thân của thường trình r. Cuối cùng, DefaultC biểu diễn cho việc xác nhận những thuộc tính của C có giá trị mặc định cùng với kiểu của chúng. Ví dụ, DefaultSTACK2 được nói đến trong lớp ngăn xếp trước là một xác nhận: representation = Void capacity = 0 count = 0 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 58 Những khái niệm này cho phép ta có một định nghĩa chung về tính đúng đắn của lớp: Định nghĩa: tính đúng đắn của lớp Một lớp là đúng với những xác nhận của nó nếu và chỉ nếu: + C1: Với bất kỳ bộ tham số hợp lệ xp nào của thủ tục khởi tạo p thì: {DefaultC and prepp(xp)} Bodyp {postp(xp) and INV} + C2: Với mọi thường trình r được export ra ngoài và bất kỳ bộ tham số hợp lệ xr nào thì: {prepr(xr) and INV} Bodyr {postr(xr) and INV} Quy định này thật sự là một khai báo toán học của lược đồ thông tin trước đây biểu diễn chu kỳ sống của một đối tượng điển hình. Ta hãy cùng xem lại ví dụ về BANK_ACCOUNT: Hình 10-1: Thời gian tồn tại của một đối tượng Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 59 Điều kiện C1 nghĩa là: bất kỳ thủ tục khởi tạo nào (ứng với hình Hình 9-1 trên là make), khi được gọi với những tiền điều kiện được thỏa mãn của nó thì phải trả về được một trạng thái khởi đầu (trong hình trên là S1) thỏa mãn điều kiện bất biến và hậu điều kiện của thủ tục đó. Điều kiện C2 diễn tả rằng bất kỳ thường trình r nào được export (ứng với hình trên là f và g), nếu được gọi trong trạng thái (S1, S2 hay S3) thỏa mãn cả tiền điều kiện và điều kiện bất biến của nó, thì phải kết thúc trong trạng thái thỏa mãn cả hậu điều kiện và điều kiện bất biến của nó. Như vậy, luật C1 là một bước cơ bản của việc dẫn nhập, nói rằng điều kiện bất biến giữ tất cả những đối tượng mới sinh ra là kết quả trực tiếp của một câu lệnh khởi tạo. Luật C2 là một bước dẫn nhập mà thông qua đó, ta quyết định nếu có một thế hệ những thể hiện nào đó thỏa mãn điều kiện bất biến thì thế hệ kế tiếp - tức là một bộ những thể hiện thu được do áp dụng những đặc tính được export của những thành viên trong thế hệ hiện tại – cũng sẽ thỏa mãn nó. Việc bắt đầu từ những đối tượng mới sinh ra và đi từ thế hệ này qua thế hệ khác thông qua những đặc tính được export, ta thu được toàn bộ những thể hiện có thể của một lớp cho phép ta quyết định rằng tất cả thể hiện đó có thỏa mãn điều kiện bất biến hay không. Có 2 ý kiến về mặt thực tiễn như sau: + Nếu một lớp không có mệnh đề creation, ta có thể xem như nó có một thủ tục khởi tạo không tường minh là nothing với một thân rỗng. Áp dụng luật C1 cho Bnothing với ý nghĩa là DefaultC phải bao gồm INV: những giá trị mặc định phải thỏa mãn điều kiện bất biến. + Một yêu cầu có dạng {P}A{Q} không thực thi A trong bất kỳ trường hợp nào mà P không thoả mãn lúc ban đầu. Do đó, hợp đồng sẽ không bị ràng buộc với thường trình nếu client không đáp ứng được những yêu cầu có liên quan với giao tác. Theo đó, định nghĩa tính đúng đắn của lớp không cho phép những thường trình thực thi khi nó vi phạm tiền điều kiện hay điều kiện bất biến. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 60 10.2. Vai trò của những thủ tục khởi tạo Thảo luận về điều kiện bất biến sẽ cho ta cái nhìn sâu hơn về khái niệm của thủ tục khởi tạo. Một điều kiện bất biến của lớp biểu diễn một bộ những thuộc tính mà những đối tượng (những thể hiện của lớp) phải thỏa mãn tại những thời điểm ổn định trong thời gian sống của chúng. Đặc biệt, những thuộc tính này phải được giữ trước khi thể hiện được khởi tạo. Cơ cấu cấp phát đối tượng chuẩn khởi tạo những trường với những giá trị mặc định của những kiểu thuộc tính tương ứng; những giá trị này có thể thỏa mãn hay không điều kiện bất biến. Nếu không, một thủ tục khởi tạo đặc biệt sẽ được yêu cầu để gán giá trị cho những thuộc tính này để chúng thoả mãn điều kiện bất biến. Vì vậy, khởi tạo có thể xem như là một thao tác đảm bảo cho tất cả thể hiện của một lớp được bắt đầu cuộc sống của chúng với một chế độ đúng – tức là thỏa mãn được điều kiện bất biến. Việc biểu diễn đầu tiên của những thủ tục khởi tạo được giới thiệu như một cách để trả lời cho câu hỏi hết sức tầm thường là: làm sao để viết đè những quy luật khởi tạo mặc định khi chúng không thích hợp cho một lớp đặc biệt nào đó, hoặc là trong trường hợp ta muốn cung cấp cho những client nhiều hơn một cơ cấu khởi tạo? Nhưng chỉ với sự giới thiệu về những điều kiện bất biến và những thảo luận một cách lý thuyết cùng với áp dụng luật C1 thì ta chỉ có thể kết luận về vai trò sâu hơn của những thủ tục khởi tạo là: chúng đảm bảo cho bất kỳ thể hiện nào của lớp khi bắt đầu thời gian sống phải thỏa mãn những quy định cơ bản thuộc về lớp đó - tức là thoả mãn những điều kiện bất biến của lớp đó. 10.3. Xem lại về mảng Thư viện lớp ARRAY đã được tóm tắt trong chương trước. Tuy nhiên, bây giờ là lúc đưa ra định nghĩa chính xác cho nó. Khái niệm mảng luôn đòi hỏi phải có tiền điều kiện, hậu điều kiện và một điều kiện bất biến. Đây là một bản phác thảo cùng với những xác nhận. Những tiền điều kiện là cần thiết trong việc truy cập và điều chỉnh mảng với quy định là chỉ số mảng phải Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 61 trong giới hạn cho phép. Điều kiện bất biến biểu diễn mối quan hệ giữa count, lower và upper; nó cho phép count được cài đặt như một hàm chứ không phải một thuộc tính. indexing description: "Mảng giá trị cùng kiểu, truy xuất các phần tử thông qua các chỉ số mảng" class ARRAY [G] creation make feature -- Khởi tạo make (minindex, maxindex: INTEGER) is -- Xác định 2 biên của mảng với minidex và maxindex -- Mảng rỗng nếu minindex > maxindex. require meaningful_bounds: maxindex >= minindex - 1 do ensure exact_bounds_if_non_empty: (maxindex >= minindex) implies ((lower = minindex) and (upper = maxindex)) conventions_if_empty: (maxindex < minindex) implies ((lower = 1) and (upper = 0)) end feature – Truy cập lower, upper, count: INTEGER -- Chỉ số cao nhất vào thấp nhất hợp lệ; kích thước mảng. infix "@", item (i: INTEGER): G is -- Giá trị mảng tại chỉ số i Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 62 require index_not_too_small: lower <= i index_not_too_large: i <= upper do end feature -– Thay đổi thành phần put (v: G; i: INTEGER) is -- Gán giá trị v cho phần tử có chỉ số require index_not_too_small: lower <= i index_not_too_large: i <= upper do ensure element_replaced: item (i) = v end invariant consistent_count: count = upper – lower + 1 non_negative_count: count >= 0 end -- class ARRAY Phần trống duy nhất còn lại là phần cài đặt của thân những thường trình item và put. Chương 11: Kết nối với kiểu dữ liệu trừu tượng Trong phần này, ta sẽ củng cố thêm khái niệm “xác nhận” bằng việc tìm hiểu về sự kết nối giữa các xác nhận và những thành phần của một đặc tả của một kiểu dữ liệu trừu tượng (ADT – Abstract Data Type). Một ADT được tạo bởi 4 thành phần: − Tên kiểu, có thể cùng với những tham số chung (phần TYPES) Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 63 − Danh sách các hàm với những ký hiệu của chúng (phần FUNCTIONS) − Tiên đề (AXIOMS) mô tả những thuộc tính của kết quả − Những quy định để sử dụng được hàm (phần PRECONDITIONS) Ví dụ: ADT của lớp STACK TYPES • STACK [G] FUNCTIONS • put: STACK [G] × G → STACK [G] • remove: STACK [G] →STACK [G] • item: STACK [G] → G • empty: STACK [G] → BOOLEAN • new: STACK [G] AXIOMS For any x: G, s: STACK [G] A1 • item (put (s, x)) = x A2 • remove (put (s, x)) = s A3 • empty (new) A4 • not empty (put (s, x)) PRECONDITIONS • remove (s: STACK [G]) require not empty (s) • item (s: STACK [G]) require not empty (s) 11.1. So sánh đặc tính của lớp với những hàm ADT Để hiểu được mối liên hệ giữa những xác nhận và ADT, trước tiên ta cần tìm hiểu mối liên hệ giữa những đặc tính của lớp và phần tương ứng của ADT – những hàm của ADT. Những hàm này gồm 3 loại: creator, query và command. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 64 Sự phân loại của một hàm f: A × B × Æ X phụ thuộc vào vị trí xuất hiện của ADT (A, B, , X) so với mũi tên , gọi là T . Nếu T chỉ xuất hiện ở bên phải của mũi tên thì f là hàm creator. Trong lớp đối tượng, nó là phương thức khởi tạo. Ví dụ: hàm new Nếu T chỉ có mặt ở bên trái của mũi tên thì f là hàm query. Trong lớp đối tượng, nó là những phương thức truy xuất đến những thuộc tính của các thể hiện của một lớp. Ví dụ: hàm item và empty. Nếu T xuất hiện ở cả 2 bên mũi tên thì f là hàm command. Những hàm này tạo ra những đối tượng mới từ những đối tượng đã có. Trong lớp đối tượng, những hàm này thường được biểu diễn như một phương thức để làm thay đổi một đối tượng hơn là tạo ra một đối tượng mới. Ví dụ hàm put và remove. 11.2. Biểu diễn những tiên đề Từ sự tương ứng giữa những hàm ADT và những đặc tính của lớp, ta có thể suy ra sự tương ứng giữa ngữ nghĩa thuộc tính ADT và những xác nhận. Tiền điều kiện của ADT xuất hiện lại như những mệnh đề tiền điều kiện (precondition clauses) của các thủ tục tương ứng. Một tiên đề, bao gồm một hàm command và một hay nhiều hàm query, xuất hiện lại như những mệnh đề hậu điều kiện (postcondition clauses) trong những thủ tục tương ứng. Những tiên đề chỉ bao gồm những hàm query xuất hiện lại như những hậu điều kiện của những hàm tương ứng hoặc những mệnh đề của điều kiện bất biến. Tiên đề bao gồm những hàm khởi tạo xuất hiện lại trong hậu điều kiện của những thủ tục khởi tạo tương ứng. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 65 11.3. Hàm trừu tượng Hình 11-1: Sự biến đổi giữa những đối tượng trừu tượng và cụ thể A là một ADT và C là một lớp được cài đặt từ A. Lúc này tương ứng với hàm trừu tượng af của A sẽ có hàm cụ thể cf trong lớp C. Mũi tên a mô tả cho sự trừu tượng hóa hàm, với mỗi đối tượng cụ thể (thể hiện của lớp), sự trừu tượng hoá này sẽ sinh ta một đối tượng trừu tượng (thể hiện của ADT). Những hàm trừu tượng này thường là từng phần. Sự tương ứng giữa lớp và ADT (cf ; a) = (a ; af) Trong đó dấu “;” là toán tử kết hợp giữa các hàm. Nói cách khác, nếu ta có hai hàm f và g thì f;g là hàm h sao cho h(x) = g(f(x)) với mọi x (f;g còn được viết dưới dạng g o f ) Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 66 Hai đường đứt khúc cùng chỉ đến đối tượng trừu tượng ABST_2. Kết quả vẫn như nhau ngay cả khi bạn: - Áp dụng sự biến đối cụ thể cf, sau đó trừu tượng hóa kết quả, sinh ra a(cf(CONC_1)). - Trừu tượng hóa trước, sau đó áp dụng sự biến đổi trừu tượng af, sinh ra af(a(CONC_1)). 11.4. Cài đặt những điều kiện bất biến Một số xác nhận xuất hiện trong những điều kiện bất biến nhưng chúng lại không là bản sao trực tiếp trong đặc tả ADT. Những xác nhận này bao hàm những thuộc tính, một số là thuộc tính ẩn mà lúc định nghĩa thì chúng sẽ không có ý nghĩa trong ADT. Một ví dụ đơn giản là những thuộc tính dưới đây xuất hiện trong điều kiện bất biến của lớp STACK4 count_non_negative: 0<=count count_bounded: count<=ca...ng sửa lỗi cho đến khi đạt được tính đúng đắn). Từ khóa xuyên suốt ở đây là Design By Contract. Trong thế giới thực, một hợp đồng tốt là một hợp đồng chỉ định rõ ràng quyền lợi và nghĩa vụ của mỗi bên tham gia, và giới hạn của những quyền và nghĩa vụ này. Trong thiết kế phần mềm, tính đúng đắn và tính vững chắc vô cùng quan trọng, vì vậy ta cần chỉ rõ những điều khoản của hợp đồng như là một điều kiện tiên quyết trước khi hợp đồng có hiệu lực. Những xác nhận cung cấp phương tiện nhằm chỉ rõ những điều được mong đợi và được bảo đảm cho mỗi đối tác của sự ký kết này. 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 Ứng dụng thứ hai này rất cần thiết cho việc sản xuất những thành phần của phần mềm có tính tái sử dụng cao, và tổng quát hơn, trong việc tổ chức những interface của một môđun trong một hệ thống lớn. Tiền điều kiện, hậu điều kiện và những điều kiện bất biến của lớp cung cấp cho những khách hàng tiềm năng của một môđun thông tin cơ bản về những dịch vụ được cung cấp bởi môđun đó. Những thông tin này được biểu diễn bằng một hình thức ngắn gọn và chính xác. Không một tài liệu dài dòng nào có thể thay thế được một tập những xác nhận dùng để biểu diễn xuất hiện trong chính phần mềm. Thể rút gọn này sử dụng xác nhận như là một thành phần quan trọng trong việc trích những thông tin thích hợp cho những khách hàng tiềm năng từ lớp đối tượng. Thể rút gọn này chỉ bao gồm những thông tin có ích cho tác giả của những lớp client, vì vậy nó không cho thấy những đặc tính ẩn cũng như cài đặt của lớp (mệnh đề do). Nhưng thể rút gọn này vẫn giữ lại những xác nhận, chúng sẽ cung cấp những tài liệu cần thiết của hợp đồng mà lớp này quy định với những client. Thể rút gọn của lớp STACK4 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 79 indexing description: " Stacks: Cấu trúc dữ liệu với quy tắc truy xuất LIFO, và có độ lớn cố định." class interface STACK4 [G] creation make feature -- Khởi tạo make (n: INTEGER) is -- Cấp phát cho stack độ lớn n phần tử require non_negative_capacity: n >= 0 ensure capacity_set: capacity = n end feature -– Truy cập capacity: INTEGER -- Số phần tử tối đa của stack count: INTEGER -- Số phần tử của stack item: G is -- Phần tử trên cùng require not_empty: not empty –- i.e: count > 0 end feature -– Báo cáo tình trạng empty: BOOLEAN is -- Kiểm tra stack rỗng? ensure empty_definition: Result = (count = 0) end Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 80 full: BOOLEAN is -- Kiểm tra stack đầy? ensure full_definition: Result = (count = capacity) end feature –- Thay đổi thành phần put (x: G) is -- Thêm phần tử x vào stack. require not_full: not full ensure not_empty: not empty added_to_top: item = x one_more_item: count = old count + 1 end remove is -- Xóa phần tử trên cùng của stack. require not_empty: not empty –- i.e: count > 0 ensure not_full: not full one_fewer: count = old count – 1 end invariant count_non_negative: 0 <= count count_bounded: count <= capacity empty_if_no_elements: empty = (count = 0) end -- class interface STACK4 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 81 Thể rút gọn này không phải là những mã chương trình đúng cú pháp. Nếu ta so sánh những xác nhận trong thể rút gọn này với những xác nhận trong lớp đối tượng, ta thấy rằng tất cả những mệnh đề bao gồm representation đều biến mất. Thể rút gọn này gây sự chú ý đặc biệt bởi những lý do sau: − Tài liệu này có mức độ trừu tượng hơn so với những gì chúng mô tả, đây là một yêu cầu chủ yếu để có một tài liệu có chất lượng. Những cài đặt thực tế (trả lời câu hỏi như thế nào) được loại bỏ, nhưng những xác nhận (trả lời câu hỏi cái gì – hoặc tại sao) vẫn được giữ lại. Lưu ý rằng những ghi chú ở đầu thủ tục (để bổ sung cho xác nhận bằng những giải thích sơ lược về mục đích của thủ tục) và mô tả trong mệnh đề clause cũng được giữ lại. − Với thể rút gọn này, tài liệu không còn được xem như một sản phẩm riêng biệt mà bao gồm trong chính phần mềm. Điều này có nghĩa là chỉ có duy nhất một sản phẩm để bảo trì. Và cũng vì vậy, tài liệu chắc chắn sẽ đúng đắn hơn, bởi vì bạn sẽ không quên việc cập nhật tài liệu mỗi khi thay đổi phần mềm hay ngược lại. − Thể rút gọn này có thể được phát sinh từ lớp đối tượng bằng những công cụ tự động. Chương 15: Giới thiệu công cụ XC# 15.1. Giới thiệu XC# là một phần mở rộng của trình biên dịch C#. Luôn biên dịch sau trình biên dịch C#. Có khả năng kiểm tra mã nguồn và đưa ra các cảnh báo lỗi nếu có. Cho phép người lập trình tự định nghĩa các ràng buộc, luật của riêng mình. Cho phép thêm hay loại bỏ các các khai báo tiền tố, hậu tố, rất hữu dụng cho việc debug chương trình. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 82 15.2. XC# hoạt động như thế nào XC# bao gồm các component thực hiện các tác vụ biên dịch, đưa ra các cảnh báo lỗi, và một số tác vụ khác. XCSharp.Compiler.dll đây là trình biên dịch của XC# XCSharp.Parser.dll đây là bộ phân tích cú pháp của XC#, nó tạo ra CodeDom ASTs từ mã nguồn XCSharp.Interface.dll tạo sự tương tác giữa trình biên dịch và các thuộc tính XCSharp.Attributes.dll and XCSharp.Verifier.dll nắm giữ toàn bộ tập các thuộc tính (như obfuscation, declarative assertions, verification, etc.) XCSharp.VisualStudio.dll nhận dạng và biên dịch Visual Studio solutions XCSharp.AddIn.dll quản lý việc Add_in trong Visual Studio xcsc.exe biên dịch bằng dòng lệnh của XC# Trình biên dịch thông thường như MS C# lấy dữ liệu đầu vào là tập các file mã nguồn và đầu ra là mã thực thi. Tuy nhiên, cách này vẫn còn một hạn chế là không thể hiệu chỉnh được các cư xử bên trong của quá trình biên dịch. XC# cho phép can thiệp vào bên trong quá trình biên dịch bằng cách khai báo các câu lệnh, các luật ngay trong mã nguồn. Điều này cho phép trình biên dịch có thể đưa ra các cảnh báo và thông báo lỗi theo các ràng buộc đã được định nghĩa. 15.3. Khai báo các xác nhận Như đã mô tả ở trên, khai báo các xác nhận cho phép can thiệp vào bên trong quá trình biên dịch, đưa ra các cảnh báo lỗi Các xác nhận có thể là tiền điều kiện hay hậu điều kiện. 15.3.1. Tiền điều kiện − Kiểm tra điều kiện ban đầu của phương thức Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 83 − Thuộc tính Requires giúp xác định điều kiện ban đầu của phương thức. Đối của Requires đơn giản chỉ là một đoạn text mô tả điều kiện ban đầu của phương thức. Ví dụ : [Requries (“obj != null”)] public void SetData(Object obj) { } 15.3.2. Hậu điều kiện − Kiểm tra điều kiện kết thúc của phương thức − Thuộc tính Ensures giúp xác định điều kiện kết thúc của phương thức. Đối của Ensures cũng là một đoạn text mô tả điều kết thúc của phương thức. Ví dụ : [Ensures (“result != null”)] public Object GetData() { Object obj; rerurn obj; } 15.3.3. Một số thuộc tính mà XC# qui ước sẵn Tên Mô tả Sử dụng NotNull Yêu cầu đối tượng nhập vào hay trả về phải “not null” Void SetData([NotNull] Object obj) {} //obj != null Equal Yêu cầu đối Void SetData([Equal (5)] int Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 84 tượng nhập vào hoặc trả về phải “equal” với một giá trị cho trước value) {} //value == 5 ExclusiveBetween Yêu cầu đối tượng nhập vào hoặc trả về phải nẳm trong một khoảng cho trước Void SetData([ExclusiveBetween (1, 5)] int value) {} //1 <= value <= 5 GreaterThan Yêu cầu đối tượng nhập vào hoặc trả về phải lớn hơn với một giá trị cho trước Void SetData([GraeterThan (5)] int value) {} //value > 5 GreaterThanOrEqual Yêu cầu đối tượng nhập vào hoặc trả về phải lớn hơn hau bằng với một giá trị cho trước Void SetData([GraeterThanOrEqual (5)] int value) {} //value >= 5 Is Yêu cầu đối tượng nhập vào hoặc trả về phải “Is” một giá trị cho trước Void SetData([Is (typeof (HOCSINH))] Object obj) {} //kiểu của obj phải là HOCSINH LessThan Yêu cầu đối tượng nhập vào hoặc trả về phải Void SetData([LessThan (5)] int value) {} //value < 5 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 85 nhỏ hơn một giá trị cho trước LessThanOrEqual Yêu cầu đối tượng nhập vào hoặc trả về phải nhỏ hơn hoặc bằng một giá trị cho trước Void SetData([LessThanOrEqual (5)] int value) {} //value <= 5 MaxCount Yêu cầu số thành phần của đối tượng nhập vào hoặc trả về phải nhỏ hơn hoặc bằng một giá trị cho trước Void SetData([MaxCount (10)] ArrayList arr) {} //arr.Count <= 10 MaxLength Quy ước chiều dài tối đa của một chuỗi là một giá trị cho trước Void SetData([MinLength (10)] String str) {} //str.Length <= 10 MinCount Yêu cầu số thành phần của đối tượng nhập vào hoặc trả về phải lớn hơn hoặc bằng một giá trị cho trước Void SetData([MinCount (10)] ArrayList arr) {} //arr.Count >= 10 MinLength Quy ước chiều dài tối thiểu của Void SetData([MinLength (10)] String str) {} Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 86 một chuỗi là một giá trị cho trước //str.Length >= 10 NotEqual Yêu cầu đối tượng nhập vào hoặc trả về phải “not equal” với một giá trị cho trước Void SetData([NotEqual (5)] int value) {} //value != 5 OneOf Quy ước giá trị nhập vào hay trả về của một giá trị phải nằm trong các giá trị cho trước Void SetData([OneOf (1,3,5,7,9,10)] int value) {} //value có giá trị là một trong các giá trị sau : [1,3,5,7,9,10] . 15.4. Ví dụ lớp Stack private Object[] representation; public int count; // inv: count>=0 (count khong am) public int capacity;// inv: count<=capacity private int current;// inv: current>=0 // [Requires ("size >= 0")] [Ensures ("representation != null && capacity == size && IsEmpty()")] public MyStack([GreaterThanOrEqual (0)]int size) { Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 87 capacity = size; representation = new Object[capacity]; } [Requires ("!IsFull()")] [Ensures ("!IsEmpty() && (int)representation[count-1] == obj")] public void put(int obj) { representation[count++] = obj; } [Requires ("!IsEmpty()")] [Ensures ("!IsFull()")] public void remove() { --count; } [Ensures ("result == (count == capacity)")] public bool IsFull() { return count == capacity; } [Ensures ("result == (count == 0)")] public bool IsEmpty() { return count == 0; } Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 88 [Requires ("position >= 0 && position < count")] [Ensures ("current == position")] public void SetCurrentItem(int position) { current = position; } [Ensures ("current == count - 1")] public void ResetCurrentItem() { current = count - 1; } [Requires ("!IsEmpty()")] [Ensures ("result != null && current >= 0")] public Object nextItem() { return representation[current--]; } Chương 16: Kết quả thực nghiệm: công cụ DCS 16.1. Nguyên lý làm việc DCS là một Add-In trong môi trường Visual C#, nguyên lý làm việc của DCS là bắt sự kiện OnBuildBegin của project, thực hiện những bước sau: ƒ Duyệt qua tất cả những lớp của project (mỗi lớp ứng với một file *.cs, trừ file AssemblyInfo.cs) và lưu thông tin của mỗi lớp (tên lớp, tên file, tên những lớp dẫn xuất). Trong mỗi lớp, chương trình thực hiện những bước sau: − Kiểm tra xem lớp có chứa những xác nhận (Invariant, PreCondition, PostCondition) hay không. Lưu thông tin của Invariant (các mệnh đề và thông báo Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 89 tương ứng của Invariant) nếu có, sau đó, duyệt qua từng hàm trong lớp, trong mỗi hàm, thực hiện những bước sau: + Kiểm tra hàm có PreCondition hoặc PostCondition hay không. Nếu có, lưu lại thông tin của hàm. Thông tin lưu trữ gồm có: Tên hàm, PreCondition và PostCondition (lưu các mệnh đề và thông báo). + Đổi tên hàm, nếu lớp có Invariant, tất cả tên hàm sẽ được đổi, nếu không có Invariant, chỉ những hàm có PreCondition hoặc PostCondition mới được đổi tên. Tên hàm được đổi như sau: Tên hàm mới = @origin_[Tên hàm cũ] − Dựa vào thông tin đã lưu trữ được, bổ sung thông tin về những xác nhận của các lớp dẫn xuất cho mỗi lớp. Việc lưu trữ này thực hiện bằng cách duyệt qua tất cả các lớp. Trong đó, ở mỗi lớp: + Duyệt qua tất cả tất cả những lớp dẫn xuất của lớp này (đã được lưu trữ), lưu thông tin Invariant của những lớp dẫn xuất. + Duyệt qua các hàm, hàm nào là hàm cài đặt lại sẽ được lưu trữ thông tin về Assertion của lớp dẫn xuất. ƒ Phát sinh source code bổ sung để kiểm tra các xác nhận cho các lớp. Trong mỗi lớp, source code sẽ được thêm vào phía dưới của source code hiện tại. Mỗi hàm sẽ phát sinh source code tương ứng của mình. Với mỗi hàm, dựa vào thông tin đã lưu trữ, source code được phát sinh như sau: [Khai báo hàm theo tên hàm cũ] { Gọi hàm kiểm tra PreCondition Gọi hàm kiểm tra Invariant Gọi hàm gốc (hàm đã được đổi tên @origin_*) Gọi hàm kiểm tra PostCondition Gọi hàm kiểm tra Invariant } Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 90 [Hàm kiểm tra PreCondition] { Các câu lệnh kiểm tra các mệnh đề và xuất thông báo tương ứng của PreCondition } [Hàm kiểm tra Invariant] { Các câu lệnh kiểm tra các mệnh đề và xuất thông báo tương ứng của Invariant } [Hàm kiểm tra PostCondition] { Các câu lệnh kiểm tra các mệnh đề và xuất thông báo tương ứng của PostCondition } Ví dụ: Hàm và PreCondition, PostCondition, Invariant: /* @#$Require: !IsFull() # Stack Full @#$Ensure: !IsEmpty() (int)representation[count-1] == obj count == OLD_count + 1 $int # New count = Old count + 1 */ public void put(int obj) Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 91 { representation[count++] = obj; } /* @#$Invariant: count >= 0 count <= capacity current >= 0 */ Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 92 Code phát sinh: public void put(int obj) { int OLD_count = count; if(put_PreCondition(obj)!="") throw new Exception("PreCondition Violated at [MyStack - public void put(int obj)]:" +put_PreCondition(obj)); if(put_Invariant(obj)!="") throw new Exception("Invariant Violated at [MyStack]:" +put_Invariant(obj)); @origin_put(obj); if(put_PostCondition(obj,OLD_count)!="") throw new Exception("PostCondition Violated at [MyStack - public void put(int obj)]:" +put_PostCondition(obj,OLD_count)); if(put_Invariant(obj)!="") throw new Exception("Invariant Violated at [MyStack]:" +put_Invariant(obj)); } private string put_PreCondition(int obj) { if (!(!IsFull() )) return " Stack Full"; return ""; } Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 93 private string put_Invariant(int obj) { if (!(count >= 0)) return " "; if (!(count <= capacity)) return " "; if (!(current >= 0)) return " "; return ""; } private string put_PostCondition(int obj,int OLD_count) { if (!(!IsEmpty())) return " "; if (!((int)representation[count-1] == obj)) return " "; if (!(count == OLD_count + 1 )) return " New count = Old count + 1"; return ""; } Project được biên dịch theo source code mới. Bắt sự kiện OnBuildDone của project, thực hiện việc trả lại source code như cũ cho project. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 94 16.2. Thiết kế 16.2.1. Tổng thể Hình 16-1: Sơ đồ thiết kế tổng thể Danh sách các lớp đối tượng: STT Tên Ý nghĩa 1 Configuration Màn hình cho phép người dùng enable hoặc disable chức năng kiểm tra của PreCondition, PostCondition, Invariant. 2 Connect Lớp chính của chương trình, đây là lớp quản lý mọi thao tác của Add-In với project. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 95 3 ProjectInfo Lớp đối tượng để lưu trữ thông tin của project hiện hành. 4 ClassInfo Lớp đối tượng để lưu trữ thông tin của một lớp trong project. 5 FunctionInfo Lớp đối tượng để lưu trữ thông tin của một phương thức trong class. 6 Assertion Lớp đối tượng để lưu trữ thông tin của một Assertion (precondition, postcondition, invariant) 7 Extra Lớp đối tượng chứa những hàm riêng, không thuộc trách nhiệm của những lớp trên. 16.2.2. Chi tiết các lớp đối tượng 16.2.2.1 Màn hình Configuration Hình 16-2: Màn hình Configuration Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 96 Hình 16-3: Chi tiết màn hình Configuration Danh sách các đối tượng thể hiện: STT Tên Loại / Kiểu Ý nghĩa 1 chkPreCondition checkbox Xác định có sử dụng PreCondition hay không. 2 chkPostCondition checkbox Xác định có sử dụng PostCondition hay không. 3 chkInvariant checkbox Xác định có sử dụng Invariant hay không. 4 chkBasePre checkbox Xác định có sử dụng PreCondition của những lớp dẫn xuất hay không. 5 chkBasePost checkbox Xác định có sử dụng PostCondition của những lớp dẫn xuất hay không. 6 chkBaseInv checkbox Xác định có sử dụng Invariant của những lớp dẫn xuất hay không. 7 btnOK Button Đồng ý với những thông số đã chọn và thoát khỏi màn hình 8 btnClose Button Thoát khỏi màn hình Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 97 Danh sách các đối tượng xử lý: STT Tên Lớp/Kiểu Ý nghĩa 1 PreConditionCheck bool Xác định có sử dụng PreCondition hay không. 2 PostConditionCheck bool Xác định có sử dụng PostCondition hay không. 3 InvariantCheck bool Xác định có sử dụng Invariant hay không. 4 BasePreConditionCheck bool Xác định có sử dụng PreCondition của những lớp dẫn xuất hay không. 5 BasePostConditionCheck bool Xác định có sử dụng PostCondition của những lớp dẫn xuất hay không. 6 BaseInvariantCheck bool Xác định có sử dụng Invariant của những lớp dẫn xuất hay không. Danh sách các biến cố : STT Thể hiện Biến cố Xử lý 1 Form Load Hiển thị màn hình Configuration cho phép người dùng enable hoặc disable chức năng kiểm tra của PreCondition, PostCondition, Invariant. 2 btnOK Click Lưu những thông số đã chọn trên màn hình và thoát khỏi màn hình 3 btnClose Click Thoát khỏi màn hình. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 98 16.2.2.2 Lớp Connect Hình 16-4: Lớp Connect Danh sách các biến thành phần: STT Tên Kiểu/Lớp Ý nghĩa 1 projectInfo ProjectInfo Lưu trữ thông tin của Project hiện hành. Danh sách các biến cố: STT Thể hiện Biến cố Xử lý 1 Command Exec RightClick vào màn hình soạn thảo code, xuất hiện pop-up menu. Click vào command này, màn hình Configuration hiển thị cho phép người dùng enable hoặc disable chức năng kiểm tra của PreCondition, PostCondition, Invariant. 2 Project BuildBegin Bắt đầu chạy chương trình: ¾ Lưu thông tin của project hiện hành: thông tin của các phương thức trong các lớp (tên phương thức, precondition, postcondition) và Invariant của mỗi lớp trong project. ¾ Đổi tên tất cả các phương thức có liên quan đến contract. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 99 ¾ Lưu thông tin về contract của những lớp dẫn xuất cho lớp kế thừa. ¾ Phát sinh source code để kiểm tra những Assertion. 3 Project BuildDone Trả source code về như cũ. 16.2.2.3 Lớp ProjectInfo Hình 16-5: Lớp ProjectInfo Danh sách biến thành phần: STT Tên Kiểu/Lớp Ý nghĩa 1 classInfo ClassInfo[] Mảng các đối tượng ClassInfo, mỗi đối tượng lưu trữ thông tin một lớp của project. 2 NumFile int Số file trong project này. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 100 Danh sách hàm thành phần: STT Tên Tham số Kết quả Xử lý 1 FileCount Đếm số file của project, lưu vào biến NumFile 2 ChangeAllFuncName Duyệt qua từng lớp, gọi phương thức đổi tên hàm của mỗi lớp đó. 3 SaveAssertionOfBase Classes Duyệt qua từng lớp, gọi phương thức lưu thông tin về assertion của những lớp dẫn xuất của từng lớp đó 4 GenerateCode Duyệt qua từng lớp, gọi phương thức thêm vào phần code kiểm tra Assertion của từng lớp đó. 5 ReturnOriginalCode Duyệt qua từng lớp, gọi phương thức trả code về như cũ của từng lớp đó. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 101 16.2.2.4 Lớp ClassInfo Hình 16-6: Lớp ClassInfo Danh sách biến thành phần: STT Tên Kiểu/Lớp Ý nghĩa Ghi chú 1 functionInfo FunctionInfo[] Mảng các đối tượng FunctionInfo, mỗi đối tượng lưu trữ thông tin một hàm của lớp. 2 NumFunc int Số hàm trong class này. 3 Invariant Assertion Đối tượng lớp Assertion để lưu trữ thông tin về Invariant của lớp. 4 BaseInvariant Assertion[] Mảng đối tượng lớp Assertion để lưu trữ thông tin về Invariant của những Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 102 lớp dẫn xuất. 5 FileName string Tên file chứa lớp. Mỗi file chỉ được chứa 1 lớp 6 ClassName string Tên lớp. 7 BaseClassName string[] Mảng tên các lớp dẫn xuất. 8 extra Extra Đối tượng lớp Extra, dùng để gọi những hàm riêng, không thuộc trách nhiệm của những lớp chính. Danh sách hàm thành phần: STT Tên Tham số Kết quả Xử lý 1 FuncCount Đếm số hàm của lớp, lưu vào biến NumFunc 2 GetClassName Phân tích code để lấy tên của lớp, lưu vào ClassName. 3 GetBaseClassesName Phân tích code để lấy tên của những lớp dẫn xuất của lớp này, lưu vào BaseClassName. 4 SaveAssertionOfBase Class ClassInfo [] Lưu Invarian, PreCondition, PostCondition của những lớp dẫn xuất. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 103 5 SaveInvariantInfo Lưu thông tin Invariant của lớp vào biến Invariant. 6 ChangeFuncName Duyệt qua từng hàm trong lớp, lưu thông tin của từng hàm (tên hàm, PreCondition, PostCondition), sau đó đổi tên hàm. 7 GenerateCode Tìm vị trí thích hợp trong code, gọi hàm CodeGenerated để phát sinh code vào đó. 8 CodeGenerated string Duyệt qua từng hàm, gọi phương thức phát sinh code của từng hàm tương ứng, trả ra chuỗi code đã được phát sinh. 9 ReturnOriginalCode Xoá phần code phát sinh và điều chỉnh tên hàm về như cũ. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 104 16.2.2.5 Lớp FunctionInfo Hình 16-7: Lớp FunctionInfo Danh sách biến thành phần: STT Tên Kiểu/Lớp Ý nghĩa 1 PreCondition Assertion Đối tượng lớp Assertion để lưu trữ thông tin về PreCondition của hàm. 2 PostCondition Assertion Đối tượng lớp Assertion để lưu trữ thông tin về PostCondition của hàm. 3 FunctionName string Biến lưu tên hàm. 4 BasePreCondition Assertion[] Mảng đối tượng lớp Assertion để lưu trữ thông tin về PreCondition của những lớp dẫn xuất. 5 BasePreCondition Assertion[] Mảng đối tượng lớp Assertion để lưu trữ thông tin về PostCondition của những lớp dẫn xuất. 6 Extra Extra Đối tượng lớp Extra, dùng để gọi những hàm riêng, không thuộc trách nhiệm của những lớp chính. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 105 Danh sách hàm thành phần: STT Tên Tham số Kết quả Xử lý Ghi chú 1 ChangeName Đổi tên hàm theo dạng @origin_[Tên cũ] 2 SaveContractsInfo Lưu thông tin PreCondition và PostCondition của hàm vào biến PreCondition và PostCondition. 3 GetVar string string[] Phân tích một mệnh đề của Assertion để lấy ra biến và kiểu dữ liệu dùng cho những mệnh đề có từ khoá OLD 4 GetVarHaveOLD Keyword Assertion string[][] Với mỗi mệnh đề của một đối tượng Assertion, gọi hàm GetVar để lấy biến và kiểu dữ liệu. Chỉ làm việc với những mệnh đề có từ khoá OLD 5 GenerateCode Dùng những tên hàm đã lưu, phát sinh ra những hàm mới. Những hàm này sẽ gọi lại Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 106 những hàm gốc (đã bị đổi tên) cùng với code kiểm tra những PreCondition, PostCondition và Invariant của hàm. 16.2.2.6 Lớp Assertion Hình 16-8: Lớp Assertion Danh sách biến thành phần: STT Tên Kiểu/Lớp Ý nghĩa Ghi chú 1 Routine string Lưu tên thủ tục(tên hàm) chứa Assertion này. Giá trị rỗng đối với Invariant 2 ConditionFull string[] Lưu trữ toàn bộ mệnh đề của Assertion. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 107 3 Condition string Lưu trữ toàn bộ mệnh đề của Assertion. Khác ConditionFull ở chỗ không lưu kiểu dữ liệu của biến có từ khoá OLD 4 Message string[] Lưu những Message đi kèm với mỗi Condition 5 Extra Extra Đối tượng lớp Extra, dùng để gọi những hàm riêng, không thuộc trách nhiệm của những lớp chính. Danh sách hàm thành phần: STT Tên Tham số Kết quả Xử lý 1 GenerateAssertion Code string FuncName, string Type string Dựa vào FuncName và Type (Precondition, PostCodition, Invariant, BasePreCondition, BasePostCondition, BaseInvariant) để phát sinh hàm kiểm tra Assertion. 2 GenerateCode string FuncName, string Type, string[][] OLDVar Phát sinh trong hàm FuncName những dòng code kiểm tra gọi đến những hàm kiểm tra Assertion đã tạo ra bằng Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 108 GenerateAssertionCode. OLDVar là mảng chứa những biến có từ khoá OLD của PostCondition và kiểu dữ liệu tương ứng để phát sinh code kiểm tra đối với những biến này. 3 GenerateAssertion CodeBasePre Assertion ass, string FuncName, string Type string Dựa vào FuncName và Type (Precondition, PostCodition, Invariant, BasePreCondition, BasePostCondition, BaseInvariant) để phát sinh hàm kiểm tra Assertion. Hàm này tương tự hàm GenerateAssertionCode nhưng chỉ dùng trong trường hợp lớp dẫn xuất có PreCondition, lúc này cần truyền tham số kiểu Assertion cho hàm. 4 GenerateCode_Ba sePre string FuncName, Assertion[] BasePreCondition Chức năng giống hàm GenerateCode nhưng hỉ dùng trong trường hợp lớp dẫn xuất có chứa PreCondition, vì trường hợp này code phát sinh Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 109 khác với những trường hợp còn lại. 16.2.2.7 Lớp Extra Hình 16-9: Lớp Extra Danh sách hàm thành phần: STT Tên Tham số Kết quả Xử lý 1 IsContractor string Line bool Kiểm tra xem dòng Line có phải là khai báo của một contructor không. 2 IsAccessibilityL evelFound string s bool Kiểm tra xem dòng s có chứa một trong những từ khóa {"private", "public", "protected", "internal","protected internal", "static" } 3 IsContain string large, string small bool Kiểm tra chuỗi large có chứa chuỗi small. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 110 4 IsHaveContract EditPoint e, TextDocument t bool Kiểm tra hàm tại điểm EditPoint e, trong văn bản TextDocument t có chứa PreCondition hoặc PostCondition. 5 GetReturnType string FuncName string Lấy kiểu trả về của FuncName này. 6 GetFuncName string FuncDec,int Flag string Từ khai báo của hàm (vd: public int A(int x) ), trả về 2 dạng: ¾ Flag=1: A(x) ¾ Flag=2: A(int x) 7 IsHaveVar string FName bool Kiểm tra FName có tham số không. 8 FixFuncName string FName, string Type string Sửa tên hàm FName() thành FName_[Type](), trong đó, Type là PreCondition, PostCondition, Invariant hay BasePreCondition, BasePostCondition, BaseInvariant. 9 AddOLDVar string FName1, string FName2, string[][] OLDVar OLDVar là mảng các biến và kiểu dữ liệu tương ứng, sửa đổi FName1 và FName2 bằng cách thêm những thông tin của OLDVar vào tham số. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 111 KẾT LUẬN Sau khi nghiên cứu đề tài, chúng em đã hiểu khá rõ về công nghệ Design By Contract và khả năng ứng dụng của nó trong lập trình hướng đối tượng. Đồng thời, để phục vụ cho yêu cầu của đề tài cũng như giúp cho việc hoàn thiện kiến thức đã tìm hiểu được, chúng em đã xây dựng một công cụ hỗ trợ Design By Contract dưới dạng Add-In cho C#. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 112 HƯỚNG PHÁT TRIỂN − Xây dựng công cụ hỗ trợ Design By Contract cho những môi trường lập trình khác. − Mở rộng khả năng kiểm tra của công cụ, có thể kiểm tra những điều kiện thiết thực hơn. − Mở rộng những kiểu dữ liệu kiểm tra của công cụ, có thể kiểm tra kiểu đối tượng chứ không chỉ dừng lại ở các kiểu dữ liệu cơ sở. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 113 TÀI LIỆU THAM KHẢO [1] B. Meyer, Object-Oriented Software Construction, Prentice Hall, 2nd edition, 1997. [2] Eiffel Software, Design By Contract. [3] ResolveCorp, eXtensible C# - Design by contract Add-In for C# [4] Man Machine Systems, Design by contract tool for Java—JMSAssert. [5] Kevin McFarlane, Design by Contract Framework for C#. [6] Parasoft Corp, Jcontract home page. [7] R. Kramer, iContract home page. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 114 Ý KIẾN CỦA GIÁO VIÊN PHẢN BIỆN