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

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C#require not_empty: not empty -- i.e. count 0 do Result := representation @ count end feature – Status report empty: BOOLEAN is -- Kiểm tra Stack rỗng? do Result := (count = 0) ensure empty_definition: Result = (count = 0) end full: BOOLEAN is -- Kiểm tra Stack đầy? do Result := (count = capacity) ensure full_definition: Result = (count = capacity) end feature – Element change put (x: G) is -- Thêm phần tử x vào Stack. require not_full: not full --i.e. count...
Nội dung trích xuất từ tài liệu:
TÌM HIỂU CÔNG NGHỆ DESIGN BY CONTRACT VÀ XÂY DỰNG CÔNG CỤ HỖ TRỢ CHO C# - 4Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# require not_empty: not empty -- i.e. count > 0 do Result := representation @ count endfeature – Status report empty: BOOLEAN is -- Kiểm tra Stack rỗng? do Result := (count = 0) ensure empty_definition: Result = (count = 0) end full: BOOLEAN is -- Kiểm tra Stack đầy? do Result := (count = capacity) ensure full_definition: Result = (count = capacity) endfeature – Element change put (x: G) is -- Thêm phần tử x vào Stack. require not_full: not full --i.e. count < capacity in this representation do count := count + 1 representation . put (count, x) ensure not_empty: not empty added_to_top: item = x 37Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# one_more_item: count = old count + 1 in_top_array_entry: representation @ count = x end remove is -- Xóa phần tử trên cùng của Stack. require not_empty: not empty -- i.e. count > 0 do count := count – 1 ensure not_full: not full one_fewer: count = old count – 1 endfeature {NONE} -- Implementation representation: ARRAY [G] -- Mảng dùng để chứa các phần tử của Stackinvariant … Sẽ tìm hiểu trong phần sauend -- class STACK2 Phần biểu diễn về lớp ở trên cho ta thấy sự đơn giản khi làm việc với nhữngxác nhận. Ngoại trừ mệnh đề invariant còn thiếu sẽ được bổ sung trong phần sau,chúng ta hãy cùng nhau xem xét tỉ mỉ những thuộc tính khác nhau của nó. 8.2. Mệnh lệnh và yêu cầu Những xác nhận trong lớp STACK2 minh họa một khái niệm cơ bản mà ta đãcó cái nhìn lướt qua về sự chuyển tiếp từ những kiểu dữ liệu trừu tượng sang nhữnglớp: sự khác nhau giữa những khung nhìn “imperative” và “applicative”. Những xác nhận trong empty và full có thể làm bạn băn khoăn. Xét thủ tụcfull trong lớp trên: 38Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# full: BOOLEAN is -- Stack có đầy không? do Result := (count = capacity) ensure full_definition: Result = (count = capacity) end Hậu điều kiện yêu cầu rằng thực thể Result có giá trị luận lý bằng với giátrị của biểu thức count = capacity. Điều đó có nghĩa là Result có giá trị truenếu count bằng với capacity và nó có giá trị false nếu ngược lại. Result = (count = capacity) (1) Bởi vì trong thân thủ tục đã gán Result := (count = capacity) (2) Vậy thì liệu hậu điều kiện ở đây có dư thừa không? Có sự khác biệt rất lớn giữa (1) và (2), vì vậy không hề có sự dư thừa. (2) là một câu lệnh, thể hiện một hành động, gán giá trị true hay false củabiểu thức count = capacity cho biến Result. Trong khi đó, (1) chỉ là một xácnhận, không làm gì hết. Nó chỉ đặc tả thuộc tính của trạng thái cuối cùng đượcmong đợi Một câu lệnh, tức (2), thì mang tính chất ra lệnh, còn một xác nhận, tức (1),thì chỉ mang tính chất mô tả. Câu lệnh mô tả cho câu hỏi “như thế nào”, còn xácnhận mô tả cho câu hỏi “cái gì”. Một câu lệnh là một phần của cài đặt, còn một xácnhận chỉ là một thành phần của đặc tả. Câu lệnh thì mang tính mệnh lệnh, bắt buộc, còn xác nhận thì chỉ mang tínhyêu cầu. Hai thuật ngữ này nhấn mạnh sự khác nhau cơ bản giữa tin học và toánhọc. Những thao tác của tin học có thể làm thay đổi trạng thái của máy −tính. Những chỉ thị của các ngôn ngữ lập trình thông thường là những câu lệnh tácđộng trực tiếp đến máy tính. 39Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Những lý luận toán học không thể thay đổi bất cứ gì. Ví dụ như khi ta −lấy căn bậc hai của 2 thì số 2 trước khi lấy căn và sau khi lấy căn vẫn như nhau. Tóm lại, xác nhận là mô tả một kết quả được mong đợi, còn chỉ thị (thânvòng lặp) là ra lệnh bằng cách nào đó đạt được kết quả. ...