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

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

Thêm vào BST

Báo xấu

75
lượt xem 5
download

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

Mô tả tài liệu

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# n0; x/=Void Lưu ý cách dùng dấu chấm phẩy (“;”). Ý nghĩa của dấu chấm phẩy ở đây tương đương với phép and. Dấu chấm phẩy có thể đặt giữa phần khai báo và chỉ thị. Khi những mệnh đề của xác nhận nằm trên những dòng khác nhau, ta không cần dùng dấu chấm phẩy (xem như có một phép and mặc định giữa các dòng liên tiếp). Những quy ước này giúp ta có thể nhận biết các thành phần riêng biệt của một...

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# - 3

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# n>0; x/=Void Lưu ý cách dùng dấu chấm phẩy (“;”). Ý nghĩa của dấu chấm phẩy ở đây tương đương với phép and. Dấu chấm phẩy có thể đặt giữa phần khai báo và chỉ thị. Khi những mệnh đề của xác nhận nằm trên những dòng khác nhau, ta không cần dùng dấu chấm phẩy (xem như có một phép and mặc định giữa các dòng liên tiếp). Những quy ước này giúp ta có thể nhận biết các thành phần riêng biệt của một xác nhận. Trong thực tế, ta thường dán nhãn (label) cho những thành phần này, ví dụ như: Positive: n>0 Not_void: x/=Void Các nhãn như trên có vai trò nhất định trong lúc thực thi xác nhận. Tuy nhiên, việc sử dụng chúng ở đây là nhằm làm cho văn bản của ta rõ ràng và tường minh hơn. Chương 6: Tiền điều kiện và hậu điều kiện Ứng dụng đầu tiên của xác nhận là đặc tả ngữ nghĩa của thủ tục. Một thủ tục không chỉ là một đoạn mã chương trình mà nó là cài đặt của một hàm nào đó từ đặc tả của một kiểu dữ liệu trừu tượng, nó sẽ thực hiện một công việc hữu ích. Việc biểu diễn công việc này một cách chính xác là vô cùng cần thiết. Ta có thể đặc tả công việc cần thực thi của một thủ tục bằng 2 xác nhận liên quan với nó là tiền điều kiện (preconditions) và hậu điều kiện (postconditions). Tiền điều kiện chỉ ra những thuộc tính cần được thoả mãn bất cứ khi nào thủ tục được gọi; còn hậu điều kiện chỉ ra những thuộc tính chắc chắn có sau khi thủ tục thực thi xong. 6.1. Lớp ngăn xếp Một ví dụ sẽ giúp ta làm quen với cách sử dụng các xác nhận: 25
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# class STACK [G] feature …Declaration of the features: count, empty, full, put, remove, item end Trước khi xem phần cài đặt, cần chú ý rằng những thủ tục được đặc trưng bởi những thuộc tính ngữ nghĩa mạnh mẽ và độc lập với cách biểu diễn nó. Ví dụ như: remove và item chỉ thực thi được khi có số phần tử lớn hơn 0. − put tăng số phần tử lên 1, remove giảm số phần tử đi 1. − Những thuộc tính như thế là một phần trong đặc tả của kiểu dữ liệu trừu tượng, ngay cả những người chưa bao giờ sử dụng đến kiểu dữ liệu trừu tượng cũng phải hiểu như vậy. Nhưng trong các cách tiếp cận thông thường của việc xây dựng phần mềm, những văn bản phần mềm thường không đề cập đến chúng. Thông qua những tiền điều kiện và hậu điều kiện của thủ tục, ta có thể đưa chúng vào những thành phần tường minh của phần mềm. Ta sẽ biểu diễn những tiền điều kiện và hậu điều kiện như là mệnh đề được giới thiệu qua hai từ khóa require và ensure. Lưu ý rằng những phần cài đặt của những thủ tục được chừa trống, ta sẽ tìm hiểu trong phần sau. indexing description: "Stacks: Cấu trúc dữ liệu với quy tắc truy xuất LIFO” class STACK1 [G] feature – Access count: INTEGER -- Số phần tử của Stack item: G is -- Phần tử trên cùng require not empty 26
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# do … end feature – Status report empty: BOOLEAN is -- Kiểm tra Stack rỗng? do ... end full: BOOLEAN is -- Kiểm tra Stack đầy? do … end feature -- Element change put (x: G) is -- Thêm phần tử x vào Stack. require not full do … ensure not empty item = x count = old count + 1 end remove is -- Xóa phần tử trên cùng của Stack. require not empty do … ensure not full 27
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# count = old count – 1 end end Cả 2 mệnh đề require và ensure đều là tùy chọn. Nếu có thì require phải nằm trước mệnh đề local. Những phần tiếp theo giải thích chi tiết hơn ý nghĩa của tiền điều kiện và hậu điều kiện. 6.2. Tiền điều kiện Tiền điều kiện biểu diễn những ràng buộc mà một thủ tục sẽ thực hiện một cách chính xác. Ví dụ như: put sẽ không được gọi nếu ngăn xếp đã đầy. − remove và item sẽ không thực hiện trên một ngăn xếp rỗng. − Tiền điều kiện vào có hiệu lực đến tất cả những lời gọi của thủ tục, cả trong lớp và từ những lớp liên quan. Một hệ thống chính xác sẽ không bao giờ thực thi một lời gọi không thỏa mãn tiền điều kiện. 6.3. Hậu điều kiện Hậu điều kiện biểu diễn những thuộc tính của trạng thái kết quả có được sau khi thực thi thủ tục. Ví dụ như: Sau thủ tục put, ngăn xếp sẽ không thể rỗng, phần tử trên cùng là phần − tử mới được thêm vào, và số lượng phần tử sẽ tăng lên 1. Sau thủ tục remove, ngăn xếp không thể đầy, số phần tử giảm đi 1. − Sự có mặt của mệnh đề hậu điều kiện trong thủ tục bảo đảm kết quả của thủ tục sẽ thoả mãn các thuộc tính (giả sử rằng thủ tục đã thỏa mãn tiền điều kiện để được gọi). Một từ khóa đặc biệt, old, xuất hiện trong hậu điều kiện. put và remove dùng từ khóa này để biểu diễn sự thay đổi của biến count. Cú pháp: old e, trong đó e là 28
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# một biểu thức, thường là một thuộc tính, biểu thị giá trị của e trong đầu vào của thủ tục. Hậu điều kiện của put có mệnh đề count = old count + 1 để thể hiện rằng put, khi được gọi bởi bất kỳ đối tượng nào, sẽ tăng giá trị biến count của đối tượng đó lên 1. Chương 7: Giao ước cho tính đáng tin cậy của phần mềm Định nghĩa tiền điều kiện và hậu điều kiện cho một thủ tục là một cách định nghĩa một hợp đồng (contract) giữa thủ tục và những lớp gọi nó. 7.1. Quyền lợi và nghĩa vụ Bằng cách kết hợp những mệnh đề require pre và ensure post trong thủ tục r, lớp đối tượng “tuyên bố” với những khách hàng của nó: Nếu các bạn hứa gọi r thỏa mãn pre, tôi hứa sẽ trả về kết quả thỏa mãn post Trong mối liên hệ giữa người và người hoặc giữa các công ty với nhau, hợp đồng là một văn bản làm cho những điều khoản của mối quan hệ trở nên trong sáng, rõ ràng. Thật đáng ngạc nhiên khi trong lĩnh vực phần mềm, nơi mà sự đúng đắn, rõ ràng có vai trò sống còn, ý tưởng hợp đồng này lại phải mất quá nhiều thời gian để thể hiện mình. Tiền điều kiện và hậu điều kiện mô tả một hợp đồng giữa thủ tục (đóng vai trò nhà cung cấp) và những đối tượng gọi đến nó (vai trò khách hàng). Đặc tính quan trọng nhất của hợp đồng trong công việc của con người là sự đòi hỏi về “nghĩa vụ” (obligation) và “quyền lợi” (right) cho cả 2 bên – thường là nghĩa vụ của bên này sẽ trở thành quyền lợi của bên kia. Điều này cũng đúng đối với hợp đồng giữa các lớp đối tượng: 29
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Tiền điều kiện ràng buộc khách hàng: nó định nghĩa những điều kiện − để một lời gọi đến thủ tục trở nên hợp pháp. Đây là nghĩa vụ của khách hàng và là quyền lợi của nhà cung cấp. Hậu điều kiện ràng buộc lớp đối tượng: nó định nghĩa những điều − kiện cần phải được đảm bảo bởi thủ tục khi trả về. Đây là quyền lợi của khách hàng và là nghĩa vụ của nhà cung cấp. 7.1.1. Những quyền lợi Đối với khách hàng, đó là sự đảm bảo những thuộc tính phải có được − sau khi gọi thủ tục. Đối với nhà cung cấp, đó là sự đảm bảo những tính chất phải được − thỏa mãn ở bất cứ nơi nào thủ tục được gọi. 7.1.2. Những nghĩa vụ Đối với khách hàng, đó là sự đáp ứng những yêu cầu được phát biểu − trong tiền điều kiện. Đối với nhà cung cấp, đó là những gì phải làm mà hậu điều kiện đã − định ra. Đây là hợp đồng cho thủ tục put của ví dụ trên: Nghĩa vụ Quyền lợi put Kết quả hậu điều kiện: Đáp ứng tiền điều kiện: Chỉ gọi Thông tin ngăn xếp được cập Khách hàng put(x) khi ngăn xếp chưa đầy. nhật: không rỗng, x nằm trên cùng, count tăng 1. Đáp ứng hậu điều kiện: Cập Kết quả tiền điều kiện: nhật thông tin ngăn xếp: không Nhà cung cấp Được bảo đảm là ngăn xếp rỗng, x nằm trên cùng, count chưa đầy khi put được gọi. tăng 1. 30
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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 Mặc dù bạn có thể chưa để ý, một trong những nguyên tắc của hợp đồng có xu hướng đi ngược lại những kiến thức tổng quát đã được công nhận trong ngành công nghiệp phần mềm; gặp nhiều sự phản ứng ngay từ đầu, nhưng Design by Contract đã là một trong số những đóng góp chính vào sự tin cậy của phần mềm và đạt được tầm quan trọng xứng đáng. Một quy tắc tương phản với sự quan sát đã nêu trên: tiền điều kiện là quyền lợi của nhà cung cấp và được biểu diễn ở góc dưới bên phải trong bảng trên: nếu phần khách hàng của hợp đồng không được thõa mãn, nói cách khác nếu lời gọi không đáp ứng tiền điều kiện, sau đó lớp đối tượng không được bao bọc bởi hậu điều kiện. Trong trường hợp này thủ tục có thể làm bất cứ chuyện gì: trả ra giá trị bất kỳ, lặp vô hạn, không trả về giá trị, thậm chí làm hỏng sự thực thi bằng một cách nào đó. Đây là trường hợp “khách hàng sai”. Lợi ích đầu tiên của thỏa thuận này là sự đơn giản hóa đáng kể phong cách lập trình. Tiền điều kiện được xem như những ràng buộc mà một lời gọi đến một thủ tục phải tuân theo, còn nếu bạn là người phát triển lớp đối tượng, bạn sẽ giả sử rằng những ràng buộc này được thỏa mãn khi viết những thủ tục; bạn sẽ không cần phải kiểm tra những ràng buộc đó trong thủ tục. Xét hàm căn bậc 2 như sau: sqrt (x: REAL): REAL is -- Căn bậc 2 của x require x >= 0 do … end Bạn sẽ chỉ viết thuật toán tính căn bậc 2 mà không cần quan tâm đến trường hợp x < 0, điều này đã được kiểm tra bởi tiền điều kiện và trở thành trách nhiệm của những khách hàng – những lớp sẽ gọi tới hàm này. Thực tế phương pháp của Design by Contract còn đi xa hơn nữa. Viết đoạn chương trình này vào sau do 31
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# if x < 0 then “Handle the error, somehow” else “Proceed with normal square root computation” end không chỉ là không cần thiết mà là không thể chấp nhận được. Điều này có thể biểu diễn như một nguyên tắc: Nguyên tắc không dư thừa Không được kiểm tra tiền điều kiện trong thân của thủ tục trong bất kỳ trường hợp nào Nguyên tắc này đã đi ngược với chủ trương của rất nhiều sách giáo khoa về công nghệ phần mềm hay phương pháp lập trình, thường được biết đến như là phương pháp lập trình phòng thủ - với ý tưởng: để thu được một phần mềm đáng tin cậy, bạn nên thiết kế mỗi thành phần của hệ thống sao cho nó có khả năng tự bảo vệ cao nhất. Thà dư còn hơn thiếu, một người không bao giờ là quá cẩn thận khi tiếp xúc với người lạ. Sự kiểm tra dư thừa có thể vô ích, nhưng ít nhất là nó không gây tác hại. Design By Contract đi theo một hướng ngược lại: những kiểm tra dư thừa có thể và thật sự gây ra tác hại. Điều này mới nghe có vẻ lạ, mọi người sẽ nghĩ rằng sự kiểm tra dư thừa có thể là vô ích, nhưng không thể nào gây ra tác hại. Tuy nhiên chỉ những người có sự hiểu biết chưa sâu về tính tin cậy của phần mềm và chỉ tập trung vào những phần riêng biệt của phần mềm mới có suy nghĩ như vậy. Nếu hạn chế tầm nhìn trong một phạm vi hẹp của một thành phần cụ thể, ví dụ như thủ tục sqrt ở trên, ta sẽ thấy rằng thủ tục có vẻ chặt chẽ hơn nếu có phần kiểm tra thêm trong thân thủ tục. Nhưng một hệ thống không chỉ giới hạn trong một thủ tục cụ thể mà nó bao gồm nhiều thủ tục trong nhiều lớp đối tượng khác nhau. Để đạt được một hệ thống 32
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# đáng tin cậy, ta phải từ bỏ cái nhìn hạn chế để có một tầm nhìn vĩ mô, bao hàm trên kiến trúc tổng thể. Nếu ta có được cái nhìn như thế thì tính đơn giản sẽ trở thành một tiêu chuẩn quyết định. Như ta đã nói từ đầu, sự phức tạp là kẻ thù chính của chất lượng. Khi quan tâm đến điều này, ta sẽ thấy rằng những kiểm tra dư thừa không còn là vô hại nữa. Thử hình dung một hệ thống thông thường, với hàng ngàn thủ tục, những kiểm tra dư thừa này sẽ trở thành một sự phức tạp không cần thiết khổng lồ. Nếu chúng ta bắt đầu bằng con đường này, có thể chắc chắn một điều là: không bao giờ đạt được một hệ thống đáng tin cậy. Với Design By Contract, bạn sẽ nhận ra những điều kiện chắc chắn và cần thiết để thực hiện các chức năng của một liên hiệp khách hàng – nhà cung cấp (hay gọi là một hợp đồng); và để cho rõ ràng, đối với mỗi điền kiện, cần xác định rõ trách nhiệm là của ai: khách hàng hay nhà cung cấp. Có thể có nhiều câu trả lời, theo một chừng mực nào đó, điều này là những phong cách thiết kế khác nhau. Nhưng một khi bạn đã quyết định thì bạn cần phải bám vào nó. Nếu bạn có yêu cầu về sự chính xác của tiền điều kiện, xác định rõ rằng yêu cầu là một phần trách nhiệm của khách hàng (những lời gọi đến thủ tục) thì không được kiểm tra trong thân của thủ tục; còn nếu yêu cầu này không nằm trong tiền điều kiện thì thủ tục cần phải kiểm tra nó. Đối với một hệ thống phần mềm, dù lớn hay nhỏ, chất lượng riêng của từng thành phần là chưa đủ. Cái giá trị nhất chính là sự bảo đảm rằng mỗi tương tác giữa hai thành phần bất kỳ đều phải có một sự phân công rõ ràng về quyền lợi và nghĩa vụ, tức là cần phải có một bản hợp đồng. 7.3. Những xác nhận không phải là một cơ chế kiểm tra đầu vào Để tránh hiểu lầm, lưu ý rằng những hợp đồng ta đang bàn là giữa một thủ tục (nhà cung cấp) và những thủ tục khác (khách hàng – những thủ tục gọi đến thủ tục đó). Chúng ta đang quan tâm đến mối quan hệ phần mềm – phần mềm, không 33
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# phải là phần mềm – con người hay phần mềm – ngoại cảnh. Vì vậy, tiền điều kiện sẽ không quan tâm đến sự đúng sai của dữ liệu người dùng nhập vào, ví dụ xét thủ tục read_positive_integer đòi hỏi người dùng nhập vào một số dương, một tiền điều kiện: require input > 0 không phải là một kỹ thuật đáng tin cậy. Trong trường hợp này không thể có sự thay thế cho một điều kiện if … then thông thường. Sự xác nhận không phải là một giải pháp kiểm tra sự đúng đắn của dữ liệu nhập. Tiêu chuẩn của Modular Protection (bảo vệ tính môđun cho phần mềm) khuyến khích rằng cần xác nhận tính hợp lệ của dữ liệu nhập từ các đối tượng ngoài hệ thống sao cho càng gần với mã nguồn càng tốt, có thể sử dụng “bộ lọc” nếu cần thiết: Hình 7-1: Sử dụng bộ lọc các module Để nhận dữ liệu từ ngoài hệ thống (đường màu xanh nhạt), bạn không thể dựa vào tiền điều kiện. Nhưng với những môđun màu vàng, dữ liệu phải thỏa mãn 34
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# tiền điều kiện mới có thể đi vào những môđun xử lý (màu xanh đậm). Vậy trong trường hợp này, ta chỉ có thể sử dụng xác nhận cho đường màu xanh đậm, thể hiện sự tương tác phần mềm – phần mềm. Và hậu điều kiện mà những môđun nhập nhận được sẽ phải phù hợp với tiền điều kiện của những thủ tục xử lý. Chương 8: Làm việc với những xác nhận Trong phần này chúng sẽ tìm hiểu chi tiết hơn về cách dùng tiền điều kiện và hậu điều kiện thông qua những ví dụ cơ bản. Những vấn đề đơn giản và phức tạp của xác nhận sẽ được minh họa rõ ràng qua những ví dụ dưới đây. 8.1. Lớp stack Lớp STACK được trang bị xác nhận có dạng chung như STACK1. Bây giờ, ta có thể nghĩ ra một phiên bản đầy đủ cùng với một cài đặt được giải thích rõ ràng. Để một lớp có thể sử dụng trực tiếp được, ta phải chọn một cài đặt. Hãy xem một cài đặt của ngăn xếp bằng cách dùng mảng. Hình 8-1: Stack được cài đặt bằng mảng Mảng được gọi là representation, có phạm vi từ 1 đến capacity. Thuộc tính count có kiểu số nguyên (integer) cho biết số phần tử trong ngăn xếp. 35
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Gọi a là một đối tượng của lớp này, phương thức a.put(x,i) gán giá trị x cho phần tử thứ i của stack; để lấy giá trị tại phần tử thứ i, ta dùng phương thức a.item(i) hoặc a @ i. Lưu ý rằng phạm vi của mảng là từ 1 đến capacity, vì vậy i phải nằm giữa 1 và capacity. 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 STACK2 [G] creation make feature -- Initialization make (n: INTEGER) is --Cấp phát cho Stack độ lớn n phần tử require positive_capacity: n >= 0 do capacity := n !! representation . make (1, capacity) ensure capacity_set: capacity = n array_allocated: representation /= Void stack_empty: empty end feature -- Access 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 36