Wikipedia

Assertion (phát triển phần mềm)

Trong lập trình máy tính, đặc biệt là khi sử dụng mô phạm lập trình mệnh lệnh, assertion (có thể dịch là xác quyết) là một vị ngữ (tức hàm có giá trị Boolean lên không gian trạng thái, thường được biểu diễn dưới dạng mệnh đề logic bằng cách sử dụng biến số của chương trình) được kết nối với một điểm trong chương trình, mà luôn luôn phải tính giá trị[a] ra true tại điểm đó trong quá trình thực thi mã. Assertion có thể giúp đỡ lập trình viên trong việc đọc code, giúp trình biên dịch trong việc biên dịch code, hoặc giúp cho chương trình trong việc phát hiện ra các khiếm khuyết của chính nó trong run-time. Assertion có thể hiểu nôm na là "nhất quyết phải chính xác", hay "xác quyết".

Đối với việc phát hiện khiếm khuyết trong run-time, một số chương trình kiểm tra assertion bằng cách thực sự tính giá trị vị ngữ khi chúng chạy luôn. Sau đó, nếu vị ngữ đấy thực ra không phải là true – tức assertion bất thành[b] – thì chương trình sẽ coi bản thân là bị hỏng và thường sẽ chủ động crash hoặc ném ra ngoại lệ assertion bất thành.

Chi tiết sửa

Đoạn mã sau chứa hai assertion, x > 0 và x > 1, và chúng quả thực là true tại các điểm được chỉ định trong quá trình thực thi: 

x = 1;
assert x > 0;
x++;
assert x > 1;

Lập trình viên có thể sử dụng assertion để giúp trong việc đặc tả chương trình và để suy lý về tính đúng sai của chương trình. Ví dụ, điều kiện tiên quyết – tức assertion đặt ở phần đầu của đoạn code – xác định tập hợp trạng thái mà lập trình viên mong rằng dựa vào đó mã sẽ thực thi, và điều kiện hậu quyết – đặt ở phần cuối – mô tả trạng thái mong muốn khi kết thúc thực thi. Ví dụ:

x > 0 { x++ } x > 1

Ví dụ trên sử dụng loại ký pháp để kèm assertion được C. A. R. Hoare sử dụng trong bài viết năm 1969 của mình.[1] Loại ký pháp này không thể sử dụng được trong các ngôn ngữ lập trình dòng chính hiện có. Tuy nhiên, lập trình viên có thể kèm assertion unchecked[c] trong run-time bằng cách dùng tính năng chú thích của ngôn ngữ lập trình mà mình dùng. Ví dụ, trong C: 

x = 5;
x = x + 1;
// {x > 1}

Dấu ngoặc nhọn kèm trong comment giúp phân biệt cách sử dụng comment thế này với cách sử dụng thế khác.

Các thư viện cũng có thể cung cấp tính năng assertion. Ví dụ, trong C sử dụng glibc với hỗ trợ C99: 

#include <assert.h>

int f(void)
{
  int x = 5;
  x = x + 1;
  assert(x > 1);
}

Vài ngôn ngữ lập trình hiện đại có bao gồm checked assertion – tức câu lệnh được kiểm tra trong run-time hoặc đôi khi được kiểm tra tĩnh. Nếu assertion tính giá trị ra false trong run-time thì sẽ dẫn đến assertion bất thành, từ đó thường khiến việc thực thi được bỏ dở. Như vậy sẽ hướng được sự chú ý đến vị trí phát hiện ra sự bất nhất logic, và có lẽ càng tốt khi hướng được luôn đến cái hành trạng của chương trình mà đáng ra phải chạy được nếu không bị lỗi.

Sử dụng assertion giúp lập trình viên thiết kế, phát triển và suy lý về chương trình.

Sử dụng sửa

Trong các ngôn ngữ như Eiffel, assertion là một phần của quá trình thiết kế; còn các ngôn ngữ khác như C và Java thì sử dụng chúng chỉ để kiểm tra giả định trong run-time thôi. Trong cả hai trường hợp, assertion đều có thể được dùng để kiểm tra tính hợp lệ trong run-time nhưng cũng thường có thể được ẩn đi.

Assertion trong thiết kế theo khế ước sửa

Assertion có thể mang chức năng như một dạng tài liệu: nó có thể mô tả trạng thái mà code trông mong trước khi chạy (tức điều kiện tiên quyết), và trạng thái mà code mong muốn đưa ra khi chạy xong (tức điều kiện hậu quyết); nó còn có thể đặc tả lượng bất biến[d] của lớp nữa. Eiffel có tích hợp các assertion như vậy vào ngôn ngữ và tự động trích xuất chúng trở thành tài liệu cho lớp. Đây là một phần quan trọng của phương pháp thiết kế theo khế ước.[e]

Lối tiếp cận này cũng có hữu ích trong những ngôn ngữ không tường minh hỗ trợ nó: điểm lợi của việc sử dụng câu lệnh assertion chứ không dùng assertion trong comment đó là chương trình có thể kiểm tra assertion mỗi lần nó chạy; nếu assertion không còn thỏa thì có thể báo cáo lỗi. Điều này phòng ngừa chuyện code bị mất đồng bộ với assertion.

Assertion để kiểm tra run-time sửa

Assertion có thể được dùng để xác minh rằng giả định do lập trình viên tạo ra trong quá trình biên soạn chương trình vẫn giữ được tính hợp lệ khi chương trình được thực thi. Ví dụ: xem xét mã Java sau: 

 int total = countNumberOfUsers();
 if (total % 2 == 0) {
   // total là số chẵn
 } else {
   // total là số lẻ và không âm
   assert total % 2 == 1;
 }

Trong Java, % là toán tử lấy số dư (modulo), và trong Java, nếu toán hạng đầu tiên của nó là số âm, thì kết quả cũng có thể là số âm (không giống như modulo được dùng trong toán học). Ở đây, lập trình viên đã giả định rằng total không âm, do đó phần dư của phép chia cho 2 sẽ luôn là 0 hoặc 1. Assertion ở đây làm cho giả định này tường minh: hễ countNumberOfUsers trả về giá trị âm, thì tức là chương trình có thể có bug.[f]

Một ưu điểm chính yếu của kỹ thuật này đó là khi có lỗi xảy ra, nó sẽ được phát hiện ngay lập tức và một cách trực tiếp, chứ không phải để mãi sau mới phát hiện ra thông qua những tác dụng thường là không rõ ràng của lỗi. Vì sự bất thành của assertion thường báo cáo luôn vị trí code, nên người ta hay có thể định vị được lỗi mà không cần debug gì thêm.

Assertion đôi khi cũng được đặt ở những điểm mà sự thực thi đúng ra không có chuyện tới được. Ví dụ, assertion có thể được đặt ở tiểu cú[g] default của câu lệnh switch trong các ngôn ngữ như C, C++ và Java. Bất cứ trường hợp nào mà lập trình viên không chủ ý xử trí thì sẽ giơ lỗi và chương trình sẽ dừng ngang chứ không âm thầm tiếp tục trong trạng thái bị lỗi. Trong D, assertion như vậy được tự động thêm khi câu lệnh switch không chứa tiểu cú default.

Trong Java, assertion là một phần của ngôn ngữ kể từ phiên bản 1.4 đến giờ. Assertion bất thành sẽ kéo theo việc giơ AssertionError khi chương trình được chạy với các cờ thích hợp, nếu không đặt các cờ đấy thì các câu lệnh assertion sẽ được bỏ qua. Trong C, nó được thêm vào thông qua header tiêu chuẩn assert.h trong đó có định nghĩa assert(assertion). Trong C++, cả hai header assert.h và cassert đều cung cấp macro assert.

Sự nguy hiểm của assertion đó là nó có thể gây ra tác dụng phụ vì nó có thể thay đổi dữ liệu bộ nhớ hoặc thay đổi việc canh giờ của thread. Assertion nên được thực hiện cẩn thận để chúng không gây ra tác dụng phụ trên mã chương trình.

Kết cấu assertion trong ngôn ngữ cho phép dễ dàng phát triển dẫn động bằng kiểm thử[h] mà không cần sử dụng thư viện của bên thứ ba.

Assertion trong chu trình phát triển sửa

Trong chu trình phát triển, lập trình viên thường sẽ chạy chương trình với các assertion được bật. Khi sự bất thành assertion xảy ra, lập trình viên sẽ ngay lập tức được báo tin về vấn đề. Nhiều bản thực hiện assertion cũng sẽ ngưng thực thi chương trình: điều này hữu ích, vì nếu chương trình tiếp tục chạy sau khi xảy ra sự vi phạm assertion thì nó có thể làm hỏng trạng thái của mình và làm cho nguyên nhân của vấn đề khó xác định hơn. Bằng thông tin được assertion cung cấp (chẳng hạn như vị trí của chỗ bị bất thành và có thể là cả stacktrace, hoặc thậm chí là trạng thái chương trình đầy đủ nếu môi trường đấy hỗ trợ core dump hoặc nếu chương trình đấy đang chạy trong debugger), lập trình viên thường có thể khắc phục vấn đề. Do đó, assertion là một công cụ rất mạnh trong việc debug.

Assertion trong môi trường sản xuất sửa

Khi chương trình được triển khai vào sản xuất, assertion thường được tắt để tránh bất kỳ tác dụng phụ nào mà nó có thể mang. Trong một số trường hợp, assertion hoàn toàn vắng mặt trong code triển khai, chẳng hạn như trong assertion của C/C++ thông qua macro. Trong các trường hợp khác như Java chẳng hạn, assertion lại hiện diện trong code triển khai và có thể được bật lại bằng cờ tham số để debug.[2]

Assertion cũng có thể được sử dụng để hứa hẹn với trình biên dịch rằng một 'điều kiện biên' đã cho nào đó không thực sự có thể tới được, do đó cho phép trình biên dịch tiến hành các tối ưu hóa nhất định mà mặt khác ra không thể nào làm được. Trong trường hợp này, việc vô hiệu hóa assertion thực sự có thể làm giảm hiệu suất chương trình.

Assertion tĩnh sửa

Assertion mà được kiểm tra tại thời điểm biên dịch thì được gọi là assertion tĩnh.

Assertion tĩnh có tính hữu ích trong template metaprogramming của compile-time nói riêng, nhưng cũng có thể được dùng trong các ngôn ngữ mức thấp như C bằng cách đưa code bất hợp lệ vào nếu (và chỉ nếu) assertion chạy không được. C11 và C++11 có hỗ trợ assertion tĩnh một cách trực tiếp thông qua static_assert. Trong các phiên bản C trước đó, assertion tĩnh có thể được thực hiện ví dụ như sau: 

#define SASSERT(pred) switch(0){case 0:case pred:;}

SASSERT( BOOLEAN CONDITION );

Nếu phần (BOOLEAN CONDITION) tính giá trị ra false thì đoạn mã trên sẽ không biên dịch được bởi vì trình biên dịch sẽ không cho phép hai nhãn case có cùng một hằng số. Biểu thức boolean phải là một giá trị hằng số trong compile-time, ví dụ: (sizeof(int)==4) sẽ là một biểu thức hợp lệ trong ngữ cảnh đó. Kết cấu này không dùng được ở tầm vực tập tin (tức là không ở bên trong hàm), và vì vậy nó phải được bọc bên trong hàm.

Một cách phổ biến khác[3] để thực hiện assertion trong C là: 

static char const static_assertion[ (BOOLEAN CONDITION)
                  ? 1 : -1
                 ] = {'!'};

Nếu phần (BOOLEAN CONDITION) tính giá trị ra false thì đoạn mã trên sẽ không biên dịch được vì mảng không thể có độ dài âm. Nếu trong thực tế, trình biên dịch cho phép độ dài âm thì phần byte khởi tạo (phần '!') vẫn sẽ khiến ngay cả những trình biên dịch khoan dung nhất cũng phải phàn nàn. Biểu thức boolean phải là một giá trị hằng số trong compile-time, ví dụ: (sizeof(int) == 4) sẽ là một biểu thức hợp lệ trong ngữ cảnh đó.

D cung cấp assertion tĩnh bằng static assert.[4]

Vô hiệu hóa assertion sửa

Hầu hết ngôn ngữ đều cho phép bật hoặc tắt assertion một cách toàn cục, và đôi khi một cách đơn lẻ. Assertion thường hay được bật trong lúc phát triển và được tắt đi trong lúc thử nghiệm cuối cùng và trong bản phát hành cho khách hàng. Việc không kiểm tra assertion sẽ tránh được chi phí thực thi assertion (giả sử assertion không có tác dụng phụ nào) mà vẫn giữ được cùng kết quả dưới điều kiện bình thường. Còn dưới điều kiện bất thường, việc tắt kiểm tra assertion có thể có nghĩa là chương trình đúng ra phải bị dừng ngang thì sẽ tiếp tục chạy. Điều này đôi khi được ưng hơn.

Một số ngôn ngữ, bao gồm cả C và C++, có thể loại bỏ hoàn toàn các assertion tại compile-time bằng cách sử dụng preprocessor.

Tương tự, khởi chạy trình thông dịch Python với đối số "-O" (viết tắt của "optimize", tối ưu hóa) sẽ khiến trình tạo mã Python không sinh ra bất kỳ bytecode nào cho các assertion.[5]

Java yêu cầu truyền tùy chọn cho run-time engine thì mới bật được assertion. Không có tùy chọn đấy thì assertion sẽ được bỏ qua, song assertion vẫn luôn ở trong code trừ phi được quá trình tối ưu hóa của trình biên dịch JIT ở run-time loại bỏ đi hoặc được loại bỏ đi tại compile-time thông qua việc lập trình viên tự tay đặt từng assertion sau tiểu cú if (false).

Lập trình viên có thể xây dựng các chặng kiểm tra vào trong code của mình sao cho chúng luôn luôn hữu hoạt bằng cách lách qua hoặc thao túng cơ chế kiểm tra assertion bình thường của ngôn ngữ.

So sánh với phép xử trí lỗi sửa

Asssertion khác biệt với phép xử trí lỗi thường dùng. Assertion có tác dụng ghi chép lại các tình huống không thể nào về mặt logic và phát hiện ra lỗi lập trình: nếu điều không thể mà lại xảy ra, thì rõ ràng chương trình có vấn đề cơ bản gì đó. Điều này khác biệt hẳn với phép xử trí lỗi: hầu hết tình huống lỗi đều có thể xảy ra, mặc dù một số tình huống có thể cực kỳ khó mà xảy ra trong thực tế. Sử dụng assertion làm cơ chế xử trí lỗi đa dụng là điều không sáng suốt: assertion không hề cho phép hồi phục từ trạng thái lỗi; sự bất thành của assertion thường sẽ ngưng sự thực thi chương trình lại một cách đột ngột; và assertion còn thường hay bị vô hiệu hóa trong code sản xuất. Assertion cũng không hiển thị thông báo lỗi thân thiện với người dùng.

Xem xét ví dụ sau về việc sử dụng assertion để xử trí lỗi: 

  int *ptr = malloc(sizeof(int) * 10);
  assert(ptr);
  // rồi dùng ptr thế nào đó
  ...

Ở đây, lập trình viên nhận thức được rằng malloc sẽ trả về một con trỏ NULL nếu bộ nhớ không được cấp phát. Điều này có thể xảy ra: hệ điều hành không hề đảm bảo rằng mọi lời gọi tới malloc đều sẽ thành công. Nếu xảy ra lỗi hết bộ nhớ, chương trình sẽ ngay lập tức dừng ngang. Nếu không có assertion, chương trình sẽ tiếp tục chạy cho đến khi ptr được khử tham chiếu, và có thể còn lâu hơn, tùy thuộc vào phần cứng cụ thể đang được sử dụng. Miễn là assertion không bị vô hiệu hóa thì đảm bảo chương trình sẽ thoát ra ngay. Nhưng nếu mong muốn tác vụ được bất thành một cách yên ổn thì chương trình phải xử trí sự bất thành đó. Ví dụ: server nào đó có thể có nhiều máy khách, hoặc có thể giữ tài nguyên mà sẽ không được giải phóng sạch sẽ, hoặc nó có thể có những thay đổi chưa được commit để ghi vào kho dữ liệu. Trong những trường hợp như vậy, làm cho giao dịch bị bất thành (cùng với hồi phục về trạng thái trước lỗi) thì tốt hơn là đột ngột dừng ngang.

Một sai lầm khác là dựa dẫm vào tác dụng phụ của biểu thức được sử dụng làm đối số cho assertion. Ta nên luôn ghi nhớ rằng assertion có thể có lúc không hề được thực thi tí nào, vì nó chỉ có mỗi mục đích là xác minh rằng điều kiện nào đó nên luôn là true sẽ luôn luôn là true mà thôi. Bởi vậy, nếu chương trình được coi là không có lỗi và được phát hành thì assertion có thể được tắt đi và sẽ không còn được tính giá trị nữa.

Xem xét một phiên bản khác của ví dụ trước: 

 int *ptr;
 // Câu lệnh dưới đây chạy không được nếu malloc() trả về NULL,
 // nhưng khi biên dịch bằng -NDEBUG thì sẽ không được thực thi!
 assert(ptr = malloc(sizeof(int) * 10));
 // nếu biên dịch bằng -NDEBUG thì ptr sẽ không được khởi tạo ở đây!
 ...

Đây có vẻ là một cách trông rất thông minh để gán giá trị trả về của malloc vào ptr và kiểm tra xem nó có NULL hay không bằng đúng một bước, nhưng lời gọi malloc và việc gán vàoptr đều là tác dụng phụ của việc tính giá trị biểu thức tạo nên điều kiện assert. Khi tham số NDEBUG được truyền cho trình biên dịch, khi chương trình được coi là không có lỗi và được phát hành, câu lệnh assert() sẽ bị xóa, nên malloc() sẽ không được gọi, khiến cho ptr không được khởi tạo. Điều này có thể dẫn đến segmentation fault hoặc lỗi tương tự là con trỏ null, những lỗi này mãi về sau trong dòng thực thi chương trình mới xuất hiện, gây nên những bug có thể lác đác và rất khó lần theo. Lập trình viên đôi khi sử dụng phương cách tương tự là define VERIFY(X) để giảm thiểu vấn đề này.

Các trình biên dịch hiện đại có thể sẽ đưa ra cảnh báo khi bắt gặp đoạn mã như trên.[6]

Lịch sử sửa

Trong báo cáo năm 1947 của von Neumann và Goldstine về thiết kế của họ cho máy IAS, họ đã mô tả các thuật toán bằng cách sử dụng phiên bản sơ kỳ của lưu đồ, trong đó bao gồm khẳng định là: "Có lẽ đúng là mỗi khi C thực sự chạy đến một điểm nhất định trong biểu đồ lưu trình, một hoặc nhiều biến số ràng buộc với nhau sẽ tất yếu mang các giá trị cụ thể nhất định, hoặc mang các tính chất nhất định, hoặc thỏa mãn các tính chất nhất định với nhau. Thêm nữa, tại những điểm như vậy, chúng ta có thể chỉ ra tính hợp lệ của những sự hạn định này. Bởi lý do này, chúng ta sẽ biểu thị mỗi khu vực, mà trong đó tính hợp lệ của những sự hạn định như vậy được xác quyết, bằng một chiếc hộp đặc biệt, mà chúng ta gọi nó là chiếc hộp xác quyết."[i][7]

Alan Turing đã chủ trương dùng phương pháp assertion để chứng minh tính đúng đắn của chương trình. Trong buổi nói chuyện "Checking a Large Routine" tại Cambridge, ngày 24 tháng 6 năm 1949, Turing đề xuất: "Ta kiểm tra routine lớn theo ý là đảm bảo nó đúng bằng cách nào đây? Nhằm để người kiểm tra không phải bị tác vụ quá khó khăn, lập trình viên nên tạo một số lượng các xác quyết có tính minh xác mà có thể được kiểm tra riêng rẽ, và bằng cách đó tính đúng đắn của cả thảy chương trình dễ dàng đi theo".[i][8]

Xem thêm sửa

Ghi chú thuật ngữ sửa

  1. ^ Evaluate
  2. ^ Assertion failure
  3. ^ Không được thực thi khi chương trình chạy
  4. ^ Invariant
  5. ^ Design by contract
  6. ^ Căn nguyên gây lỗi
  7. ^ Clause
  8. ^ Test-driven programming
  9. ^ a b Assertion trong các trích đoạn này được dịch là "xác quyết"

Tham khảo sửa

  1. ^ C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, 1969. Pdf link.
  2. ^ Programming With Assertions, Enabling and Disabling Assertions
  3. ^ Jon Jagger, Compile Time Assertions in C, 1999.
  4. ^ “Static Assertions”. D Language Reference. The D Language Foundation. Truy cập ngày 16 tháng 3 năm 2022.
  5. ^ Official Python Docs, assert statement
  6. ^ “Warning Options (Using the GNU Compiler Collection (GCC))”.
  7. ^ Goldstine and von Neumann. "Planning and Coding of problems for an Electronic Computing Instrument" Lưu trữ 2018-11-12 tại Wayback Machine. Part II, Volume I, 1 April 1947, p. 12. "It may be true, that whenever C actually reaches a certain point in the flow diagram, one or more bound variables will necessarily possess certain specified values, or possess certain properties, or satisfy certain properties with each other. Furthermore, we may, at such a point, indicate the validity of these limitations. For this reason we will denote each area in which the validity of such limitations is being asserted, by a special box, which we call an assertion box."
  8. ^ Alan Turing. Checking a Large Routine, 1949; quoted in C. A. R. Hoare, "The Emperor's Old Clothes", 1980 Turing Award lecture. "How can one check a large routine in the sense of making sure that it's right? In order that the man who checks may not have too difficult a task, the programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole program easily follows"

Liên kết ngoài sửa

Lấy từ “https://vi.wikipedia.org/w/index.php?title=Assertion_(phát_triển_phần_mềm)&oldid=69481870”