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

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#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...
Nội dung trích xuất từ tài liệu:
TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 5Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#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ínhvà 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ộctí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ảnngâ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ếncủ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ềngử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ủalớ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 trongphầ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 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# consistent_with_array_size: capacity = representation.capacity empty_if_no_elements: empty = (count = 0) item_at_top: (count > 0) implies (representation item (count) = item) end Một điều kiện bất biến của lớp C là một bộ những xác nhận mà mỗi thể hiệncủa C sẽ thoả mãn tất cả những thời điểm bền vững (stable times). Những thời điểmbền vững là những thời điểm mà tại đây, thể hiện của lớp trong tình trạng có thểquan sát được: + Khi khởi tạo thể hiện, tức là sau khi thực thi !!a hoặc là !!a.make(…), acó kiểu là lớp C. + Trước và sau mỗi khi yêu cầu một thủ tục r của lớp thông qua lời gọia.r(…). Hình vẽ sau sẽ chỉ ra thời gian tồn tại của một đối tượng Hình 9-1: Thời gian tồn tại của một đối tượng 50Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Vào lúc bắt đầu, tức là bên trái hình Hình 8-1, đối tượng không tồn tại. Đốitượng được sinh ra bởi câu lệnh !!a hay !!a.make(…) hoặc là do một clone.Sau đó, client sử dụng đối tượng thông qua các tham chiếu đến a có dạng a.f(…)với f là một tính năng của lớp sinh ra đối tượng. Và từ đó, đối tượng tồn tại ít nhấtlà cho đến khi việc thi hành kết thúc. Điều kiện bất biến là một thuộc tính đặc thù của những trạng thái được biểudiễn bởi những ô vuông màu xám trong hình Hình 8-1 (Ví dụ: S1). Những thờiđiểm bền vững (stable times) trong hình trên là những chỗ mà đối tượng có thể thấyđược từ bên ngoài, nghĩa là client có thể áp dụng một tính năng nào đó cho nó, baogồm: + Trạng thái kết quả của việc tạo một đối tượng (trong hình là S1). + Những trạng thái ngay trước và sau khi client thực hiện một lời gọi có dạnga.some_routine(…). 9.3. Điều kiện bất biến thay đổi Tuy có tên là điều kiện bất biến nhưng nó cũng không cần phải thoả mãn hếttại mọi thời điểm mặc dù trong ví dụ STACK4, nó vẫn đúng sau khi được khởi tạo.Trong những trường hợp tổng quát hơn, việc một thủ tục g vào lúc ban đầu vì cốthực hiện những mục đích của mình - tức là cố đạt được hậu điều kiện – mà có thểlàm hủy đi điều kiện bất biến trong quá trình này (cũng như con người, việc cố gắnglàm một cái gì đó hữu ích có thể phá vỡ trật tự đã được thiết lập của mọi thứ);nhưng sau đó, ở giai đoạn thực thi tiếp theo, thủ tục này không vi phạm quá nhiềuđiều kiện bất biến vốn có là hoàn toàn được chấp nhận. Trong vài tình trạng tứcthời, ví dụ như trong những tình trạng được đánh dấu trên hình Hình 8-1, điềukiện bất biến sẽ không thể giữ được. Tuy nhiên, điều này vẫn có thể chấp nhận đượcmiễn là thủ tục sẽ thiết lập lại điều kiện bất biến trước khi kết thúc việc thực thi củanó. 51Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 9.4. Ai phải bảo quản điều kiện bất biến? Những lời gọi đủ điều kiện, có dạng là a.f(…), thực hiện nhân danh chomột client, là những cái duy nhất luôn phải được bắt đầu và rời khỏi trong trạng tháithoả mãn điều kiện bất biến; không có quy định nào cho những lời gọi không đủđiều kiện có dạng f(…) thực thi tr ...