LUẬN VĂN:NGHIÊN CỨU THIẾT KẾ THEO HỢP ĐỒNG VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ

Chia sẻ: Lan Lan | Ngày: | Loại File: PDF | Số trang:61

Thêm vào BST

Báo xấu

107
lượt xem 16
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Khóa luận tìm hiểu về công nghệ thiết kế theo hợp đồng (Design by Contract) [3] và trình bày những khái niệm cơ bản. Đây là công nghệ giúp cho chúng ta xây dựng đặc tả giữa các lớp trong một thành phần và xem xét sự kết hợp giữa chúng với nhau. Mở rộng hơn nữa là đặc tả các thành phần trong một phần mềm và các thành phần phải thỏa mãn những điều kiện nào đó mới có thể liên kết với nhau để tạo thành phần mềm có tính tin cậy, tính đúng đắn cao ...

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: LUẬN VĂN:NGHIÊN CỨU THIẾT KẾ THEO HỢP ĐỒNG VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ

ĐẠ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 ý kiến đóng góp có giá trị khi thực hiện đề tài này. Đề tài “Nghiên cứu thiết kế theo hợp đồng và xây dựng công cụ hỗ trợ” được hoàn thành trong thời gian hạn hẹp nên không tránh khỏi những khiếm khuyết. Chúng tôi rất mong nhận được ý kiến đóng góp từ thầy cô giáo và các bạn để có thể tiếp tục hoàn thiện hệ thống này hơn. Hà nội ngày 24 tháng 4 năm 2010 Sinh viên Nguyễn Thế Nam
TÓM TẮT NỘI DUNG Khóa luận tìm hiểu về công nghệ thiết kế theo hợp đồng (Design by Contract) [3] và trình bày những khái niệm cơ bản. Đây là công nghệ giúp cho chúng ta xây dựng đặc tả giữa các lớp trong một thành phần và xem xét sự kết hợp giữa chúng với nhau. Mở rộng hơn nữa là đặc tả các thành phần trong một phần mềm và các thành phần phải thỏa mãn những điều kiện nào đó mới có thể liên kết với nhau để tạo thành phần mềm có tính tin cậy, tính đúng đắn cao. Bên cạnh đó khóa luận còn đưa ra một số khái niệm và cơ chế cho tính đúng đắn của phần mềm. Các cấu trúc đơn giản thường có tính tin cậy hơn những phần mềm có cấu trúc phức tạp. Nhưng điểm yếu của nó lại không thể phục vụ được nhu cầu ngày càng tăng lên của người phát triển và người sử dụng. Vì thế, một số cơ chế như cố gắng giữ cho cấu trúc của phần mềm càng đơn giản càng tốt. Viết văn bản mô tả phần mềm để người phát triển sau này có thể đọc lại hoặc viết lại. Quản lý bộ nhớ, hay còn đượ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 2.3.1. Tiền điều kiện và hậu điều kiện. .......................................................... 11 2.3.2. Tính bất biến ....................................................................................... 12 2.4. Design By Contract trong Eiffel.................................................................... 12 2.4.1. Biểu diễn Design by Contract trong Eiffel .......................................... 13 2.4.2. Ví dụ minh họa ................................................................................... 14 CHƯƠNG 3. Mô hình thành phần CORBA ........................................................... 16 3.1. Khái niệm cơ bản về công nghệ phần mềm hướng thành phần ...................... 16 3.1.1. Giới thiệu............................................................................................ 16 3.1.2. Thành phần ......................................................................................... 17 3.1.3. Đối tượng và thành phần ..................................................................... 17 3.1.4. Giao diện ............................................................................................ 18 3.1.5. Hợp đồng ............................................................................................ 19 3.1.6. Khuôn mẫu ......................................................................................... 21
3.1.7. Frameworks ........................................................................................ 21 3.1.8. Frameworks và thành phần ................................................................. 22 3.2. Khái niệm CORBA ....................................................................................... 22 3.2.1. Giới thiệu............................................................................................ 22 3.2.2. Ngôn ngữ đặc tả giao tiếp IDL ............................................................ 23 3.3. Mô hình thành phần CORBA........................................................................ 25 3.3.1. Giao diện và sự nối ghép ..................................................................... 25 3.3.2. Đặc tả CCM bằng ngôn ngữ IDL ........................................................ 27 3.3.2.1. Thành phần ..................................................................................... 27 3.3.2.2. Facets .............................................................................................. 27 3.3.2.3. Receptacles ..................................................................................... 28 3.3.2.4. Event Sources.................................................................................. 28 3.3.2.5. Event Sinks ..................................................................................... 30 3.3.3. Điều kiện kết nối................................................................................. 30 CHƯƠNG 4. Xây dựng công cụ đặc tả và kiểm chứng thành phần ...................... 31 4.1. Mô tả công cụ ............................................................................................... 31 4.2. Ngôn ngữ phát triển công cụ ......................................................................... 31 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 Hình 13: Giao diện kết quả sau khi thêm một thành phần thành công ........................ 42 Hình 14: Giao diện điền thông tin khi thêm một cổng mới ......................................... 43 Hình 15: Giao diện kết quả khi thêm mới cổng thành công ........................................ 44 Hình 16: Giao diện khi kết nối thành công các cổng .................................................. 45 Hình 17: Giao diện khi kết nối không thành công các cổng ........................................ 46
DANH MỤC BẢNG BIỂU Bảng 1: Hợp đồng giữa một hãng hàng không và khành hàng .................................... 10 Bảng 2: Hợp đồng chèn một từ vào từ điển ................................................................ 11 Bảng 3: Bảng ánh xạ từ IDL sang java ....................................................................... 24 Bảng 4: Các lớp đối tượng trong ứng dụng ................................................................ 33 Bảng 5: Chi tiết lớp component ................................................................................. 35 Bảng 6: Chi tiết lớp port ............................................................................................ 36 Bảng 7: Chi tiết lớp canvaspanel ................................................................................ 36 Bảng 8: Chi tiết lớp Contract ..................................................................................... 37
DANH MỤC CÔNG THỨC Công thức 1: Công thức tính đúng đắn ......................................................................... 4 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................. 5 Công thức 3: Hậu điều kiện mạnh, tiền điều kiện không cần phải quan tâm. ................ 6 Công thức 4: Điều kiện bất biến trong công thức tính đúng đắn ................................. 12
BẢNG KÝ HIỆU, CHỮ VIẾT TẮT Viết tắt Viết đầy đủ Giải nghĩa DbC Design by Contract Thiết kế theo hợp đồng Component-Based CBSE Kĩ nghệ phần mềm hướng thành phần Software Engineering Component-Based CBD Phát triển hướng thành phần Development Common Object Request Kiến trúc môi giới gọi các đối tượng CORBA Broker Architecture phân tán CORBA component CCM Mô hình thành phần CORBA Model Application API Giao diện lập trình ứng dụng Programming Interface
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, chúng tôi đã 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 tôi còn xây dựng một công cụ về đặc tả và kiểm chứng cho các thành phần trong ngôn ngữ Java. Đối tượng và phạm vi nghiên cứu: ý tưởng chính của thiết kế theo hợp đồng là lập một “hợp đồng” giữa các đối tượng cung cấp (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. Mở rộng hơn là nghiên cứu thành phần phần mềm. Nó là một trong những nghiên cứu quan trọng trong kỹ nghệ phần mềm hướng thành phần, thể hiện bước đầu tiên hướng tới việc tái sử dụng thành phần, đặc tả thành phần mang lại những thông tin cần thiết để người sử dụng có thể hiểu được vì sao và như thế nào mà thành phần có thể sử dụng được hoặc tái sử dụng. Từ đó nghiên cứu mối quan hệ giữa các thành phần trong một phần mềm và điều kiện để 1
các thành phần đó có thể liên kết được với nhau. Song song với việc nghiên cứu công nghệ thiết kế theo hợp đồng, chúng tôi cũng đã nghiên cứu sâu hơn về ngôn ngữ java, mô hình thiết kế Model – View – Controller (M-V-C) và xây dựng công cụ đặc tả, kiếm chứng giúp cho việc làm sáng rõ thêm công nghệ mà chúng tôi đã nghiên cứu. 2
CHƯƠNG 1. 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. 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 Ý nghĩa của công thức tính đúng đắn {P} A {Q} Bất kỳ thi hành nào của A, bắt đầu ở trạng thái P thì sẽ kết thúc với trạng thái Q Những công thức của tính đúng đắn (còn được gọi là bộ ba Hoare [7]) là một ký hiệu toán học, không phải là một khái niệm lập trình; chúng không phải là một trong 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 công thức 1, 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. 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ụ, chúng 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>=10} x := x+6 {x>=15} 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ố 15 ở 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>=7 là đúng trước câu lệnh, x>=15 sẽ đúng sau khi thực hiện câu lệnh. Tuy nhiên, chúng 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>=16. 4
- 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 {…} 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 5
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 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ả. Còn với hậu điều kiện Q, tình trạng bị đảo ngược. Một hậu điều kiện mạnh là một tin xấu: nó chỉ ra rằng bạn phải mang lại nhiều kết quả hơn. Q càng yếu, càng tốt cho người làm thuê. Thực tế, công việc ăn không ngồi rồi tốt nhì trên thế giới là công việc được định nghĩa mà không chú ý đến tiền điều kiện: {…} A {True} Công thức 3: Hậu điều kiện mạnh, tiền điều kiện không cần phải quan tâm. Hậu điều kiện True là một xác nhận yếu nhất vì nó thỏa mãn mọi trường hợp. Khái niệm “mạnh hơn” hay “yếu hơn” được định nghĩa một cách hình thức từ logic: P1 được gọi là mạnh hơn P2, và P2 yếu hơn P1 nếu P1 bao hàm P2 và chúng không bằng nhau. Khi mọi lời xác nhận bao hàm True, và False bao hàm mọi xác nhận thì thật là hợp lý để nói rằng True như là yếu nhất và False như là mạnh nhất với tất cả xác nhận có thể. Đến đây, có một câu hỏi được đặt ra: “Tại sao công thức 2 là công việc tốt nhì trên thế giới?” Câu trả lời chính là một điểm tinh tế trong phần định nghĩa ý nghĩa của công thức {P} A {Q}: sự kết thúc. Định nghĩa nói rằng sự thực thi phải kết thúc trong tình trạng thoả Q miễn là khi bắt đầu nó thoả P. Với công thức 1, không có trường hợp nào thoả P. Do đó, A là gì cũng không thành vấn đề, ngay cả nó là một đoạn mã 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. 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). 6
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ó 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. 7
1.3.1. Quyền lợi Đối với khách hàng, đó là sự đảm bảo những thuộc tính phải có được sau khi gọi thủ tục. Đối với nhà cung cấp, đó là sự đảm bảo những tính chất phải được thỏa mãn ở bất cứ nơi nào thủ tục được gọi. 1.3.2. Nghĩa vụ Đối với khách hàng, đó là sự đáp ứng những yêu cầu được phát biểu trong tiền điều kiện. Đối với nhà cung cấp, đó là những gì phải làm mà hậu điều kiện đã định ra. 8
CHƯƠNG 2. Giới thiệu về Design by Contract 2.1. Giới thiệu 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. 9