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

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# trong giới hạn cho phép. Điều kiện bất biến biểu diễn mối quan hệ giữa count, lower và upper; nó cho phép count được cài đặt như một hàm chứ không phải một thuộc tính. indexing description: "Mảng giá trị cùng kiểu, truy xuất các phần tử thông qua các chỉ số mảng" class ARRAY [G] creation make feature -- Khởi tạo make (minindex, maxindex: INTEGER) is -- Xác định 2 biên của mảng với minidex và maxindex -- Mảng rỗng nếu minindex maxindex. require meaningful_bounds: maxindex...
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# - 6 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# trong giới hạn cho phép. Điều kiện bất biến biểu diễn mối quan hệ giữa count, lower và upper; nó cho phép count được cài đặt như một hàm chứ không phải một thuộc tính. indexing description: 'Mảng giá trị cùng kiểu, truy xuất các phần tử thông qua các chỉ số mảng' class ARRAY [G] creation make feature -- Khởi tạo make (minindex, maxindex: INTEGER) is -- Xác định 2 biên của mảng với minidex và maxindex -- Mảng rỗng nếu minindex > maxindex. require meaningful_bounds: maxindex >= minindex - 1 do … ensure exact_bounds_if_non_empty: (maxindex >= minindex) implies ((lower = minindex) and (upper = maxindex)) conventions_if_empty: (maxindex < minindex) implies ((lower = 1) and (upper = 0)) end feature – Truy cập lower, upper, count: INTEGER -- Chỉ số cao nhất vào thấp nhất hợp lệ; kích thước mảng. infix '@', item (i: INTEGER): G is -- Giá trị mảng tại chỉ số i 61 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# require index_not_too_small: lower Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Danh sách các hàm với những ký hiệu của chúng (phần − FUNCTIONS) Tiên đề (AXIOMS) mô tả những thuộc tính của kết quả − Những quy định để sử dụng được hàm (phần PRECONDITIONS) − Ví dụ: ADT của lớp STACK TYPES • STACK [G] FUNCTIONS • put: STACK [G] × G → STACK [G] • remove: STACK [G] →STACK [G] • item: STACK [G] → G • empty: STACK [G] → BOOLEAN • new: STACK [G] AXIOMS For any x: G, s: STACK [G] A1 • item (put (s, x)) = x A2 • remove (put (s, x)) = s A3 • empty (new) A4 • not empty (put (s, x)) PRECONDITIONS • remove (s: STACK [G]) require not empty (s) • item (s: STACK [G]) require not empty (s) 11.1. So sánh đặc tính của lớp với những hàm ADT Để hiểu được mối liên hệ giữa những xác nhận và ADT, trước tiên ta cần tìm hiểu mối liên hệ giữa những đặc tính của lớp và phần tương ứng của ADT – những hàm của ADT. Những hàm này gồm 3 loại: creator, query và command. 63 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Sự phân loại của một hàm f: A × B × … X phụ thuộc vào vị trí xuất hiện của ADT (A, B, …, X) so với mũi tên , gọi là T . Nếu T chỉ xuất hiện ở bên phải của mũi tên thì f là hàm creator. Trong lớp đối tượng, nó là phương thức khởi tạo. Ví dụ: hàm new Nếu T chỉ có mặt ở bên trái của mũi tên thì f là hàm query. Trong lớp đối tượng, nó là những phương thức truy xuất đến những thuộc tính của các thể hiện của một lớp. Ví dụ: hàm item và empty. Nếu T xuất hiện ở cả 2 bên mũi tên thì f là hàm command. Những hàm này tạo ra những đối tượng mới từ những đối tượng đã có. Trong lớp đối tượng, những hàm này thường được biểu diễn như một phương thức để làm thay đổi một đối tượng hơn là tạo ra một đối tượng mới. Ví dụ hàm put và remove. 11.2. Biểu diễn những tiên đề Từ sự tương ứng giữa những hàm ADT và những đặc tính của lớp, ta có thể suy ra sự tương ứng giữa ngữ nghĩa thuộc tính ADT và những xác nhận. Tiền điều kiện của ADT xuất hiện lại như những mệnh đề tiền điều kiện (precondition clauses) của các thủ tục tương ứng. Một tiên đề, bao gồm một hàm command và một hay nhiều hàm query, xuất hiện lại như những mệnh đề hậu điều kiện (postcondition clauses) trong những thủ tục tương ứng. Những tiên đề chỉ bao gồm những hàm query xuất hiện lại như những hậu điều kiện của những hàm tương ứng hoặc những mệnh đề của điều kiện bất biến. Tiên đề bao gồm những hàm khởi tạo xuất hiện lại trong hậu điều kiện của những thủ tục khởi tạo tương ứng. 64 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 11.3. Hàm trừu tượng Hình 11-1: Sự biến đổi giữa những đối tượng trừu tượng và cụ thể A là một ADT và C là một lớp được cài đặt từ A. Lúc này tương ứng với hàm trừu tượng af của A sẽ có hàm cụ thể cf trong lớp C. Mũi tên a mô tả cho sự trừu tượng hóa hàm, với mỗi đối tượng cụ thể (thể hiện của lớp), sự trừu tượng hoá này sẽ sinh ta một đối tượng trừu tượng (thể hiện của ADT). Những hàm trừu tượng này thường là từng phần. Sự tương ứng giữa lớp và ADT (cf ; a) = (a ; af) Trong đó dấu “;” là toán tử kết hợp giữa các hàm. Nói cách khác, nếu ta có hai hàm f và g thì f;g là hàm h sao cho h(x) = g(f(x)) với mọi x (f;g còn được viết dưới dạng g o f ) 65 Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Hai đường đứt khúc cùng chỉ đến đối tượng trừu tượng ABST_2. Kết quả vẫn như nhau ngay cả khi bạn: - Áp dụng sự biến đối cụ thể cf, sau đó trừu tượng hóa kết quả, sinh ra a(cf(CONC_1)). - Trừu tượng hóa trước, sau đó áp dụng sự biến đổi trừu tượng af, sinh ra af(a(CONC_1)). 11.4. Cài đặt nh ...