ĐẠ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
HÀ NỘI - 2010
ĐẠ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
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 những tận
tình truyền đạt kiến thức mà còn luôn động viên chúng tôi trong học tập cũng như trong
cuộc sống.
Đặc biệt, chúng tôi xin chân thành cảm ơn thầy giáo hướng dẫn, thầy Trương Ninh
Thuận, đã tận tình chỉ bảo, tạo mọi điều kiện cơ sở vật chất cũng như tinh thần cho
chúng tôi hoàn thành khóa luận và sửa chữa những sai sót trong suốt quá trình thực hiện
đề tài.
Chúng tôi cũng xin cảm ơn tới các bạn sinh viên K51 đã cho chúng tôi những ý

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. .................................................................................................................. 3
Tính đúng đắn, tính tin cậy của phần mềm ..................................................................... 3
CHƯƠNG 2. ................................................................................................................. 9
Giới thiệu về Design by Contract .................................................................................... 9
CHƯƠNG 3. ................................................................................................................ 16
Mô hình thành phần CORBA ........................................................................................ 16
Xây dựng công cụ đặc tả và kiểm chứng thành phần .................................................... 31
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......................................................25
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

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

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ừ nhu cầu ấy, công nghệ thiết kế
theo hợp đồng (Design By Contract) đã ra đời nhằm giúp cho việc đả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 tôi đã chọn đề tài này.
Với mục đích tìm hiểu công nghệ thiết kế theo hợp đồng một cách khá kỹ lưỡng,

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.
3
1.2.Biểu diễn một đặc tả
1.2.1.Những công thức của tính đúng đắn
Giả sử A thực hiện một vài thao tác (ví dụ A là một câu lệnh hay thân của một thủ
tục). Một công thức của tính đúng đắn là một cách biểu diễn theo dạng sau:
{P} A {Q}
Công thức 1: Công thức tính đúng đắn

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 {…}
Công thức 2: Tiền điều kiện mạnh, hậu điều kiện không cần phải quan tâm
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 đó ngay lập tức. Tiền
điều kiện False là sự xác nhận mạnh nhất có thể vì nó không bao giờ thỏa mãn một trạng
thái nào cả. Bất cứ yêu cầu nào để thực thi A cũng sẽ không đúng, và lỗi không nằm ở
trách nhiệm của A mà là ở người yêu cầu hay khách hàng (client) bởi nó đã không xem
5
xét bất cứ tiền điều kiện nào cần đến. Dù cho A có làm hay không làm gì đi nữa thì nó
cũng luôn đúng với đặc tả.

6
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ó vai
trò sống còn, ý tưởng hợp đồng này lại phải mất quá nhiều thời gian để thể hiện mình.
Tiền điều kiện và hậu điều kiện mô tả một hợp đồng giữa thủ tục (đóng vai trò nhà cung
cấp) và những đối tượng gọi đến nó (vai trò khách hàng).
Đặc tính quan trọng nhất của hợp đồng trong công việc của con người là sự đòi hỏi
về “nghĩa vụ” (obligation) và “quyền lợi” (right) cho cả 2 bên – thường là nghĩa vụ của
bên này sẽ trở thành quyền lợi của bên kia. Điều này cũng đúng đối với hợp đồng giữa
các lớp đối tượng:
- Tiền điều kiện ràng buộc khách hàng: nó định nghĩa những điều kiện để
một lời gọi đến thủ tục trở nên hợp pháp. Đây là nghĩa vụ của khách hàng
và là quyền lợi của nhà cung cấp.
- Hậu điều kiện ràng buộc lớp đối tượng: nó định nghĩa những điều kiện cần
phải được đảm bảo bởi thủ tục khi trả về. Đây là quyền lợi của khách hàng
và là nghĩa vụ của nhà cung cấp.

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.
9
• 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
tượng có ít hoặc hoàn toàn không có lỗi.
• Xây dựng được các framework hiệu quả hơn cho việc gỡ lỗi, kiểm thử.
• Dễ dàng viết tài liệu cho phần mềm.
• Hiểu và kiểm soát được kỹ thuật thừa kế.
• Một kỹ thuật cho mối quan hệ với các trường hợp dị thường, dẫn đến sự an
toàn và hiệu quả cho việc xây dựng các ngôn ngữ xử lý các trường hợp
ngoại lệ.
2.2.Khái niệm về hợp đồng
Trong công việc thường ngày, một hợp đồng được viết bởi hai bên khi một bên
(bên cung cấp) trình bày các công việc với bên kia (bên khách hàng). Mỗi bên mong chờ
các lợi ích từ hợp đồng và chấp nhận các giao ước có trong hợp đồng đó. Thông thường,
mỗi giao ước của bên này sẽ là lợi ích cho bên kia và ngược lại. Mục tiêu của bản hợp
đồng là giải thích rõ ràng các lợi ích và các giao ước.
Một ví dụ đơn giản sau đây minh họa cho một hợp đồng giữa một hãng hàng
không và khách hàng.
Bảng 1: Hợp đồng giữa một hãng hàng không và khành hàng
Giao ước Lợi ích

, 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
i
là công việc chèn một từ vào từ điển (một bảng mà mỗi phần tử được
xác định bởi một chuỗi ký tự sử dụng như là một khóa). Hợp đồng sẽ là:
Bảng 2: Hợp đồng chèn một từ vào từ điển
Giao ước Lợi ích
Bên thực hiện - Chắc chắn rằng bảng
không đầy dữ liệu và
khóa không phải là chuỗi
rỗng
- Cập nhật bảng chứa các
yếu tố xuất hiện, liên kết
với các khóa.
Bên cung cấp - Bản ghi đưa các yếu tố
vào bảng, liên kết với các
khóa.
- Không cần phải làm gì
nếu bảng đầy hoặc khóa
là một chuỗi rỗng..
Thiết kế theo hợp đồng được sử dụng ở đây để cung cấp đặc tả chính xác cho các

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ỗ
trợvòng đời phần mềm bao gồm việc phân tích, thiết kế, thực thi và bảo trì, hỗ trợ
Design By Contract, viết xác nhận, quản lý ngoại lệ…
Design By Contract hầu như là vấn đề luôn được nhắc đến khi đề cập về Eiffel.
Trong Eiffel, mỗi thành phần của hệ thống đều có thể được thực hiện theo một đặc tả
tiên quyết về các thuộc tính trừu tượng của nó, liên quan đến những thao tác nội tại và
những giao tác của nó với các thành phần khác.
12
Eiffel thực thi một cách trực tiếp ý tưởng Design By Contract, một phương pháp
làm nâng cao tính đáng tin cậy của phần mềm, cung cấp một nền tảng cho việc đặc tả,
làm tài liệu và kiểm nghiệm phần mềm, cũng như việc quản lý các ngoại lệ và cách sử
dụng kế thừa thích hợp.
2.4.1.Biểu diễn Design by Contract trong Eiffel
• Precondition: Được thể hiện bằng từ khóa require
Ví dụ:
require
boolean expressions
Cần phải thỏa mãn biểu thức lô-gic boolean expressions trong mệnh đề require
trước mới có thể thực hiện tiếp thủ tục r ở sau đó.
• Postcondition: Được thể hiện bằng từ khóa ensure
Ví dụ:
ensure
boolean expressions
Sau khi thực hiện thủ tục r, kết quả trả về phải thỏa mãn biểu thức lô-gic boolean
expressions trong mệnh đề ensure

2.4.2.Ví dụ minh họa
Lấy ví dụ cho thuật toán put với công việc chèn một phần tử x vào từ điển với x
chứa một chuỗi các kí tự được coi như là khóa.
Put (x: ELEMENT; key: STRING)is
require
count <= capacity
notkey.empty
do
… Thuật toàn chèn…
ensure
has (x)
item (key) = x
14
count = old count + 1
end
Mệnh đề requie giới thiệu về điều kiện input, hoặc là tiền điều kiện; mệnh đề
ensure giới thiệu về điều kiện output hay còn gọi là hậu điều kiện. Cả hai điều kiện là ví
dụ về sự xác nhận, hoặc điều kiện logic (mệnh đề hợp đồng) liên kết với thành phần
của phần mềm. Trong tiền điều kiện, biến count là số phần tử hiện thời và capacity là số
lượng lớn nhất có thể đưa vào; trong hậu điều kiện, has là hàm boolean để xem từ đó có
không, và item trả lại từ liên kết với khóa. Kí hiệu old count là giá trị count cũ.
Một ví dụ khác về cơ chế gửi tin.
send (m: MESSAGE)is
-- Gửi một tin nhắn m theo chế độ gửi nhanh nếu có thể,
nếu không sẽ chuyển sang chế độ gửi chậm.
local
tried_fast, tried_slow:BOOLEAN
do
if tried_fast then
tried_slow := True