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

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