Chương 1: Giới thiệu về Eiffel 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.
9 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 1. Design By Contract trong Eiffel Eiffel 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. 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.
EiffelStudio EiffelStudio là trình biên dịch của Eiffel. Ngoài ra, nó còn là một IDE rất mạnh với những tính năng độc nhất như: công cụ công nghệ đảo tích hợp, bộ máy 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. 10 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 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. 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.
Class view là khung làm việc chính của bạn. Sau khi lập trình xong, bạn có thể biên dịch và cho chạy chương trình bằng công cụ Compile (F7). Debug chương trình: F10, F11. Lưu project: File > Save.
11 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Biểu diễn Design By Contract trong Eiffel: Precondition: require boolean expressions Postcondition: ensure boolean expressions Class invariant: invariant boolean expressions Chỉ thị Check: check assertion_clause1 assertion_clause2 … assertion_clausen end Loop invariant, loop variant: from initialization until exit invariant inv variant 12 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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.
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. 13 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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. 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 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.