Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
61
trong giới hạn cho phép. Điều kiện bất biến biểu diễn mối quan hệ giữa count,
lower và upper; nó cho phép count được cài đặt như một hàm chứ không phải
một thuộc tính.
indexing
description: "Mảng giá trị cùng kiểu, truy xuất các phần
tử thông qua các chỉ số mảng"
class ARRAY [G] creation
make
feature Khởi tạo
make (minindex, maxindex: INTEGER) is
Xác định 2 biên của mảng với minidex và
maxindex
Mảng rỗng nếu minindex > maxindex.
require
meaningful_bounds: maxindex >=
minindex - 1
do
…
ensure
exact_bounds_if_non_empty: (maxindex >=
minindex) implies

index_not_too_small: lower <= i
index_not_too_large: i <= upper
do
…
ensure
element_replaced: item (i) = v
end
invariant
consistent_count: count = upper – lower + 1
non_negative_count: count >= 0
end class ARRAY

Phần trống duy nhất còn lại là phần cài đặt của thân những thường trình
item và put. Chương 11: Kết nối với kiểu dữ liệu trừu tượng
Trong phần này, ta sẽ củng cố thêm khái niệm “xác nhận” bằng việc tìm hiểu
về sự kết nối giữa các xác nhận và những thành phần của một đặc tả của một kiểu
dữ liệu trừu tượng (ADT – Abstract Data Type).
Một ADT được tạo bởi 4 thành phần:
− Tên kiểu, có thể cùng với những tham số chung (phần TYPES)
hiểu mối liên hệ giữa những đặc tính của lớp và phần tương ứng của ADT – những
hàm của ADT. Những hàm này gồm 3 loại: creator, query và command. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
64
Sự phân loại của một hàm f: A × B × …
Æ
X phụ thuộc vào vị trí xuất hiện
của ADT (A, B, …, X) so với mũi tên , gọi là T .
Nếu T chỉ xuất hiện ở bên phải của mũi tên thì f là hàm creator. Trong lớp
đối tượng, nó là phương thức khởi tạo. Ví dụ: hàm new
Nếu T chỉ có mặt ở bên trái của mũi tên thì f là hàm query. Trong lớp đối
tượng, nó là những phương thức truy xuất đến nhữ
ng thuộc tính của các thể hiện
của một lớp. Ví dụ: hàm item và empty.
Nếu T xuất hiện ở cả 2 bên mũi tên thì f là hàm command. Những hàm này
tạo ra những đối tượng mới từ những đối tượng đã có. Trong lớp đối tượng, những
hàm này thường được biểu diễn như một phương thức để làm thay đổi một đối
tượng hơn là tạo ra một đối tượng mới. Ví dụ hàm put và remove.

11.2. Biểu diễn những tiên đề
Từ sự tương ứng giữa những hàm ADT và những đặc tính của lớp, ta có thể
suy ra sự tương ứng giữa ngữ nghĩa thuộc tính ADT và những xác nhận.

hiện của lớp), sự trừu tượng hoá này sẽ sinh ta một đối tượng trừu tượng (thể hiện
của ADT). Những hàm trừu tượng này thường là từng phần. Sự tương ứng giữa lớp và ADT
(cf ; a) = (a ; af) Trong đó dấu “;” là toán tử kết hợp giữa các hàm. Nói cách khác, nếu ta có
hai hàm f và g thì f;g là hàm h sao cho h(x) = g(f(x)) với mọi x (f;g còn được viết
dưới dạng g o f ) Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
66
Hai đường đứt khúc cùng chỉ đến đối tượng trừu tượng ABST_2. Kết quả
vẫn như nhau ngay cả khi bạn:
- Áp dụng sự biến đối cụ thể cf, sau đó trừu tượng hóa kết quả, sinh ra
a(cf(CONC_1)).
- Trừu tượng hóa trước, sau đó áp dụng sự biến đổi trừu tượng af, sinh ra
af(a(CONC_1)).

11.4. Cài đặt những điều kiện bất biến
Một số xác nhận xuất hiện trong những điều kiện bất biến nhưng chúng lại Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
67
hơn hoặc bằng count, và những phần tử có chỉ số vượt quá count có thể có giá trị
tùy ý.
Quan hệ cài đặt thường không phải là một hàm, nhưng sự nghịch đảo của nó
(mũi tên hướng lên) là một hàm thật sự vì mỗi đối tượng cụ thể biểu diễn cho nhiều
nhất một đối tượng trừu tượng. Trong ví dụ về lớp STACK của chúng ta, mỗi cặp
<representation,count> hợp lệ chỉ biểu diễn cho một STACK trừu tượng. Hình 11-2: Hai cài đặt của cùng một đối tượng trừu tượng

Cả hai stack cụ thể trên đây đều là cài đặt (implementation) của stack trừu
tượng bao gồm 3 phần tử 342, -133 và 5. Việc a là một hàm là một yêu cầu chung:
nếu một đối tượng cụ thể là cài đặt của nhiều đối tượng trừu tượng, đại diện được
chọn sẽ trở nên mơ hồ và không thích hợp. Vì vậy mũi tên a nên vẽ theo chiều như
trên để
mô tả cho sự kết nối giữa kiểu cụ thể và trừu tượng.
end
Khi chương trình thực thi thì những xác nhận assertion_clause
X
sẽ
được bảo đảm.
Đây là cách để chắc chắn một lần nữa rằng những thuộc tính nhất định được
thỏa mãn, và quan trọng hơn, nó giúp những người đọc phần mềm hiểu được những
giả thuyết mà ta dựa vào. Việc viết phần mềm đòi hỏi sự xác nhận thường xuyên
những thuộc tính của đối tượng. Xét ví dụ về hàm sqrt(x), bấ
t cứ hàm nào gọi Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
69
đến sqrt(x) đều dựa vào xác nhận rằng x không âm. Xác nhận này có thể hiển
hiện trong ngữ cảnh, ví dụ như một câu lệnh if then
if x >= 0 then y := sqrt (x) end
nhưng nó cũng có thể không trực tiếp như trên, ví dụ như x đã được gán
trước đó:
x := a^2 + b^2
Chỉ thị check sẽ giúp biểu diễn xác nhận đó nếu nó không hiển hiện trong
câu lệnh

x := a ^2 + b^2
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
70
if full then
error := Overflow
else
check representation /= Void end
representation.put (x); error := 0
end
Ở đây người đọc sẽ nghĩ rằng không an toàn khi gọi
representation.put(x); như vậy, bởi vì không có một sự kiểm tra nào trước
đó về sự không rỗng của
representation. Nhưng nếu để ý kỹ, bạn sẽ thấy rằng
nếu
full sai thì capacity phải là số dương. Vì vậy, representation không
thể là rỗng. Đây là một điều rất quan trọng và sẽ là một phần trong cài đặt các ràng
buộc của lớp. Trong thực tế, với cài đặt đầy đủ của một ràng buộc được định trước,
ta nên viết chỉ thị check như sau:
check
representation_exists: representation /= Void
Because of clause
representation_exists_if_not_full of the
cài đặt điều kiện bất biến.
end
Trong những sự tiếp cận thông thường của việc xây dựng phần mềm, mặc dù
những lời gọi hàm và những phương thức khác thường tin tưởng vào sự đúng đắn
của chúng nhờ những xác nhận khác nhau, nhưng chúng vẫn là những xác nhận
không tường minh. Lập trình viên sẽ tự thuyết phục mình rằng một thuộc tính luôn
luôn được giữ ở một thời điểm nào đó, và đưa phân tích này vào trong mã ngu

13.2. Những vòng lặp đúng
Việc sử dụng khôn ngoan xác nhận sẽ giúp ta giải quyết những vấn đề này.
Một vòng lặp có thể có một xác nhận liên kết, gọi là vòng lặp có điều kiện bất biến
(loop invariant). Cũng có khái niệm “loop variant (vòng lặp có điều kiện biến đổi)”.
Đây không phải là một xác nhận mà là một biểu thức nguyên. Hai khái niệm này sẽ
giúp ta bảo đảm sự chính xác của vòng lặp.
Xét ví dụ tính giá trị
lớn nhất của một mảng số nguyên:
maxarray (t: ARRAY [INTEGER]): INTEGER is
Giá trị lớn nhất của mảng t
require
t.capacity >= 1
local
i: INTEGER
do
from
i := t.lower Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
72
Result := t @ lower
until i = t.upper loop
i := i + 1