CHƯƠNG 2. Giới thiệu về Design by Contract

CHƯƠNG 2.

Giới thiệu về Design by Contract

1. 
   
   
2. 
   
   
   1. 
      Giới thiệu
      

Một phần chính trong chất lượng sản phẩm là tính đúng đắn, tính tin cậy của phần mềm: đó là khả năng của một hệ thống có thể thực hiện các công việc của mình theo các đặc tả có sẵn và có thể xử lý được các tình huống bất thường. Nói một cách đơn giản, tính tin cậy tức là không có lỗi.

Có nhiều cách xây dựng nên tính tin cậy cho phần mềm. Chúng ta có thể sử dụng lại các phương thức có sẵn. Có nghĩa là dùng lại những thành phần của các phần mềm thông dụng mà đúng đắn, nó làm cho phần mềm mà chúng ta xây dựng đạt được tính tin cậy hơn là xây dựng mới các phần mềm. Một cách khác, việc bẫy những mâu thuẫn của chương trình trước khi chúng trở thành lỗi cũng góp phần củng cố thêm tính đúng đắn của phần mềm. Hoặc là “kỹ thuật thu gom rác” – kỹ thuật thu gọn các mảnh vụn bộ nhỡ không còn được sử dụng nữa – cũng làm cho phần mềm được tin cậy hơn.

Nhưng như thế vẫn chưa đủ, để chắc chắn rằng phần mềm hướng đối tượng sẽ thi hành một cách đúng đắn, chúng ta vẫn cần một hệ thống các phương pháp để xác định và triển khai các thành phần của phần mềm hướng đối tượng và các mối quan hệ của chúng trong hệ thống phần mềm. Một phương pháp mới mẻ đã xuất hiện, nó được gọi là “Design by Contract”, được tạm dịch là “Thiết kế theo hợp đồng”. Theo thuyết Design by Contract, một hệ thống phần mềm được xem như là tập hợp các thành phần có các giao tiếp tương tác với nhau dựa trên định nghĩa chính xác của các giao ước trong hợp đồng.

Lợi ích của “Design by Contract” bao gồm:

• 
  Giúp cho việc hiểu biết rõ hơn về các phương pháp hướng đối tượng và tổng quát hơn là của cấu trúc của phần mềm.
  
• 
  Tiếp cận một cách có hệ thống đến việc xây dựng hệ thống hướng đối tượng có ít hoặc hoàn toàn không có lỗi.
  
• 
  Xây dựng được các framework hiệu quả hơn cho việc gỡ lỗi, kiểm thử.
  
• 
  Dễ dàng viết tài liệu cho phần mềm.
  
• 
  Hiểu và kiểm soát được kỹ thuật thừa kế.
  
• 
  Một kỹ thuật cho mối quan hệ với các trường hợp dị thường, dẫn đến sự an toàn và hiệu quả cho việc xây dựng các ngôn ngữ xử lý các trường hợp ngoại lệ.
  

2. 
   Khái niệm về hợp đồng
   

Một ví dụ đơn giản sau đây minh họa cho một hợp đồng giữa một hãng hàng không và khách hàng.

Bảng 1: Hợp đồng giữa một hãng hàng không và khành hàng

Cùng chung một ý tưởng áp dụng cho phần mềm. Xem xét một yếu tố phần mềm E. Để đạt được mục đích (thực hiện hợp đồng riêng của mình). E sử dụng một chiến lược nhất định, bao gồm những công việc con t₁, t₂,…, t_n. Nếu một công việc con t_i nào đó bất thường, nó sẽ được thực hiện bằng cách gọi một thủ tục R. Nói cách khác, E hợp đồng ra công việc con cho R. Tình trạng như vậy cần phải được quản lý bằng bảng phân công nghĩa vụ và lợi ích một cách rõ ràng.

Ví dụ như t_i là công việc chèn một từ vào từ điển (một bảng mà mỗi phần tử được xác định bởi một chuỗi ký tự sử dụng như là một khóa). Hợp đồng sẽ là:

Bảng 2: Hợp đồng chèn một từ vào từ điển

3. 
   Tiền điều kiện, hậu điều kiện và tính bất biến
   
   1. 
      Tiền điều kiện và hậu điều kiện.
      

Tiền điều kiện mô tả sự ràng buộc mà với sự ràng buộc này, phương thức sẽ thực hiện một cách đúng đắn. Đó là nghĩa vụ của bên thực hiện và là quyền lợi của bên cung cấp.

Hậu điều kiện diễn tả các thuộc tính từ kết quả thực hiện một phương thức. Đó là nghĩa vụ của bên cung cấp và là quyền lợi của bên thực hiện

Ví dụ một hành động xóa bản ghi từ tập hợp cần có tiền điều kiện yêu cầu bản ghi với khóa chính phải tồn tại và hậu điều kiện yêu cầu bản ghi đó không được nhiều hơn các yếu tố trong tập hợp đó

2. 
   Tính bất biến
   

Điều kiện bất biến của lớp mô tả các ràng buộc toàn vẹn của lớp. Khái niệm này quan trọng cho việc quản lý cấu hình và kiếm thử hồi quy vì nó mô tả xâu hơn đặc tính của một lớp. Điều kiện bất biến của lớp được thêm vào với tiền điều kiện và hậu điều kiện của mỗi phương thức của lớp:

4. 
   Design By Contract trong Eiffel
   

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. 
   Biểu diễn Design by Contract trong Eiffel
   

• 
  Precondition: Được thể hiện bằng từ khóa require
  

Cần phải thỏa mãn biểu thức lô-gic boolean expressions trong mệnh đề require trước mới có thể thực hiện tiếp thủ tục r ở sau đó.

• 
  Postcondition: Được thể hiện bằng từ khóa ensure
  

Sau khi thực hiện thủ tục r, kết quả trả về phải thỏa mãn biểu thức lô-gic boolean expressions trong mệnh đề ensure

• 
  Class invariant: Được thể hiện bằng từ khóa invariant
  

Trong suốt quá trình thực hiện thủ tục r cần phải thỏa mãn biểu thức lô-gic boolean expressions trong mệnh đề invariant

• 
  Chỉ thị Check: Được thể hiện bằng cặp từ khóa check…end
  

…

assertion_clause_n

• 
  Loop invariant, loop variant
  

2. 
   Ví dụ minh họa
   

… Thuật toàn chèn…

Mệnh đề requie giới thiệu về điều kiện input, hoặc là tiền điều kiện; mệnh đề ensure giới thiệu về điều kiện output hay còn gọi là hậu điều kiện. Cả hai điều kiện là ví dụ về sự xác nhận, hoặc điều kiện logic (mệnh đề hợp đồng) liên kết với thành phần của phần mềm. Trong tiền điều kiện, biến count là số phần tử hiện thời và capacity là số lượng lớn nhất có thể đưa vào; trong hậu điều kiện, has là hàm boolean để xem từ đó có không, và item trả lại từ liên kết với khóa. Kí hiệu old count là giá trị count cũ.

Một ví dụ khác về cơ chế gửi tin.

send (m: MESSAGE)is

-- Gửi một tin nhắn m theo chế độ gửi nhanh nếu có thể, nếu không sẽ chuyển sang chế độ gửi chậm.

local

tried_fast, tried_slow:BOOLEAN

do

if tried_fast then

tried_slow := True

send_slow (m)

else

tried_fast := True

send_fast (m)

end

rescue

if not tried_slow then

retry

end

end

Trong ví dụ này các giá trị logic ban đầu sẽ được khởi tạo là False. Nếu send_fast không thành công, phần thân của mệnh đề do sẽ được thực hiện lại. Còn nếu việc thực thi send_slow không thành công, mệnh đề rescue sẽ được thự hiện.