TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 2

Chia sẻ: Cao Tt | Ngày: | Loại File: PDF | Số trang:12

Thêm vào BST

Báo xấu

86
lượt xem 6
download

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

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# var loop body end Demo: Project stack STACK_CLASS: lớp stack chính, chứa các định nghĩa các thao tác trên stack. make: Hàm khởi tạo của stack. item: hàm lấy phần tử trên cùng stack. get(t): hàm lấy phần tử thứ t empty: kiểm tra stack có rỗng. full: kiểm tra stack có đầy put(x): thêm phần tử x vào stack remove: bỏ phần tử trên cùng stack TEST_CLASS: lớp chính(main), lớp gọi các hàm của lớp STACK_CLASS. Ta sẽ thử vài trường hợp cho thấy...

Chủ đề:

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

Lưu

Nội dung Text: TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 2

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# var loop body end Demo: Project stack STACK_CLASS: lớp stack chính, chứa các định nghĩa các thao tác trên stack. make: Hàm khởi tạo của stack. item: hàm lấy phần tử trên cùng stack. get(t): hàm lấy phần tử thứ t empty: kiểm tra stack có rỗng. full: kiểm tra stack có đầy put(x): thêm phần tử x vào stack remove: bỏ phần tử trên cùng stack TEST_CLASS: lớp chính(main), lớp gọi các hàm của lớp STACK_CLASS. Ta sẽ thử vài trường hợp cho thấy khả năng bắt lỗi của Eiffel. Lưu ý: Sau mỗi trường hợp hãy sửa lại code như ban đầu rồi mới thử tiếp trường hợp khác. Mở tập tin test_class.e. Chạy thử chương trình (F5). Chương trình khởi tạo stack gồm 8 phần tử từ 0 đến 7 và xuất stack. Stack được xuất ra màn hình. 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). 13
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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: Code gây ra lỗi ở tiền điều kiện Nguyên nhân: Khi bạn gọi thủ tục a.make(n), do trước đó khởi tạo n là một số âm (=-8), client không đảm bảo contract, nên trong thủ tục make của lớp STACK_CLASS, thủ tục make kiểm tra không thỏa tiền điều kiện positive_capacity: n>=0, nó dừng lại và thông báo cho người lập trình biết. TH2: Lỗi xảy ra ở hậu điều kiện Trong lớp TEST_CLASS, tại thủ tục make, sửa như sau: 14
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Capacity := n capacity := n-1 Recompile (Shift-F7) và cho chạy lại chương trình (F5). 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 15
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Chọn menu Project > Project Setting… Bỏ dấu check ở ensure. Đánh dấu check ở invariant. Hành động này nhằm bỏ qua chế độ kiểm lỗi ở hậu điều kiện. Ở đây chỉ muốn minh họa cho việc phát hiện lỗi ở điều kiện bất biến. Recompile (Shift-F7) và cho chạy lại chương trình (F5). Xuất hiện thông báo ngoại lệ sau: Hình 1-6: Thông báo khi lỗi xảy ra ở điều kiện bất biến và con trỏ dừng lại ở câu lệnh Hình 1-7: Code gây ra lỗi ở điều kiện bất biến Nguyên nhân: Trước đó, ta gán count := -1, điều kiện bất biến yêu cầu count>=0. 16
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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à 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. Bộ thu gom rác không hề là một sự xa xỉ mà nó là thành phần thiết yếu để mở rộng tính đáng tin cậy cho bất kỳ một môi trường hướng đối tượng nào. Một kỹ thuật khác nữa mà cũng có thể là thiết yếu mà có liên quan đến genericity là static typing. Nếu không có những luật như thế thì chúng ta sẽ không kiểm soát được những lỗi xảy ra lúc run-time do quá trình gõ code gây nên. 17
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Tóm lại, tất cả những kỹ thuật 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. Chương 3: Tính đúng đắn của phần mềm Giả sử có một người đưa cho bạn một chương trình C với 300 000 dòng lệnh và hỏi rằng nó có đúng không. Tôi nghĩ rằng rất có khả năng bạn thấy khó và thậm chí là không thể trả lời được. Tuy nhiên, nếu là một cố vấn viên, bạn hãy trả lời “Không” và sau đó tính một giá thật cao vì rất có thể bạn đúng. Thật sự, để có thể trả lời câu hỏi trên một cách đúng nghĩa, bạn không những cần phải lấy chương trình đó mà còn phải lấy cả lời diễn giải về những gì mà chương trình đó làm được hay ta gọi chúng là những đặc tả của chương trình. 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: 18
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Tính đúng đắn của phần mềm Tính đúng đắn là một khái niệm quan hệ Một hệ thống phần mềm hay một thành phần phần mềm thì không đúng cũng không sai. Nó chỉ đúng hay sai khi có liên quan với một đặc tả nào đó. Nói một cách chính xác, ta không thảo luận những thành phần phần mềm có đúng hay không, mà là thảo luận chúng có phù hợp với những đặc tả của chúng hay không. Do đó, thuật ngữ “tính đúng đắn” không được dùng cho những thành phần phần mềm, mà nó được dùng cho từng cặp, mỗi cặp bao gồm một thành phần phần mềm và một đặc tả. Trong phần này, ta sẽ biết cách biểu diễn những đặc tả thông qua một xác nhận (assertion) để giúp ta xác nhận tính đúng đắn của phần mềm. Điều này cho thấy kết quả của việc viết những đặc tả là một bước đầu tiên quan trọng để đảm bảo rằng phần mềm thật sự đúng. Việc viết những xác nhận cùng lúc hoặc đúng ra là trước khi viết phần mềm sẽ mang lại những lợi ích tuyệt vời như sau: Sản xuất được phần mềm đúng với khi bắt đầu vì nó được thiết kế − đúng. Ích lợi này đã được Harlan D.Mills (một trong những người khởi đầu đề xướng việc lập trình có cấu trúc “Structured Programming”) trình bày vào năm 1970 trong quyển sách “How to write correct programs and know it” (có nghĩa là “Làm thế nào để viết được những chương trình đúng và biết được nó đúng”). “Biết” ở đây có nghĩa là trang bị cho phần mềm những đối số khi ta viết nó nhằm hiển thị tính đúng đắn của nó. Có được sự hiểu biết tốt hơn về vấn đề và những cách giải quyết cuối − cùng của nó. 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. 19
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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. Chương 4: Biểu diễn một đặc tả Chúng ta có thể trở lại nhận xét trước với hình ảnh một ký hiệu toán học đơn giản được mượn từ lý thuyết của việc kiểm tra một chương trình hình thức và những lý do quý giá để lập luận về tính đúng đắn của các thành phần phần mềm. 4.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} Ý 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) 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 20
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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ò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>=8. Từ một công thức đã cho, 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ờ, 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. 21
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 4.2. Những điều kiện yếu và 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: 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 đó 22
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho 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 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: Công thức 2 {…} A {True} 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 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. 23
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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 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. Chương 5: Giới thiệu về sự xác nhận trong văn bản của phần mềm Để biểu diễn một đặc tả, chúng ta sẽ tin cậy vào những xác nhận. Một xác nhận là một biểu thức bao gồm những thực thể của phần mềm và phát biểu một thuộc tính rằng các thực thể này có thể thoả mãn ở những giai đoạn xác định khi thực thi phần mềm. Một xác nhận tiêu biểu có thể biểu diễn một số nguyên có giá trị dương hoặc một tham chiếu không phải rỗng. Về mặt cú pháp, khái niệm xác nhận đơn giản là một biểu thức logic. Ví dụ như: 24