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

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<=capacity Những xác nhận như thế này là những điều kiện bất biến của lớp, gọi là cài đặt của điều kiện bất biến (implementation invariant). Chúng đáp ứng cho việc biểu diễn tính vững chắc của những đại diện được chọn trong lớp (ở đây là count, capacity và representation) có quan hệ với những ADT tương ứng. Hình 10-1 đã giúp ta hiểu rõ về cài đặt của điều kiện bất biến. Nó minh họa cho những thuộc tính đặc trưng của hàm trừu tượng a (biểu diễn bằng những mũi tên dọc). Gọi hàm a sẽ nối mỗi thành phần nguồn với nhiều nhất một thành phần đích. Nếu ta đi theo chiều ngược lại của mũi tên để xét nghịch đảo của a (có thể gọi là quan hệ biểu diễn) , ta sẽ thấy rằng đó không phải là một hàm, bởi vì có thể có nhiều biểu diễn của một đối tượng trừu tượng. Xét mảng thể hiện cho STACK thông qua cặp <representation, count>, một STACK trừu tượng có nhiều biểu diễn khác nhau, tất cả đều có giá trị count và các phần tử từ 1 đến count của mảng representation giống nhau, nhưng giá trị capacity thể hiện kích thước mảng có thể là bất kỳ giá trị nào lớn Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 67 hơn hoặc bằng count, và những phần tử có chỉ số vượt quá count có thể có giá trị tùy ý. Quan hệ cài đặt thường không phải là một hàm, nhưng sự nghịch đảo của nó (mũi tên hướng lên) là một hàm thật sự vì mỗi đối tượng cụ thể biểu diễn cho nhiều nhất một đối tượng trừu tượng. Trong ví dụ về lớp STACK của chúng ta, mỗi cặp hợp lệ chỉ biểu diễn cho một STACK trừu tượng. Hình 11-2: Hai cài đặt của cùng một đối tượng trừu tượng Cả hai stack cụ thể trên đây đều là cài đặt (implementation) của stack trừu tượng bao gồm 3 phần tử 342, -133 và 5. Việc a là một hàm là một yêu cầu chung: nếu một đối tượng cụ thể là cài đặt của nhiều đối tượng trừu tượng, đại diện được chọn sẽ trở nên mơ hồ và không thích hợp. Vì vậy mũi tên a nên vẽ theo chiều như trên để mô tả cho sự kết nối giữa kiểu cụ thể và trừu tượng. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 68 Cài đặt những điều kiện bất biến là một phần của những xác nhận không có bản đối chiếu trong đặc tả ADT. Nó không liên hệ với ADT mà là với những biểu diễn của nó. Nó định rõ khi một đối tượng cụ thể thật sự là cài đặt của một (và chỉ một) đối tượng trừu tượng. Chương 12: Một chỉ thị xác nhận Những tiền điều kiện, hậu điều kiện và điều kiện bất biến của lớp là những thành phần trung tâm của phương pháp sử dụng chỉ thị xác nhận (assertion instruction). Chúng tạo nên sự kết nối giữa việc xây dựng phần mềm hướng đối tượng và những lý thuyết bên dưới về kiểu dữ liệu trừu tượng (Abstract Data Type). Có những xác nhận mặc dù ít đặc thù hơn nhưng cũng có vai trò quan trọng trong quy trình phát triển phần mềm. Trong đó có chỉ thị check và những vòng lặp có bất biến và điều kiện biến đổi (loop invariant và variant) Chỉ thị check được sử dụng để thể hiện sự tin chắc của người viết phần mềm rằng một thuộc tính nào đó sẽ thỏa mãn những tình huống nào đó trong việc tính toán. Cú pháp: check assertion_clause1 assertion_clause2 … assertion_clausen end Khi chương trình thực thi thì những xác nhận assertion_clauseX sẽ được bảo đảm. Đây là cách để chắc chắn một lần nữa rằng những thuộc tính nhất định được thỏa mãn, và quan trọng hơn, nó giúp những người đọc phần mềm hiểu được những giả thuyết mà ta dựa vào. Việc viết phần mềm đòi hỏi sự xác nhận thường xuyên những thuộc tính của đối tượng. Xét ví dụ về hàm sqrt(x), bất cứ hàm nào gọi Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 69 đến sqrt(x) đều dựa vào xác nhận rằng x không âm. Xác nhận này có thể hiển hiện trong ngữ cảnh, ví dụ như một câu lệnh if...then... if x >= 0 then y := sqrt (x) end nhưng nó cũng có thể không trực tiếp như trên, ví dụ như x đã được gán trước đó: x := a^2 + b^2 Chỉ thị check sẽ giúp biểu diễn xác nhận đó nếu nó không hiển hiện trong câu lệnh x := a ^2 + b^2 … Other instructions … check x >= 0 -- Because x was computed above as a sum of squares end y := sqrt (x) Không cần điều kiện if...then... cho lời gọi hàm sqrt trong trường hợp này, check đã xác nhận rằng lời gọi hàm là đúng. Lưu ý rằng chỉ thị check này không làm ảnh hưởng đến thuật toán của thủ tục. Ví dụ trên đã cho ta thấy sự hữu ích của check, nó đóng vai trò một tiền điều kiện của một lời gọi hàm. Một trường hợp khác cần lưu ý, khi ta viết một lời gọi hàm có dạng x.f, ta đã chắc chắn rằng x không rỗng, cho nên ta sẽ không viết if x != Void then... nhưng sự không rỗng của x lại không hiển hiện trong ngữ cảnh này. Ta đã gặp trường hợp này trong hàm put và remove lớp STACK3. Thân hàm put gọi đến hàm tương ứng trong lớp STACK2: Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 70 if full then error := Overflow else check representation /= Void end representation.put (x); error := 0 end Ở đây người đọc sẽ nghĩ rằng không an toàn khi gọi representation.put(x); như vậy, bởi vì không có một sự kiểm tra nào trước đó về sự không rỗng của representation. Nhưng nếu để ý kỹ, bạn sẽ thấy rằng nếu full sai thì capacity phải là số dương. Vì vậy, representation không thể là rỗng. Đây là một điều rất quan trọng và sẽ là một phần trong cài đặt các ràng buộc của lớp. Trong thực tế, với cài đặt đầy đủ của một ràng buộc được định trước, ta nên viết chỉ thị check như sau: check representation_exists: representation /= Void -- Because of clause representation_exists_if_not_full of the -- cài đặt điều kiện bất biến. end Trong những sự tiếp cận thông thường của việc xây dựng phần mềm, mặc dù những lời gọi hàm và những phương thức khác thường tin tưởng vào sự đúng đắn của chúng nhờ những xác nhận khác nhau, nhưng chúng vẫn là những xác nhận không tường minh. Lập trình viên sẽ tự thuyết phục mình rằng một thuộc tính luôn luôn được giữ ở một thời điểm nào đó, và đưa phân tích này vào trong mã nguồn; nhưng sau một thời gian, chỉ còn lại mã nguồn, không còn những phân tích đó nữa. Vài tháng sau, một người nào đó (có thể là chính tác giả), muốn tìm hiểu lại phần mềm, sẽ không thể biết được những thừa nhận không tường minh đó, và sẽ phải mất nhiều công sức để hình dung lại được nó. Chỉ thị check sẽ giúp ta tránh khỏi trường hợp đó. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 71 Chương 13: Vòng lặp có điều kiện bất biến và điều kiện biến đổi 13.1. Vấn đề vòng lặp Khả năng lặp lại một tính toán với một số lần tùy ý một cách dễ dàng là một khả năng vượt xa con người của máy tính. Vì thế, vòng lặp có vai trò rất quan trọng trong ngôn ngữ lập trình. Nhưng vòng lặp cũng chứa đựng nhiều rủi ro vì rất khó khăn để có một vòng lặp chính xác. Những vấn đề hay gặp là: − Lỗi “off-by-one” (biểu diễn sự lặp lại quá nhiều hay quá ít). − Kiểm soát không tốt ở biên, ví dụ như một vòng lặp làm việc tốt trên một mảng nhiều phần tử nhưng lại bị lỗi khi mảng rỗng hay chỉ có một phần tử). − Vòng lặp vô tận. 13.2. Những vòng lặp đúng Việc sử dụng khôn ngoan xác nhận sẽ giúp ta giải quyết những vấn đề này. Một vòng lặp có thể có một xác nhận liên kết, gọi là vòng lặp có điều kiện bất biến (loop invariant). Cũng có khái niệm “loop variant (vòng lặp có điều kiện biến đổi)”. Đây không phải là một xác nhận mà là một biểu thức nguyên. Hai khái niệm này sẽ giúp ta bảo đảm sự chính xác của vòng lặp. Xét ví dụ tính giá trị lớn nhất của một mảng số nguyên: maxarray (t: ARRAY [INTEGER]): INTEGER is -- Giá trị lớn nhất của mảng t require t.capacity >= 1 local i: INTEGER do from i := t.lower Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 72 Result := t @ lower until i = t.upper loop i := i + 1 Result := Result.max (t @ i) end end Ta thấy rằng ở đây ta có thể gán i := t.lower và Result := t@lower mà không cần bận tâm đến việc mảng t tại vị trí lower có phần tử nào không, có được điều này là nhờ vào việc sử dụng xác nhận, chính là tiền điều kiện: require t.capacity >= 1 Đặc điểm của điều kiện bất biến này là mỗi lần lặp, Result luôn là giá trị lớn nhất của phần mảng số nguyên đã được xét. 13.3. Những thành phần của một vòng lặp đúng Ví dụ trên minh họa cho một lược đồ tổng quát của việc tính toán bằng vòng lặp. Bạn đã xác định được rằng lời giải cho vấn đề là một phần tử của một mặt phẳng n chiều POST, vì vậy việc giải quyết vấn đề chính là việc tìm một phần tử của POST. Trong một số trường hợp, POST chỉ có một phần tử (chính là lời giải), nhưng tổng quát thường có nhiều lời giải thích hợp. Những vòng lặp trở nên hữu ích khi bạn không có cách nào làm việc trực tiếp với POST nhưng lại thấy được một con đường gián tiếp: đầu tiên là nhắm vào một mặt phẳng m chiều INV chứa POST (m > n); sau đó tiếp cận POST, lặp đi lặp lại nhưng vẫn bám vào INV. Xem hình minh họa dưới đây: Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 73 Hình 13-1: Một vòng lặp tính toán Một tính toán bằng vòng lặp gồm những thành phần sau: Mục tiêu post, là một hậu điều kiện, được định nghĩa như là một thuộc tính mà bất cứ trạng thái cuối nào của sự tính toán đều phải thỏa mản. Ví dụ như: “Result là giá trị lớn nhất của mảng”. Mục tiêu này được biểu diễn trong hình minh họa là một tập hợp những trạng thái POST thỏa mãn post. Điều kiện bất biến inv, là một sự tổng quát hóa của mục tiêu (post là một trường hợp đặc biệt của inv). Ví dụ: “Result là giá trị lớn nhất của phần mảng không rỗng bắt đầu từ biên thấp nhất”. Điều kiện bất biến được biểu diễn trong hình minh họa là một tập hợp những trạng thái INV thỏa mãn inv. Điểm khởi động init thuộc INV, điểm này thỏa mãn điều kiện bất biến. Ví dụ: khi giá trị của i là biên dưới của mảng và giá trị của Result là phần tử mảng tương ứng tại vị trí đó, thỏa mãn điều kiện bất biến bởi vì phần tử lớn nhất của mảng một phần tử chính là phần tử đó. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 74 Sự biến đổi body (bắt đầu từ một điểm trong INV chứ không phải trong POST) phát sinh ra một điểm tiến đến gần POST hơn nhưng vẫn thuộc INV. Trong ví dụ trên, sự biến đổi này mở rộng mảng lên từng phần tử và thay thế Result bằng phần tử thêm đó nếu nó lớn hơn Result. Thân vòng lặp trong hàm maxarray ví dụ ở trên là cài đặt của sự biến đổi này. Biên trên dựa vào số body cần thiết để đưa điểm trong INV đến POST. Đây là biến. Tính toán xấp xỉ là phương pháp chính của toán giải tích, nhưng ý tưởng này thì được áp dụng rộng rãi hơn. Sự khác biệt cơ bản là trong toán học thuần túy, ta chấp nhận có sự tồn tại của một giới hạn, mặc dù không thể đạt được giới hạn đó. Ví dụ như 1/n có giới hạn là 0 nhưng không có n cụ thể nào để đạt được giới hạn đó. Còn trong tin học, chúng ta cần có được kết quả cụ thể, cho nên chúng ta phải nhấn mạnh rằng tất cả các sự xấp xỉ đều tiến đến kết quả cụ thể sau một số lần lặp đi lặp lại nhất định. 13.4. Cú pháp của vòng lặp − Gồm những thành phần sau: − Điều kiện bất biến (invariant) của vòng lặp inv – đây là một xác nhận − Điều kiện thoát khỏi vòng lặp exit. − Điều kiện biến đổi (variant) của vòng lặp var – đây là một biểu thức nguyên. − Tập lệnh khởi tạo init, tập lệnh này luôn tạo ra một trạng thái thỏa inv và làm var không âm. − Tập lệnh body, tập lệnh này, khi khởi đầu một trạng thái mà inv được giữ và var không âm, sẽ bảo vệ điều kiện bất biến và làm điều kiện biến đổi giảm đi (nhưng vẫn bảo đảm không âm). Vì vậy, trong trạng thái kết quả, inv được thỏa và var có giá trị nhỏ hơn trước (nhưng luôn không âm). Tóm lại, vòng lặp có cú pháp như sau: Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 75 from init invariant inv variant var until exit loop body end Đây là phiên bản vòng lặp cho hàm maxarray: from i := t.lower; Result := t @ lower invariant -- Result là giá trị lớn nhất của t khi chỉ số t.lower = i. variant t.lower – i until i = t.upper loop i := i + 1 Result := Result.max (t @ i) end Dưới đây là một ví dụ khác về điều kiện bất biến, đây là hàm tính ước chung lớn nhất (greatest common divisor - gcd) của 2 số nguyên dương a, b bằng thuật toán Euclid. Phiên bản không có không có điều kiện bất biến và điều kiện biến đổi: Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 76 gcd (a, b: INTEGER): INTEGER is -- Uớc chung lớn nhất của a và b require a > 0; b > 0 local x, y: INTEGER do from x := a; y := b until x = y loop if x>y then x:=x–y else y:=y–x end end Result := x ensure -- Result là ước chung lớn nhất của a và b end Làm sao chắc chắn được rằng hàm gcd trả về đúng giá trị ước chung lớn nhất của a và b. Có một cách để kiểm tra điều này, lưu ý rằng thuộc tính này luôn đúng trong suốt quá trình lặp: x > 0; y > 0 -- Cặp x, y có cùng ước chung lớn nhất với cặp a, b Đây chính là điều kiện bất biến mà ta cần cho hàm này. Làm sao chúng ta biết vòng lặp này luôn luôn kết thúc? Chúng ta cần một điều kiện biến đổi để xác định điều này. Không thể chọn x làm điều kiện biến đổi vì ta không chắc rằng một bước lặp tuỳ ý sẽ làm giảm x, cũng vì lý do đó, y không thể được chọn. Nhưng ta chắc rằng hoặc x hoặc y sẽ giảm giá trị, vì vậy giá trị lớn nhất của chúng (được biểu diễn bằng hàm x.max(y)) là lựa chọn tốt nhất. Ta có phiên bản có điều kiện bất biến và điều kiện biến đổi của vòng lặp cho hàm gcd: Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 77 from x := a; y := b invariant x > 0; y > 0 -- Cặp có cùng UCLN với cặp variant x.max (y) until x = y loop if x > y then x := x – y else y := y – x end end Chương 14: Sử dụng những xác nhận Xem qua tất cả các cấu trúc có liên quan đến những xác nhận, ta thấy có 4 loại ứng dụng chính liên quan đến những xác nhận: − Trợ giúp cho việc viết phần mềm chính xác. − Trợ giúp việc viết tài liệu. − Hỗ trợ kiểm tra (testing), chạy từng bước (debugging) và đảm bảo chất lượng. − Hỗ trợ khả năng chịu lỗi của phần mềm. Chỉ có 2 ứng dụng cuối có khả năng kiểm tra những xác nhận lúc thực thi. 14.1. Những xác nhận như một công cụ để viết phần mềm chính xác Ứng dụng đầu tiên này hoàn toàn mang tính phương pháp và có vai trò quan trọng nhất. Điều này đã được làm rõ trong những phần trước: giải thích rõ ràng những yêu cầu chính xác trên mỗi thủ tục, những thuộc tính tổng quát của lớp đối Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 78 tượng và vòng lặp, giúp cho người lập trình có thể tạo ra những phần mềm chính xác ngay từ lần đầu tiên (khác với những cách tiếp cận khác, cố gắ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 ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ……………………………………………………………………………………… ………………………………………………………………………………………