TRƯỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN
KHOA CÔNG NGHỆ THÔNG TIN
BỘ MÔN CÔNG NGHỆ PHẦN MỀM
LÊ TRẦN HOÀNG NGUYÊN – 0112103
NGUYỄN BÁCH KHOA - 0112140
TÌM HIỂU CÔNG NGHỆ
DESIGN BY CONTRACT VÀ XÂY DỰNG
CÔNG CỤ HỖ TRỢ CHO C#

KHÓA LUẬN CỬ NHÂN TIN HỌC GIÁO VIÊN HƯỚNG DẪN
Th.s: NGUYỄN ĐÔNG HÀ
Tháng 7, 2005. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
3
MỤC LỤC

LỜI NÓI ĐẦU 7

TỔNG QUAN 8

Chương 1:

Giới thiệu về Eiffel 9

1.1.

Giới thiệu 9

1.2.

Design By Contract trong Eiffel 10

1.3.


Chương 5:

Giới thiệu về sự xác nhận trong văn bản của phần mềm 24

Chương 6:

Tiền điều kiện và hậu điều kiện 25

6.1.

Lớp ngăn xếp 25

6.2.

Tiền điều kiện 28

6.3.

Hậu điều kiện 28

Chương 7:

Giao ước cho tính đáng tin cậy của phần mềm 29

7.1.

Quyền lợi và nghĩa vụ 29

7.1.1.

8.1.

Lớp stack 35

8.2.

Mệnh lệnh và yêu cầu 38

8.3.

Lưu ý về những cấu trúc rỗng 41

8.4.

Thiết kế tiền điều kiện: tolerant hay demanding? 42

8.5.

Một môđun tolerant 43

Chương 9:

Những điều kiện bất biến của lớp 47

9.1.

Định nghĩa và ví dụ 48

9.2.



10.3.

Xem lại về mảng 60

Chương 11:

Kết nối với kiểu dữ liệu trừu tượng 62

11.1.

So sánh đặc tính của lớp với những hàm ADT 63

11.2.

Biểu diễn những tiên đề 64

11.3.

Hàm trừu tượng 65

11.4.

Cài đặt những điều kiện bất biến 66

Chương 12:

Một chỉ thị xác nhận 68

Chương 13:


Sử dụng những xác nhận 77

14.1.

Những xác nhận như một công cụ để viết phần mềm chính xác 77

14.2.

Sử dụng những xác nhận cho việc viết tài liệu: thể rút gọn của một lớp
đối tượng 78

Chương 15:

Giới thiệu công cụ XC# 81

15.1.

Giới thiệu 81

15.2.

XC# hoạt động như thế nào 82

15.3.

Khai báo các xác nhận 82

15.3.1.


16.2.2.

Chi tiết các lớp đối tượng 95

16.2.2.1

Màn hình Configuration 95

16.2.2.2

Lớp Connect 98

16.2.2.3

Lớp ProjectInfo 99

16.2.2.4

Lớp ClassInfo 101

16.2.2.5

Lớp FunctionInfo 104

16.2.2.6

Lớp Assertion 106

16.2.2.7



Hình 1-5: Code gây ra lỗi ở hậu điều kiện ----------------------------------------------- 15

Hình 1-6: Thông báo khi lỗi xảy ra ở điều kiện bất biến------------------------------- 16

Hình 1-7: Code gây ra lỗi ở điều kiện bất biến ------------------------------------------ 16

Hình 7-1: Sử dụng bộ lọc các module ---------------------------------------------------- 34

Hình 8-1: Stack được cài đặt bằng mảng ------------------------------------------------- 35

Hình 9-1: Thời gian tồn tại của một đối tượng ------------------------------------------ 50

Hình 10-1: Thời gian tồn tại của một đối tượng----------------------------------------- 58

Hình 11-1: Sự biến đổi giữa những đối tượng trừu tượng và cụ thể------------------ 65

Hình 11-2: Hai cài đặt của cùng một đối tượng trừu tượng---------------------------- 67

Hình 13-1: Một vòng lặp tính toán -------------------------------------------------------- 73

Hình 16-1: Sơ đồ thiết kế tổng thể -------------------------------------------------------- 94

Hình 16-2: Màn hình Configuration ------------------------------------------------------ 95

Hình 16-3: Chi tiết màn hình Configuration --------------------------------------------- 96

Hình 16-4: Lớp Connect -------------------------------------------------------------------- 98

Hình 16-5: Lớp ProjectInfo ---------------------------------------------------------------- 99

cậy và rõ ràng bao nhiêu thì công việc nâng cấ
p và phát triển nó càng dễ dàng bấy
nhiêu. Do đó, có thể nói, một trong những tiêu chí của ngành công nghệ phần mềm
mà bất kỳ thời đại nào, bất kỳ sản phẩm phần mềm nào cũng đều hướng đến là tính
đáng tin cậy và đúng đắn. Xuất phát từ nhu cầu ấy, công nghệ Design By Contract
đã ra đời nhằm giúp đảm bảo cho tính đáng tin cậy của phần mềm. Đó cũng chính là
lý do mà chúng em đã chọn đề
tài này.
Với mục đích tìm hiểu công nghệ Design By Contract một cách khá kỹ
lưỡng, chúng em đã tiếp cận nó bằng các tài liệu lý thuyết cũng như qua các công cụ
có khả năng hỗ trợ Design By Contract cho các ngôn ngữ lập trình hiện đại. Không
dừng ở đó, chúng em còn xây dựng một công cụ hỗ trợ công nghệ này cho C# với
tên gọi là DCS (Design By Contract for C Sharp).
Đối tượng và phạm vi nghiên cứu: ý tưởng chính của Design By Contract là
lập một “hợp đồng” gi
ữa một lớp đối tượng (supplier) và những khách hàng (client)
của nó, tức là những lớp đối tượng khác gọi đến các phương thức của lớp này.
Những client này phải bảo đảm một số điều kiện nhất định khi gọi một phương thức
của một supplier gọi là tiền điều kiện (precondition); đáp lại, sau khi thực thi thủ
tục, supplier phải đáp ứng mộ
t số điều kiện tương ứng gọi là hậu điều kiện
(postcondition). Những điều kiện của hợp đồng sẽ được kiểm tra bởi trình biên dịch,
và bất cứ sự vi phạm nào của phần mềm cũng sẽ được phát hiện.


9
Chương 1: Giới thiệu về Eiffel
1.1. Giới thiệu
Đầu tiên, chúng ta sẽ làm quen với phần mềm Eiffel trước khi tìm hiểu về
công nghệ Design By Contract. Vì sao lại như vậy? Vì tất cả ví dụ dùng trong luận
văn đều sử dụng cấu trúc của ngôn ngữ Eiffel. Còn những khái niệm nào mới được
đề cập trong chương này sẽ được giải thích kỹ hơn trong các phần sau khi giới thiệu
về Design By Contract
Qua hơn 10 năm tồn tại, Eiffel hiện nay được coi là một trong những môi
trường phát tri
ển phần mềm tốt nhất. Trước sức mạnh to lớn của Eiffel trong lĩnh
vực phần mềm thì dù muốn dù không, bạn cũng nên biết qua về nó. Vậy thực chất
Eiffel là gì?
Eiffel là khung làm việc trợ giúp cho việc suy nghĩ, thiết kế và thực thi phần
mềm hướng đối tượng.
Eiffel là một phương pháp, một ngôn ngữ hỗ trợ mô tả một cách hiệu quả và
phát triển những hệ thố
ng có chất lượng.
Eiffel là ngôn ngữ thiết kế
Vai trò của Eiffel còn hơn một ngôn ngữ lập trình. Những gì nó đem lại
không chỉ giới hạn trong ngữ cảnh lập trình mà trải rộng khắp công việc phát triển
phần mềm: phân tích, lên mô hình, viết đặc tả, thiết kế kiến trúc, thực hiện, bảo trì,
làm tài liệu.
Eiffel là một phương pháp.
Eiffel dẫn đường các nhà phân tích và những nhà phát triển xuyên suốt tiến
trình xây dựng một ph
ần mềm.
Phương pháp Eiffel tập trung cả về yếu tố sản phẩm và chất lượng, với
những điểm nhấn: tính đáng tin cậy, tính tái sử dụng, tính mở rộng, tính khả dụng,
tính bền vững.

phân tích mã nguồn định lượng.
Tùy vào nhu cầu của mình, bạn có thể sử dụng EiffelStudio như một môi
trường lập trình hoặc chỉ như một công cụ giúp mô hình hóa, xây dựng các mô tả hệ
thống bao gồm các lớp trừu tượng mà không thực thi bằng công cụ Diagram hoặc
kết h
ợp cả 2 khả năng để đạt đến hiệu quả cao nhất. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
11
1.3.1. Giao diện Hình

1-1: Giao diện EiffelStudio

Giao diện làm việc của EiffelStudio có 4 khung chính: Features, Class,
Clusters, Context. Để thuận tiện cho việc lập trình, các bạn có thể đóng bớt các
khung cửa sổ đi. Tất cả các khung cửa sổ này đều có thể đóng lại ngọai trừ Class.

1.3.2. Các thao tác căn bản trên EiffelStudio
Khởi động chương trình: Programs --> EiffelStudio Version --> EiffelStudio
Chọn "Create a new project" > OK.

assertion_clause
1

assertion_clause
2

…
assertion_clause
n

end

Loop invariant, loop variant:
from
initialization

until
exit

invariant
inv

variant


TH1: Lỗi xảy ra ở tiền điều kiện

Sửa n:=8 thành n:=-8.
Tại dòng if (n >= 0) then nhấn tổ hợp phím Ctrl-K.
Tại dòng end --end if , nhấn tổ hợp phím Ctrl-K.
Recompile (Shift-F7) và cho chạy lại chương trình (F5). Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
14

Xuất hiện thông báo ngoại lệ sau:

Hình

1-2: Thông báo khi lỗi xảy ra ở tiền điều kiện

và con trỏ dừng lại ở câu lệnh Hình

1-3:


Xuất hiện thông báo ngoại lệ sau:

Hình

1-4: Thông báo khi lỗi xảy ra ở hậu điều kiện

và con trỏ dừng lại ở câu lệnh Hình

1-5: Code gây ra lỗi ở hậu điều kiện
Nguyên nhân:
Trước đó, ta gán capacity := n-1, hậu điều kiện lại yêu cầu capacity = n.

TH3: Lỗi xảy ra ở điều kiện bất biến.

Trong lớp TEST_CLASS, tại thủ tục make, thêm vào dòng sau:
count:=-1 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
16
Chọn menu Project > Project Setting… Bỏ dấu check ở ensure. Đánh dấu
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
17
Chương 2: Một số cơ chế mang lại tính đáng tin cậy
cho phần mềm
Trước hết, phải nói rằng kỹ thuật định nghĩa thuộc tính của một đối tượng
gần như là có liên quan với cấu trúc của những hệ thống phần mềm. Những kiến
trúc đơn giản, riêng biệt và có khả năng mở rộng sẽ giúp chúng ta đảm bảo tính
đáng tin cậy của phần mềm dễ dàng hơn so với những cấu trúc vặn vẹo. Đặc biệt, c
ố
gắng giới hạn sự liên quan giữa các môđun với nhau đến mức tối thiểu nhất sẽ là
tiêu điểm cho việc thảo luận về tính riêng biệt. Điều này giúp ngăn chặn những rủi
ro thông thường của tính đáng tin cậy, ví dụ như những biến toàn cục và việc định
nghĩa những cơ chế liên lạc bị giới hạn, client và những mối quan hệ
kế thừa. Nói
đến chất lượng phần mềm thì không thể bỏ qua tính đáng tin cậy. Chúng ta cố gắng
giữ cho những cấu trúc càng đơn giản càng tốt. Tuy rằng điều này vẫn chưa đủ đảm
bảo cho tính đáng tin cậy của phần mềm, nhưng dù sao, nó cũng là một điều kiện
cần thiết.
Một điều kiện khác cũng cần thiết nữa là làm cho ph
ần mềm của chúng ta tối
ưu và dễ đọc. Văn bản phần mềm không những được viết một lần mà nó còn phải
được đọc đi đọc lại và viết đi viết lại nhiều lần. Sự trong sáng và tính đơn giản của
các câu chú thích là những yêu cầu cơ bản để nâng cao tính đáng tin cậy của phần
mềm.
Một vũ khí khác cũng rất cần thiết là việc qu
ản lý bộ nhớ một cách tự động,
đặc biệt là bộ thu gom rác (garbage collection). Bất kỳ hệ thống nào có khởi tạo và
thao tác với cấu trúc dữ liệu động mà lại thực hiện thu hồi bộ nhớ bằng tay (tức là

Có những chú thích giống nhau cũng chẳng sao, dĩ nhiên, khi đó ta không để
ý đến kích thước của chương trình. Ví dụ, câu lệnh
x := y+1
không đúng cũng
không sai. Vì đúng hay sai chỉ có ý nghĩa khi xét trong quan hệ của nó với một lời
chú dẫn, tức là cái mà người ta mong đợi có được sau khi thực hiện câu lệnh hay ít
ra thì cũng là sự ảnh hưởng đến trạng thái của các biến trong chương trình. Do đó,
câu lệnh trên sẽ đúng với đặc tả:
“Điều này đảm bảo cho x và y có giá trị khác nhau”
nhưng nó sẽ sai với đặc tả:
“Điều này đả
m bảo rằng x có giá trị âm”
(giả sử các thực thể có kiểu số nguyên. Như vậy, x có thể có kết quả không âm sau
khi gán. Điều đó tùy thuộc vào giá trị của y).
Ví dụ này nhằm minh họa cho khái niệm “tính đúng đắn” được trình bày bên
dưới: Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
19 Tính đúng đắn của phần mềm
Tính đúng đắn là một khái niệm quan hệ

−
Việc thực hiện các tài liệu cho phần mềm dễ dàng. Chúng ta sẽ thấy
được ở phần sau rằng những xác nhận sẽ đóng một vai trò trung tâm trong việc
hướng đối tượng đến gần 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#
20
−
Cung cấp một căn bản cho việc kiểm tra và debug hệ thống.

Trong những phần còn lại chúng ta sẽ tìm hiểu những ứng dụng này.
Trong C, C++ và một số ngôn ngữ khác (dưới sự chỉ đạo của Algol W), ta có
thể viết một câu lệnh đóng vai trò một xác nhận để kiểm tra một tình trạng nào đó
có được giữ ở một trạng thái nào đó như mong muốn hay không khi thực thi phần
mềm, và chương trình sẽ không được thực thi nếu nó không thoả. Mặc dù như thế
cũng có thể làm được những gì mà ta muốn, nhưng việc làm vậy chỉ tượng trưng
cho một phần nhỏ của việc sử dụng những lời xác nhận trong phương pháp hướng
đối tượng. Do đó, nếu giống như nhiều người phát triển phần mềm khác thì bạn sẽ
quen với những câu lệnh như thế nhưng lại không thấy được bức tranh toàn cảnh.
Hầu hế
t tất cả những khái niệm được bàn ở đây đều sẽ mới lạ với bạn.


số những ngôn ngữ phần mềm mà chỉ được thiết kế nhằm giúp cho việc thể hiện
những thuộc tính của các thành phần phần mềm. Trong {P} A {Q}, A biểu thị cho
một thao tác, P và Q là những thuộc tính của những thực thể khác nhau có liên quan
hay còn được gọi là những xác nhận (chúng ta sẽ định nghĩa từ “xác nhận”
(“assertion”) một cách chính xác hơn ở phần sau). Trong hai xác nhận này, P được
gọi là tiền điều kiệ
n (precondition) và Q được gọi là hậu điều kiện (postcondition).
Ví dụ, ta có một công thức bình thường của tính đúng đắn như sau với giả sử
rằng x là một số nguyên: {x>=9} x := x+5 {x>=13}Công thức tính đúng đắn được sử dụng để đánh giá tính đúng đắn của phần
mềm. Điều đó cũng có nghĩa là tính đúng đắn chỉ được xét đến khi nó gắn với một
đặc tả nào đó. Như vậy, khi thảo luận về tính đúng đắn của phần mềm, ta không nói
đến những thành phần phần mềm riêng lẻ A, mà nó là bộ ba bao gồm một thành
phần ph
ần mềm A, một tiền điều kiện P và một hậu điều kiện Q. Mục đích duy nhất
của việc này là thiết lập kết quả cho những công thức tính đúng đắn {P} A {Q}.
Trong ví dụ trên, con số 13 ở hậu điều kiện không phải là lỗi do in ấn hay gõ
phím! Giả sử thực hiện đúng phép tính trên số nguyên ở công thức trên: với điều
kiện x>=9 là
đúng trước câu lệnh, x>=13 sẽ đúng sau khi thực hiện câu lệnh.
Tuy nhiên, ta thấy được nhiều điều thú vị hơn:
−
Với một tiền điều kiện như vậy, hậu điều kiện hay nhất phải là điều
kiện mạnh nhất, và trong trường hợp này là x>=14.
−

c hết, với P: bạn khuyên anh ta nên chọn một công việc với tiền điều
kiện yếu hay mạnh? Câu hỏi tương tự cho hậu điều kiện Q. Bạn hãy suy nghĩ và
chọn cho mình một quyết định trước khi xem câu trả lời ở phần dưới.
Trước hết, ta nói về tiền điều kiện. Từ quan điểm của người làm công tương
lai, tức là người sẽ th
ực hiện công việc A, tiền điều kiện P định nghĩa những trường
hợp mà ta sẽ phải thực hiện công việc. Do đó, một P mạnh là tốt, vì P càng mạnh thì
các trường hợp bạn phải thực hiện A càng được giới hạn. Như vậy, P càng mạnh thì
càng dễ cho người làm công. Và tuyệt vời nhất là khi kẻ làm công chẳng phải làm gì
cả tức là hắn ta là kẻ ăn không ngồi rồ
i. Điều này xảy ra khi công việc A được định
nghĩa bởi: Công thức 1
{False} A {…}Trong trường hợp này, hậu điều kiện không cần thiết phải đề cập bởi dù nó
có là gì thì cũng không có ảnh hưởng. Nếu có bao giờ bạn thấy một mục tuyển
người như vậy thì đừng mất công đọc hậu điều kiện mà hãy chớp lấy công việc đó Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#

không thành vấn đề, ngay cả nó là một đoạn code mà khi thi hành, chương trình sẽ
bị rơi vào một vòng lặp không điểm dừng hay là sẽ gây hỏng máy cũng chẳng sao.
Vì dù A là gì thì cũng đúng với đặc tả của nó. Tuy nhiên, với công thức 2, vấn đề là
ở trạng thái kết thúc, nó không cần thoả mãn bất kỳ thuộc tính đặc biệt nào nhưng
trạng thái kế
t thúc phải được đảm bảo là có tồn tại. Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#
24
Những đọc giả mà đã quen với lý thuyết khoa học máy tính hay những kỹ
thuật chứng minh lập trình sẽ thấy rằng công thức {P} A {Q} dùng ở đây ám chỉ
toàn bộ tính đúng đắn, bao gồm cả sự kết thúc cũng như việc phù hợp với đặc tả.
(Tính chất mà một chương trình sẽ thoả mãn với đặc tả của nó lúc kết thúc là một
phần của tính đúng đắn).
Nãy giờ, ta thảo luận một xác nhận mạnh hơn hay yếu hơn là những “tin tốt”
hay “tin xấu” là dựa trên quan điểm của một người làm công trong tương lai. Nếu
bây giờ thay đổi cách nhìn, đứng trên cương vị của một người chủ, ta thấy mọi thứ
sẽ thay đổi: một tiền điều kiện yếu sẽ là những tin tốt nếu ta muốn các trường hợp
thực thi công vi
ệc được tăng lên, và một hậu điều kiện mạnh sẽ là tốt nếu ta muốn
những kết quả của công việc thật sự có ý nghĩa.
Sự đảo ngược của những tiêu chuẩn này là đặc trưng của việc thảo luận về
tính đúng đắn của phần mềm, và sẽ xuất hiện lại như khái niệm chính trong luận

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: