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

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

Thêm vào BST

Báo xấu

107
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# giữa những hàm với những thuộc tính. Ví dụ, điều kiện bất biến của STACK2 có thể mô tả sự liên quan giữa thuộc tính empty và count như sau: empty = (count = 0) Trong ví dụ này, xác nhận về điều kiện bất biến liên quan đến một thuộc tính và một hàm. Nó không riêng là việc lặp lại xác nhận ở hậu điều kiện của hàm (empty). Một xác nhận sẽ trở nên hữu ích hơn nếu nó có liên quan đến nhiều...

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# - 5

Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# giữa những hàm với những thuộc tính. Ví dụ, điều kiện bất biến của STACK2 có thể mô tả sự liên quan giữa thuộc tính empty và count như sau: empty = (count = 0) Trong ví dụ này, xác nhận về điều kiện bất biến liên quan đến một thuộc tính và một hàm. Nó không riêng là việc lặp lại xác nhận ở hậu điều kiện của hàm (empty). Một xác nhận sẽ trở nên hữu ích hơn nếu nó có liên quan đến nhiều thuộc tính như ví dụ trên hoặc nhiều hơn một hàm. Tiếp theo, ta có một ví dụ tiêu biểu khác. Liên quan đến khái niệm tài khoản ngân hàng, ta giả sử có một lớp là BANK_ACCOUNT có các đặc tính như deposits_list, withdrawals_list và balance. Lúc đó, điều kiện bất biến của lớp này có thể là một mệnh đề như sau: consistent_balance: deposits_list.total – withdrawals_list.total = balance Hàm total cho biết giá trị tích lũy của danh sách những hoạt động (số tiền gửi hay số tiền rút). Ví dụ trên cho thấy tình trạng nhất quán giữa những giá trị có thể truy cập thông qua các thuộc tính deposits_list, withdrawals_list và balance. 9.2. Định dạng và các thuộc tính của điều kiện bất biến của lớp Về mặt cú pháp, một điều kiện bất biến của lớp là một xác nhận, nằm trong phần invariant, sau phần feature và trước end. class STACK4[G] creation …As in STACK2 ... feature ... As in STACK2 ... invariant count_non_negative: 0
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# consistent_with_array_size: capacity = representation.capacity empty_if_no_elements: empty = (count = 0) item_at_top: (count > 0) implies (representation item (count) = item) end Một điều kiện bất biến của lớp C là một bộ những xác nhận mà mỗi thể hiện của C sẽ thoả mãn tất cả những thời điểm bền vững (stable times). Những thời điểm bền vững là những thời điểm mà tại đây, thể hiện của lớp trong tình trạng có thể quan sát được: + Khi khởi tạo thể hiện, tức là sau khi thực thi !!a hoặc là !!a.make(…), a có kiểu là lớp C. + Trước và sau mỗi khi yêu cầu một thủ tục r của lớp thông qua lời gọi a.r(…). Hình vẽ sau sẽ chỉ ra thời gian tồn tại của một đối tượng Hình 9-1: Thời gian tồn tại của một đối tượng 50
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Vào lúc bắt đầu, tức là bên trái hình Hình 8-1, đối tượng không tồn tại. Đối tượng được sinh ra bởi câu lệnh !!a hay !!a.make(…) hoặc là do một clone. Sau đó, client sử dụng đối tượng thông qua các tham chiếu đến a có dạng a.f(…) với f là một tính năng của lớp sinh ra đối tượng. Và từ đó, đối tượng tồn tại ít nhất là cho đến khi việc thi hành kết thúc. Điều kiện bất biến là một thuộc tính đặc thù của những trạng thái được biểu diễn bởi những ô vuông màu xám trong hình Hình 8-1 (Ví dụ: S1). Những thời điểm bền vững (stable times) trong hình trên là những chỗ mà đối tượng có thể thấy được từ bên ngoài, nghĩa là client có thể áp dụng một tính năng nào đó cho nó, bao gồm: + Trạng thái kết quả của việc tạo một đối tượng (trong hình là S1). + Những trạng thái ngay trước và sau khi client thực hiện một lời gọi có dạng a.some_routine(…). 9.3. Điều kiện bất biến thay đổi Tuy có tên là điều kiện bất biến nhưng nó cũng không cần phải thoả mãn hết tại mọi thời điểm mặc dù trong ví dụ STACK4, nó vẫn đúng sau khi được khởi tạo. Trong những trường hợp tổng quát hơn, việc một thủ tục g vào lúc ban đầu vì cố thực hiện những mục đích của mình - tức là cố đạt được hậu điều kiện – mà có thể làm hủy đi điều kiện bất biến trong quá trình này (cũng như con người, việc cố gắng làm một cái gì đó hữu ích có thể phá vỡ trật tự đã được thiết lập của mọi thứ); nhưng sau đó, ở giai đoạn thực thi tiếp theo, thủ tục này không vi phạm quá nhiều điều kiện bất biến vốn có là hoàn toàn được chấp nhận. Trong vài tình trạng tức thời, ví dụ như trong những tình trạng được đánh dấu trên hình Hình 8-1, điều kiện bất biến sẽ không thể giữ được. Tuy nhiên, điều này vẫn có thể chấp nhận được miễn là thủ tục sẽ thiết lập lại điều kiện bất biến trước khi kết thúc việc thực thi của nó. 51
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 9.4. Ai phải bảo quản điều kiện bất biến? Những lời gọi đủ điều kiện, có dạng là a.f(…), thực hiện nhân danh cho một client, là những cái duy nhất luôn phải được bắt đầu và rời khỏi trong trạng thái thoả mãn điều kiện bất biến; không có quy định nào cho những lời gọi không đủ điều kiện có dạng f(…) thực thi trực tiếp bởi những client nhưng chỉ phục vụ như những công cụ hỗ trợ cho việc tiến hành những cái cần thiết của một lời gọi đủ điều kiện. Do đó, việc bắt buộc duy trì điều kiện bất biến chỉ được áp dụng cho những tính năng được xuất khẩu (export) ra ngoài hoặc là theo cách chung chung hoặc là có sự lựa chọn; một tính năng bí mật mà không client nào được sử dụng là tính năng mà không bị điều kiện bất biến nào ảnh hưởng. Sau đây là quy định định nghĩa chính xác khi nào một xác nhận được coi là một điều kiện bất biến đúng của một lớp: Quy định của điều kiện bất biến Một xác nhận I sẽ là một điều kiện bất biến đúng của một lớp C nếu và chỉ nếu nó thoả 2 điều kiện: + E1: Mọi thủ tục khởi tạo của C , khi được áp dụng cho những đối số thoả mãn tiền điều kiện của nó trong trạng thái những thuộc tính có giá trị mặc định, đều sẽ dẫn đến trạng thái thoả mãn I. + E2: Mọi thủ tục được export ra khỏi lớp, khi được áp dụng cho những đối số và một trạng thái thoả mãn cả I lẫn tiền điều kiện của thủ tục, đều sẽ dẫn đến trạng thái thoả mãn I. Chú ý, trong luật này: + Mọi lớp được coi như có một thủ tục khởi tạo, và được định nghĩa là null nếu nó không được chỉ định tường minh. 52
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# + Trạng thái của một đối tượng được định nghĩa bởi tất cả những trường của nó (tức là những giá trị của các thuộc tính của lớp ứng với một thể hiện cụ thể). + Tiền điều kiện của thủ tục có thể liên quan đến trạng thái đầu tiên và những đối số. + Hậu điều kiện có thể liên quan đến trạng thái cuối, trạng thái đầu (thông qua khái niệm old) và trong trường hợp là hàm thì giá trị trả về (nếu có) được định nghĩa trước bởi thực thể Result. + Điều kiện bất biến có thể chỉ liên quan đến trạng thái. Những xác nhận có thể là những hàm nhưng những hàm như vậy là một tham chiếu gián tiếp đến các thuộc tính tức các trạng thái. Ta có thể dùng quy định về điều kiện bất biến như một cơ sở để trả lời câu hỏi: “Sẽ có ý nghĩa gì nếu điều kiện bất biến gây xâm phạm trong tiến trình thực thi của hệ thống?” Trước đây, chúng ta đã thấy rằng những dấu hiệu xâm phạm của một tiền điều kiện là một lỗi (một “bug”) ở khách hàng, còn xâm phạm ở hậu điều kiện là do lỗi ở người cung cấp. Thật ra, những điều kiện bất biến cũng là những hậu điều kiện. Chính thuộc tính này giúp ta biết được những gì sẽ nhận được. 9.5. Vai trò của những điều kiện bất biến của lớp trong kỹ thuật xây dựng phần mềm Thuộc tính E2 chỉ ra rằng chúng ta có thể xem điều kiện bất biến là phần được thêm vào một cách không tường minh cho cả tiền và hậu điều kiện của mỗi thủ tục được export ra ngoài. Do đó, về nguyên tắc, khái niệm điều kiện bất biến là không cần thiết vì không có nó ta vẫn làm việc tốt hoặc là chỉ việc mở rộng tiền và hậu điều kiện của tất cả thủ tục trong lớp là được. Tuy nhiên, không phải vậy. Dù việc có thêm điều kiện bất biến làm phức tạp những văn bản thủ tục, nhưng quan trọng hơn, ý nghĩa sâu xa của điều kiện bất biến là nó vượt khỏi những thủ tục riêng và được áp dụng cho cả một lớp. Thật sự, điều kiện bất biến không chỉ dùng để phục vụ cho những thủ tục viết trong lớp mà còn có thể sử dụng được khi ta có nhu cầu thêm mới sau đó. Vì vậy, điều kiện bất biến có 53
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# thể kiểm soát được cả những phần mở rộng của lớp. Điều này sẽ được thể hiện rõ trong những quy định về việc kế thừa. Trong phát triển phần mềm, sự thay đổi là một điều tất yếu mà chúng ta phải chấp nhận, chỉ là ta phải cố gắng điều chỉnh nó. Một vài lĩnh vực của hệ thống phần mềm như những thành phần riêng biệt, những lớp có thể thay đổi nhanh hơn những cái khác. Đặc biệt, việc thêm vào, bớt đi hay thay đổi những đặc tính là một hiện tượng thường xuyên và bình thường. Trong quá trình dễ thay đổi này, việc cứ bám mãi vào những thuộc tính mặc dù nó có thể thay đổi sẽ gây khó khăn cho việc đảm bảo toàn bộ hệ thống được duy trì vĩnh viễn. Nhưng với điều kiện bất biến, nó không gây khó khăn cho ta khi muốn thay đổi vì chúng giữ những ràng buộc ngữ nghĩa cơ bản được áp dụng cho một lớp. Ví dụ STACK2 đã minh họa được những ý kiến cơ bản, nhưng để đánh giá được toàn bộ những ích lợi của điều kiện bất biến thì ta phải theo dõi thêm những ví dụ tiếp theo. Khái niệm về điều kiện bất biến là một trong số những khái niệm nổi trội nhất mà ta học được từ phương pháp hướng đối tượng. Chỉ khi nào ta kế thừa những điều kiện bất biến (của một lớp do chính mình viết) hay đọc và hiểu nó (từ một lớp của người khác) thì ta mới có thể thực sự cảm nhận được lớp đó là gì. 9.6. Những điều kiện bất biến và hợp đồng Những điều kiện bất biến sẽ được hiểu rõ hơn khi đưa nó vào ngữ cảnh hợp đồng. Những hợp đồng giữa người với nhau thường liên quan đến những quy tắc chung được áp dụng cho mọi khế ước của một mục nào đó; ví dụ như những quy định về việc phân chia vùng của thành phố được áp dụng cho tất cả hợp đồng xây dựng nhà. Những điều kiện bất biến cũng đóng vai trò như thế trong hợp đồng phần mềm: điều kiện bất biến của một lớp ảnh hưởng đến tất cả hợp đồng giữa một thủ tục của một lớp và một đối tượng sử dụng lớp đó. Trong phần trên, ta xem những điều kiện bất biến như một cái gì đó được thêm vào cho tiền và hậu điều kiện của mọi thủ tục được export ra ngoài. Coi body là phần thân của thủ tục (là tập hợp những câu lệnh trong phần do), pre là tiền điều 54
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# kiện, post là hậu điều kiện và INV là điều kiện bất biến của lớp. Khi ấy, yêu cầu về tính đúng đắn trong thủ tục có thể được biểu diễn thông qua những khái niệm đã được giới thiệu trước đây là: {INV and pre} body {INV and post} (Câu lệnh trên có nghĩa là: bất cứ sự thi hành nào trong phần body, bắt đầu với bất kỳ trạng thái nào của INV và pre thì sẽ kết thúc trong trạng thái thoả mãn INV và post) Như vậy, có một câu hỏi dành cho người cung cấp tức người đã viết phần body: điều kiện bất biến là những tin tốt hay xấu, nó làm cho công việc dễ hơn hay khó hơn? Để trả lời được điều này thì bạn phải hiểu được ý nghĩa của cuộc thảo luận đầu tiên về ý nghĩa của tiền và hậu điều kiện đối với người làm công và người làm chủ. Thực chất, điều kiện bất biến cũng vậy. Nó có thể là tin tốt mà cũng có thể là tin xấu. Đối với người xin việc lười biếng, họ muốn có một tiền điều kiện mạnh và một hậu điều kiện yếu. Ở đây, thêm INV vào làm cho tiền và hậu điều kiện mạnh hơn hoặc ít nhất cũng là bằng với ban đầu. Cái này xuất phát từ quy tắc logic: a và b luôn luôn hàm ý a, điều này có thể nói là nó mạnh hơn hay bằng a. Vì vậy, nếu bạn chịu trách nhiệm thực hiện phần body, thì điều kiện bất biến sẽ: + Làm cho công việc của bạn dễ hơn nếu thêm vào tiền điều kiện pre vì trạng thái đầu tiên còn phải thỏa mãn thêm INV. Như vậy, sẽ giới hạn hơn những trường hợp có thể gặp phải. + Làm cho công việc của bạn khó hơn nếu thêm vào hậu điều kiện chính thức post vì bạn phải bảo đảm trạng thái cuối còn phải thoả mãn thêm INV. Những ý kiến này là đáng tin với cách nhìn điều kiện bất biến là một tình trạng nhất quán chung được dùng cho lớp như một tổng thể. Do đó, nó cũng được dùng cho tất cả các thủ tục của lớp. Khi là tác giả của một thủ tục như thế, bạn sẽ thấy có lợi khi điều kiện này đúng vào lúc bắt đầu thủ tục, nhưng bạn phải bảo đảm 55
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# rằng thủ tục sẽ thoả mãn điều kiện này một lần nữa lúc kết thúc để thủ tục tiếp theo thực thi trên cùng một đối tượng lại thấy việc này là có lợi lần nữa. Trong lớp BANK_ACCOUNT ở trên, mệnh đề điều kiện bất biến: deposits_list.total – withdrawals_list.total = balance là một ví dụ tốt. Nếu bạn phải thêm một thủ tục vào lớp, mệnh đề này đảm bảo những đặc tính deposits_list, withdrawals_list và balance có những giá trị nhất quán. Vì vậy, bạn không cần kiểm tra thuộc tính này (và như thế, sau khi xem, chúng ta cũng không phải kiểm tra nó). Nhưng nó cũng có nghĩa là bạn phải viết thủ tục, để mà, với bất cứ cái gì khác nó làm, nó cũng sẽ rời khỏi đối tượng trong trạng thái thỏa mãn thuộc tính này lần nữa . Do thế, thủ tục withdraw dùng để ghi một thao tác rút tiền sẽ không chỉ cập nhật withdrawals_list mà nó cũng phải cập nhật giá trị của balance nếu balance là một thuộc tính để lấy số tiền gửi vào tài khoản và khôi phục lại điều kiện bất biến, bảo đảm bất kỳ thủ tục nào khác được gọi sau đó của cùng một đối tượng cũng sẽ có thể thi hành dễ dàng. Không chỉ là một thuộc tính mà balance còn có thể là một hàm mà trong đó nó sẽ tính toán và trả về giá trị của: deposits_list.total – withdrawals_list.total Trong trường hợp này, thủ tục withdraw không cần làm bất cứ gì đặc biệt để có thể duy trì điều kiện bất biến. Khả năng chuyển đổi giữa hai khả năng này mà không làm ảnh hưởng đến khách hàng là một minh họa của nguyên tắc truy cập đồng bộ (uniform access). Ví dụ này chỉ ra rằng những điều kiện bất biến của lớp như một phương tiện vận chuyển đối với phần mềm một cách lịch thiệp cũng như nếu bạn sử dụng một loại tài nguyên chia sẻ thì bạn phải đưa nó lại cho người khác sau mỗi lần sử dụng. Chương 10: Khi nào một lớp là đúng? Phần này giúp chúng ta tiếp cận với những lý thuyết cơ bản. Ngay cả là đọc lần đầu tiên thì bạn cũng có thể tiếp cận được với những ý tưởng sẽ được trình bày 56
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# sắp tới vì nó tập trung vào những điểm chính yếu và rất quý báu khi sử dụng phương pháp kế thừa. 10.1. Tính đúng đắn của một lớp Với những tiền điều kiện, hậu điều kiện và điều kiện bất biến, ta có thể định nghĩa một cách chính xác một lớp đúng đắn là thế nào. Thật ra, cơ sở để định nghĩa tính đúng đắn của một lớp đã được trình bày ngay từ đầu luận văn: một lớp, giống như bất kỳ một thành phần phần mềm nào khác, chỉ có thể được đánh giá là đúng hay không đúng khi nó gắn liền với một đặc tả nào đó. Như vậy, những tiền điều kiện, hậu điều kiện và điều kiện bất biến chính là những thông tin mà ta có thể thêm vào phần đặc tả của lớp. Điều này cung cấp một cơ sở mà dựa vào đó, ta có thể đánh giá tính đúng đắn: một lớp là đúng nếu và chỉ nếu những cài đặt của nó trong thân của thường trình phù hợp với những tiền điều kiện, hậu điều kiện và điều kiện bất biến. Khái niệm {P}A{Q} được giới thiệu từ đầu giúp cho việc biểu diễn điều này được chính xác. Hãy nhớ ý nghĩa của một công thức đúng đắn là: bất cứ khi nào A được thực thi trong trạng thái thỏa P thì sự thực thi này sẽ kết thúc trong trạng thái thỏa Q. Coi C là một lớp, INV là những điều kiện bất biến của lớp. Với mọi thường trình r của lớp, gọi prer(xr) và postr(xr) là tiền điều kiện và hậu điều kiện của nó, xr là những tham số có thể của r, mà cả tiền điều kiện và hậu điều kiện đều có thể trỏ đến. (Nếu trong phần thường trình, cả tiền điều kiện hoặc hậu điều kiện đều thiếu thì prer hoặc postr là True). Gọi Bodyr là thân của thường trình r. Cuối cùng, DefaultC biểu diễn cho việc xác nhận những thuộc tính của C có giá trị mặc định cùng với kiểu của chúng. Ví dụ, DefaultSTACK2 được nói đến trong lớp ngăn xếp trước là một xác nhận: representation = Void capacity = 0 count = 0 57
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Những khái niệm này cho phép ta có một định nghĩa chung về tính đúng đắn của lớp: Định nghĩa: tính đúng đắn của lớp Một lớp là đúng với những xác nhận của nó nếu và chỉ nếu: + C1: Với bất kỳ bộ tham số hợp lệ xp nào của thủ tục khởi tạo p thì: {DefaultC and prepp(xp)} Bodyp {postp(xp) and INV} + C2: Với mọi thường trình r được export ra ngoài và bất kỳ bộ tham số hợp lệ xr nào thì: {prepr(xr) and INV} Bodyr {postr(xr) and INV} Quy định này thật sự là một khai báo toán học của lược đồ thông tin trước đây biểu diễn chu kỳ sống của một đối tượng điển hình. Ta hãy cùng xem lại ví dụ về BANK_ACCOUNT: Hình 10-1: Thời gian tồn tại của một đối tượng 58
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# Điều kiện C1 nghĩa là: bất kỳ thủ tục khởi tạo nào (ứng với hình Hình 9-1 trên là make), khi được gọi với những tiền điều kiện được thỏa mãn của nó thì phải trả về được một trạng thái khởi đầu (trong hình trên là S1) thỏa mãn điều kiện bất biến và hậu điều kiện của thủ tục đó. Điều kiện C2 diễn tả rằng bất kỳ thường trình r nào được export (ứng với hình trên là f và g), nếu được gọi trong trạng thái (S1, S2 hay S3) thỏa mãn cả tiền điều kiện và điều kiện bất biến của nó, thì phải kết thúc trong trạng thái thỏa mãn cả hậu điều kiện và điều kiện bất biến của nó. Như vậy, luật C1 là một bước cơ bản của việc dẫn nhập, nói rằng điều kiện bất biến giữ tất cả những đối tượng mới sinh ra là kết quả trực tiếp của một câu lệnh khởi tạo. Luật C2 là một bước dẫn nhập mà thông qua đó, ta quyết định nếu có một thế hệ những thể hiện nào đó thỏa mãn điều kiện bất biến thì thế hệ kế tiếp - tức là một bộ những thể hiện thu được do áp dụng những đặc tính được export của những thành viên trong thế hệ hiện tại – cũng sẽ thỏa mãn nó. Việc bắt đầu từ những đối tượng mới sinh ra và đi từ thế hệ này qua thế hệ khác thông qua những đặc tính được export, ta thu được toàn bộ những thể hiện có thể của một lớp cho phép ta quyết định rằng tất cả thể hiện đó có thỏa mãn điều kiện bất biến hay không. Có 2 ý kiến về mặt thực tiễn như sau: + Nếu một lớp không có mệnh đề creation, ta có thể xem như nó có một thủ tục khởi tạo không tường minh là nothing với một thân rỗng. Áp dụng luật C1 cho Bnothing với ý nghĩa là DefaultC phải bao gồm INV: những giá trị mặc định phải thỏa mãn điều kiện bất biến. + Một yêu cầu có dạng {P}A{Q} không thực thi A trong bất kỳ trường hợp nào mà P không thoả mãn lúc ban đầu. Do đó, hợp đồng sẽ không bị ràng buộc với thường trình nếu client không đáp ứng được những yêu cầu có liên quan với giao tác. Theo đó, định nghĩa tính đúng đắn của lớp không cho phép những thường trình thực thi khi nó vi phạm tiền điều kiện hay điều kiện bất biến. 59
Tìm hiểu công nghệ Design By Contract và Xây dựng công cụ hỗ trợ cho C# 10.2. Vai trò của những thủ tục khởi tạo Thảo luận về điều kiện bất biến sẽ cho ta cái nhìn sâu hơn về khái niệm của thủ tục khởi tạo. Một điều kiện bất biến của lớp biểu diễn một bộ những thuộc tính mà những đối tượng (những thể hiện của lớp) phải thỏa mãn tại những thời điểm ổn định trong thời gian sống của chúng. Đặc biệt, những thuộc tính này phải được giữ trước khi thể hiện được khởi tạo. Cơ cấu cấp phát đối tượng chuẩn khởi tạo những trường với những giá trị mặc định của những kiểu thuộc tính tương ứng; những giá trị này có thể thỏa mãn hay không điều kiện bất biến. Nếu không, một thủ tục khởi tạo đặc biệt sẽ được yêu cầu để gán giá trị cho những thuộc tính này để chúng thoả mãn điều kiện bất biến. Vì vậy, khởi tạo có thể xem như là một thao tác đảm bảo cho tất cả thể hiện của một lớp được bắt đầu cuộc sống của chúng với một chế độ đúng – tức là thỏa mãn được điều kiện bất biến. Việc biểu diễn đầu tiên của những thủ tục khởi tạo được giới thiệu như một cách để trả lời cho câu hỏi hết sức tầm thường là: làm sao để viết đè những quy luật khởi tạo mặc định khi chúng không thích hợp cho một lớp đặc biệt nào đó, hoặc là trong trường hợp ta muốn cung cấp cho những client nhiều hơn một cơ cấu khởi tạo? Nhưng chỉ với sự giới thiệu về những điều kiện bất biến và những thảo luận một cách lý thuyết cùng với áp dụng luật C1 thì ta chỉ có thể kết luận về vai trò sâu hơn của những thủ tục khởi tạo là: chúng đảm bảo cho bất kỳ thể hiện nào của lớp khi bắt đầu thời gian sống phải thỏa mãn những quy định cơ bản thuộc về lớp đó - tức là thoả mãn những điều kiện bất biến của lớp đó. 10.3. Xem lại về mảng Thư viện lớp ARRAY đã được tóm tắt trong chương trước. Tuy nhiên, bây giờ là lúc đưa ra định nghĩa chính xác cho nó. Khái niệm mảng luôn đòi hỏi phải có tiền điều kiện, hậu điều kiện và một điều kiện bất biến. Đây là một bản phác thảo cùng với những xác nhận. Những tiền điều kiện là cần thiết trong việc truy cập và điều chỉnh mảng với quy định là chỉ số mảng phải 60