ĐẠI HỌC QUỐC GIA HÀ NỘI
TRƯỜNG ĐẠI HỌC CÔNG NGHỆ
Nguyễn Thế Nam

NGHIÊN CỨU THIẾT KẾ THEO HỢP ĐỒNG
VÀ
XÂY DỰNG CÔNG CỤ HỖ TRỢ
KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY

Ngành: Công Nghệ Thông Tin


KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Chuyên ngành: Công Nghệ Phần Mềm
Cán bộ hướng dẫn: TS. Trương Ninh Thuận
HÀ NỘI - 2010
LỜI CẢM ƠN
Sinh viên thực hiện khoá luận tốt nghiệp đề tài “Nghiên cứu thiết kế theo hợp
đồng và xây dựng công cụ hỗ trợ” xin được bày tỏ lòng chân thành biết ơn tới các thầy
cô giáo Trường Đại học Công Nghệ, Đại học Quốc Gia Hà Nội nói chung và thầy cô
Bộ môn Công nghệ Phần mềm nói riêng. Trong suốt bốn năm qua thầy cô không

được gọi là “kỹ thuật thu gom rác” cũng làm cho phần mềm tối ưu hơn bình thường.
Hoặc là việc sử dụng lại những công cụ có sẵn của những phần mềm đáng tin cậy
trước đó cũng là một giải pháp thường được các nhà phát triển ứng dụng. Chi tiết hơn
nữa là phát triển tất cả các giai đoạn: phân tích, thiết kế, lập trình, kiểm thử, bảo trì
trong một dự án phần mềm.
Tiếp theo, khóa luận còn đưa ra các mô hình dựa trên CORBA. Khái niệm về kỹ
nghệ phần mềm hướng thành phần. Một phần mềm được tạo ra là do sự ghép nối các
thành phần độc lập lại với nhau. Các thành phần này sẽ không cần phải biên dịch lại
hoặc không cần phải chỉnh sửa lại khi thêm mới một thành phần khác hay là chỉnh sửa
một thành phần có sẵn. Mô hình thành phần CORBA là mô hình chính mà chúng tôi
nghiên cứu và ứng dụng nó trong việc xây dựng công cụ hỗ trợ.
Ngoài ra khóa luận còn đi vào xây dựng công cụ đặc tả và kiếm chứng hỗ trợ
người dùng kiểm tra sự phù hợp của các thành phần khi kết nối với nhau một cách trực
quan. Công cụ có áp dụng những công nghệ mới hiện nay như mô hình Model – View
– Controller (M-V-C) [6] hoặc sử dụng thư viện layer trong lập trình java game, dễ
dàng cho việc lập trình công cụ.
MỤC LỤC
Mở đầu 1
CHƯƠNG 1. Tính đúng đắn, tính tin cậy của phần mềm 3
1.1. Một số cơ chế mang lại tính đúng đắn 3
1.2. Biểu diễn một đặc tả 4
1.2.1. Những công thức của tính đúng đắn 4
1.2.2. Những điều kiện yếu, mạnh 5
1.3. Giao ước cho tính tin cậy của phần mềm 7
1.3.1. Quyền lợi 8
1.3.2. Nghĩa vụ 8
CHƯƠNG 2. Giới thiệu về Design by Contract 9
2.1. Giới thiệu 9
2.2. Khái niệm về hợp đồng 10
2.3. Tiền điều kiện, hậu điều kiện và tính bất biến 11

4.3. Phân tích công cụ đặc tả và kiểm chứng thành phần 31
4.3.1. Mô tả công cụ 31
4.3.2. Mô hình hoạt động 32
4.3.3. Thiết kế các lớp và đối tượng 32
4.3.3.1. Sơ đồ tương tác giữa các đối tượng 33
4.3.3.2. Mô tả chi tiết các lớp đối tượng 35
4.4. Triển khai 37
4.5. Thử nghiệm 37
4.5.1. Bài toán 37
4.5.2. Giao diện khởi động chương trình 40
4.5.3. Giao diện khi làm việc với các thành phần 41
4.5.4. Giao diện làm việc với các cổng 42
4.5.5. Giao diện sau khi kiểm chứng kết nối giữa các thành phần 45
Kết luận 47
Hướng phát triển 48
Tài liệu tham khảo 49
Phụ lục 50
DANH MỤC HÌNH VẼ
Hình 1: Giao diện thành phần CORBA và các cổng 26
Hình 2: Mô hình MVC 32
Hình 3: Sơ đồ lớp thể hiện mối liên hệ giữa các đối tượng trong ứng dụng 34
Hình 4: Sơ đồ lớp thể hiện mối quan hệ kế thừa của các cổng 34
Hình 5: Lớp Component 35
Hình 6: Lớp port 35
Hình 7: Lớp canvaspanel 36
Hình 8: Lớp Contract 37
Hình 9: Kiến trúc CCM của hệ thống Stock Quoter. 38
Hình 10: Giao diện thành phần CORBA và các cổng 38
Hình 11: Giao diện khởi động ứng dụng 40
Hình 12: Giao diện điền thông tin khi thêm mới 1 thành phần 41

Phát triển hướng thành phần
CORBA
Common Object Request
Broker Architecture
Kiến trúc môi giới gọi các đối tượng
phân tán
CCM
CORBA component
Model
Mô hình thành phần CORBA
API
Application
Programming Interface
Giao diện lập trình ứng dụng

1

Mở đầu
Trong phát triển phần mềm, thay đổi yêu cầu là một tất yếu diễn ra hết sức
thường xuyên mà những nhà phát triển phải chấp nhận và cố gắng điều chỉnh nó. Phần
mềm này ra đời thay thế phần mềm khác là một điều vô cùng bình thường, dễ hiểu. Tại
sao lại như thế? Bởi vì người sử dụng luôn mong muốn có được một phần mềm hữu
ích hơn, tiện lợi hơn và hoạt động tốt hơn. Tuy nhiên, dù phần mềm có thể đáp ứng
những nhu cầu của người sử dụng trong thời gian hiện tại thì cũng không thể đảm bảo
nó sẽ luôn được ưa chuộng. Để có thể tồn tại lâu dài, phần mềm phải thật sự chất
lượng. Điều này đồng nghĩa với việc nó phải không ngừng được cập nhật. Mà như
chúng ta đã biết, phần mềm càng đúng đắn, đáng tin 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ính đúng đắn, tính tin cậy của phần mềm
1.1. Một số cơ chế mang lại tính đúng đắn
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 phức tạp. Đặ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 cơ chế khác 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 mô tả 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.
Thêm vào đó, một cơ chế 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à kỹ thuật thu gom rác (garbage collection). Đây là cơ chế được sử
dụng phổ biến trong việc viết ứng dụng hiện nay. Các ứng dụng một cách tự động có
thể thu hồi hoặc xóa đi các mảnh vụn bộ nhớ không còn được sử dụng nữa. 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à do người lập trình điều khiển) hoặc bộ nhớ không hề được thu hồi
thì thật là nguy hiểm.
Ngoài ra, việc sử dụng lại những công cụ của những phần mềm đáng tin cậy
trước đó cũng tăng thêm tính tin cậy cho phần mềm của chúng ta hơn là khi ta xây
dựng một hệ thống mới hoàn toàn.
Tóm lại, tất cả những cơ chế này cung cấp một nền tảng cần thiết để ta có cái
nhìn gần hơn về một hệ thống phần mềm đúng đắn và bền vững.


- 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>=16.
5

- Còn với hậu điều kiện đã đưa ra thì tiền điều kiện hay nhất phải là tiền
điều kiện yếu nhất, ở đây là x>=9.
Từ một công thức đã cho, chúng ta luôn có thể có được một công thức khác bằng
cách mở rộng tiền điều kiện hay nới lỏng đi hậu điều kiện. Bây giờ, chúng ta sẽ cùng
nhau xem xét nhiều hơn về những khái niệm “mạnh hơn” và “yếu hơn” là thế nào.
1.2.2. Những điều kiện yếu, mạnh
Một cách để xem xét đặc tả theo dạng {P} A {Q} là xem nó như một mô tả các
công việc cho A. Điều này cũng giống như có một mục quảng cáo tuyển người trên
báo đăng rằng “Cần tuyển một người có khả năng thực hiện công việc A khi A có
trạng thái bắt đầu là P, và sau khi A được hoàn tất thì nó phải thỏa mãn Q”.
Giả sử, một người bạn của bạn đang kiếm việc và tình cờ đọc được những quảng
cáo tương tự như thế này, tất cả lương và lợi ích của chúng đều như nhau, chỉ có điều
là chúng khác nhau ở những cái P và Q. Cũng giống như nhiều người, bạn của bạn thì
lười nhác, có thể nói rằng, anh ta muốn có một công việc dễ nhất. Và anh ta hỏi ý kiến
bạn là nên chọn công việc nào. Trong trường hợp này, bạn sẽ khuyên anh ấy thế nào?
Trướ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:
{False} A {…}

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.
Những ai đã 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).
7

Chúng 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 văn này:
hợp đồng giữa những khách hàng và những môđun cung cấp là một sự ràng buộc giữa
hai bên. Để sản xuất ra một phần mềm hiệu quả và đáng tin cậy thì cần phải có một
hợp đồng đại diện cho sự thoả hiệp tốt nhất của tất cả mối liên hệ giữa những nhà cung
cấp và khách hàng.
1.3. Giao ước cho tính tin cậy của phần mềm
Bằng cách kết hợp những mệnh đề tiền điều kiện pre và hậu điều kiện post trong
thủ tục r, lớp đối tượng “tuyên bố” với những khách hàng của nó:
Nếu các bạn hứa gọi r thỏa mãn pre, tôi hứa sẽ trả về kết quả thỏa mãn post [3]
Trong mối liên hệ giữa người và người hoặc giữa các công ty với nhau, hợp đồng
là một văn bản làm cho những điều khoản của mối quan hệ trở nên trong sáng, rõ ràng.
Thật đáng ngạc nhiên khi trong lĩnh vực phần mềm, nơi mà sự đúng đắn, rõ ràng có

Khi xét đến sự phát triển các phương thức và công cụ của một phần mềm mới,
các nhà phát triển đã có khuynh hướng chú trọng đến năng suất hơn là chất lượng của
phần mềm. Thời đại hiện nay, xu hướng đó đã không còn phù hợp. Trong công nghệ
hướng đối tượng [3] các lợi ích về năng suất đã xếp vị trí thứ yếu, phần lớn các nhà
phát triển đã chuyển sang lợi ích về chất lượng sản phẩm.
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.
10

 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

không)
- Đưa khách hàng điến địa
điểm cần đến
- Không cần quan tâm
khách hàng đến trễ hay
không.
- Có mang hành lý cấm
hay không.
- Đã trả tiền vé chưa.
11Hợp đồng đảm bảo cho cả bên khách bởi sự chỉ rõ nên thực hiện những gì và cho
bên cung cấp bằng cách chỉ ra bên cung cấp không phải chịu trách nhiệm về những gì
bên thực hiện không thực hiện đúng những quy định trong phạm vi hợp đồ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
1
, t
2
,…, 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

phương thức. Chúng chỉ rõ nhiệm vụ được thi hành bởi một phương thức. Việc định
nghĩa tiền điều kiện và hậu điều kiện cho một phương thức là cách để định nghĩa một
hợp đồng, hợp đồng này ràng buộc phương thức và các lời gọi đến nó.
12

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.3.2. Tính bất biến
Tính bất biến ràng buộc gán các kiểu cần giúp cho đúng với các trường hợp của
kiểu mà hành động bắt đầu được biểu diễn trong trường hợp đó. Trong trường hợp của
các phương thức thành phần, chúng ta có thể gắn tính bất biến vào giao diện để xác
định thuộc tính của đối tượng thành phần thực thi giao diện. Ví dụ, tính bất biến có thể
nói rõ được giá trị của một vài thuộc tính luôn phải lớn hơn 0.
Đ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:
{INV & P} A {INV & Q}
Công thức 4: Điều kiện bất biến trong công thức tính đúng đắn
INV là điều kiện bất biến được thêm vào. Điều này thể hiện rằng bất biến INV là
không thay đổi trước và sau khi thực hiện A.
2.4. Design By Contract trong Eiffel
Eiffel [4] hỗ trợ rất nhiều tính năng: tiếp cận hướng đối tượng hoàn thiện, khả
năng giao tiếp bên ngoài (có thể giao tiếp với các ngôn ngữ C, C++, Java,…), hỗ

boolean expressions trong mệnh đề invariant
 Chỉ thị Check: Được thể hiện bằng cặp từ khóa check…end
Ví dụ:
check
assertion_clause
1

assertion_clause
2

14

…
assertion_clause
n

end
 Loop invariant, loop variant
from
initialization
until
exit
invariant
inv
variant
var
loop
body
end
2.4.2. Ví dụ minh họa