TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 7

Chia sẻ: Cao Tt | Ngày: | Loại File: PDF | Số trang:12

Thêm vào BST

Báo xấu

107
lượt xem 4
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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,...

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 7

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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ử đó. 73
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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: 74
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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: 75
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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: 76
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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 77
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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 78
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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 79
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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. 81
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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 − 82
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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 Yêu cầu đối Void SetData([NotNull] Object tượng nhập vào obj) {} NotNull hay trả về phải //obj != null “not null” Yêu cầu đối Void SetData([Equal (5)] int Equal 83
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# tượng nhập vào value) {} hoặc trả về phải //value == 5 “equal” với một giá trị cho trước Yêu cầu đối tượng nhập vào Void SetData([ExclusiveBetween hoặc trả về phải (1, 5)] int value) {} ExclusiveBetween nẳm trong một //1 = 5 trị cho trước Yêu cầu đối tượng nhập vào Void SetData([Is (typeof hoặc trả về phải (HOCSINH))] Object obj) {} Is “Is” một giá trị //kiểu của obj phải là HOCSINH cho trước Yêu cầu đối Void SetData([LessThan (5)] int tượng nhập vào value) {} LessThan hoặc trả về phải //value < 5 84