Ý tưởng về tính đúng đắn của Tony Hoare: Từ logic đến mã an toàn

Tại sao “tính đúng đắn” hơn là “trông như hoạt động”

Khi người ta nói một chương trình “đúng”, họ thường có ý: “Tôi chạy nó vài lần và kết quả trông ổn.” Đó là một tín hiệu hữu ích — nhưng không phải là tính đúng đắn. Nói đơn giản, tính đúng đắn nghĩa là chương trình thỏa mãn đặc tả: với mọi đầu vào hợp lệ, nó cho ra kết quả yêu cầu và tôn trọng các quy tắc về thay đổi trạng thái, thời gian và lỗi.

Vấn đề là “thỏa mãn đặc tả” khó hơn nghe có vẻ.

Tại sao tính đúng đắn thực sự khó

Đầu tiên, các đặc tả thường mơ hồ. Yêu cầu sản phẩm có thể nói “sắp xếp danh sách”, nhưng điều đó có nghĩa là sắp xếp ổn định không? Còn giá trị trùng lặp, danh sách rỗng hay phần tử không phải số thì sao? Nếu đặc tả không nói rõ, mỗi người sẽ giả định khác nhau.

Thứ hai, các trường hợp biên không hiếm — chúng chỉ ít khi được thử. Giá trị null, tràn số, sai lệch một chỉ số, chuỗi hành vi người dùng bất thường và thất bại bên ngoài không mong đợi có thể biến “trông ổn” thành “thất bại ở production”.

Thứ ba, yêu cầu thay đổi. Một chương trình có thể đúng theo đặc tả hôm qua nhưng sai theo đặc tả hôm nay.

Mong đợi gì từ phần còn lại của bài viết này

Đóng góp lớn của Tony Hoare không phải là kêu gọi chứng minh mọi thứ mọi lúc. Ý chính là chúng ta có thể rõ ràng hơn về việc mã phải làm gì — và suy luận về nó theo cách có kỷ luật.

Trong bài này, chúng ta theo ba chủ đề liên kết:

• Hoare logic: suy luận nhẹ, có cấu trúc dùng tiền điều kiện (preconditions) và hậu điều kiện (postconditions).
• Quicksort: một thuật toán quen thuộc cho thấy các bước “hiển nhiên” nhỏ (như phân hoạch) cần được suy nghĩ cẩn thận.
• Tư duy an toàn: coi tính đúng đắn như trách nhiệm thực tế khi thất bại có hậu quả thật.

Hầu hết đội sẽ không viết bằng chứng hình thức đầy đủ. Nhưng ngay cả tư duy “kiểu bằng chứng” một phần cũng giúp tìm bug dễ hơn, làm cho review sắc nét hơn và hành vi rõ ràng hơn trước khi giao mã.

Tony Hoare tóm tắt: các ý tưởng đến với mã hàng ngày

Tony Hoare là một trong những nhà khoa học máy tính hiếm hoi mà công trình không chỉ nằm trên báo hay trong lớp học. Ông di chuyển giữa học thuật và công nghiệp, và ông quan tâm tới câu hỏi thực tế mà mọi đội vẫn gặp: làm sao chúng ta biết chương trình làm đúng như ta nghĩ — đặc biệt khi giá trị đặt cược cao?

Những đóng góp quan trọng cho bài viết này

Bài viết tập trung vào vài ý của Hoare thường xuất hiện trong code:

• Hoare logic: cách mô tả hành vi chương trình bằng preconditions, postconditions, và Hoare triple {P} C {Q}.
• Bất biến vòng lặp: thói quen có kỷ luật để suy luận về vòng lặp hơn là “chạy trên máy tôi thì được”.
• Quicksort (đặc biệt là bước phân hoạch): ví dụ nổi tiếng cho thấy khai báo chính xác nhỏ có thể làm sáng tỏ nhiều thứ.
• Tư duy an toàn: tính đúng đắn không phải tính năng xa xỉ; nó có thể là khác biệt giữa phiền toái và tổn hại.

Bài viết này sẽ không làm gì

Bạn sẽ không thấy toán học sâu ở đây, và chúng ta sẽ không cố gắng làm bằng chứng kiểm tra bởi máy cho Quicksort. Mục tiêu là giữ các khái niệm dễ tiếp cận: đủ cấu trúc để làm rõ suy luận, mà không biến review thành một buổi thảo luận cao học.

Tại sao công trình của ông ảnh hưởng lập trình hàng ngày

Ý tưởng của Hoare dịch thành các quyết định bình thường: giả định một hàm phụ thuộc gì, nó đảm bảo gì cho caller, điều gì phải đúng ở giữa một vòng lặp, và làm sao phát hiện thay đổi “gần đúng” trong review. Ngay cả khi bạn không viết {P} C {Q} rõ ràng, suy nghĩ theo khuôn này cải thiện API, test và chất lượng thảo luận về mã khó.

“Tính đúng đắn” có nghĩa gì trong thực hành

Quan điểm của Hoare nghiêm khắc hơn “chạy vài ví dụ là đủ”: tính đúng đắn là đáp ứng một lời hứa đã thống nhất, không phải trông đúng trên vài mẫu nhỏ.

Yêu cầu vs. đặc tả vs. hiện thực

• Yêu cầu (requirements) là nhu cầu kinh doanh bằng ngôn ngữ thông thường (những gì stakeholders muốn).
• Đặc tả (specification) là phiên bản chính xác, có thể kiểm tra của nhu cầu đó (hàm phải làm gì).
• Hiện thực (implementation) là mã bạn viết (nó làm thế nào).

Lỗi thường xảy ra khi đội bỏ qua bước ở giữa: nhảy từ yêu cầu thẳng sang code, để lời hứa mơ hồ.

Tính đúng đắn một phần vs. toàn bộ

Hai khẳng định thường bị trộn:

• Tính đúng đắn một phần: Nếu mã trả về, kết quả là đúng.
• Tính đúng đắn toàn bộ: Mã trả về và kết quả là đúng (khả năng kết thúc là một phần của khẳng định).

Với hệ thống thực tế, “không bao giờ hoàn thành” có thể có hại như “hoàn thành nhưng trả về sai”.

Tính đúng đắn luôn phụ thuộc vào giả định

Các tuyên bố về tính đúng đắn không bao giờ phổ quát; chúng dựa trên giả định về:

• Đầu vào (ví dụ: danh sách vừa trong bộ nhớ, phần tử có thể so sánh)\n- Ràng buộc (ví dụ: giới hạn thời gian, phạm vi số nguyên)\n- Môi trường (ví dụ: concurrency, lỗi I/O, cấu hình)

Việc nêu rõ giả định biến “chạy trên máy tôi” thành cái mà người khác có thể suy luận.

Một ví dụ đặc tả nhỏ

Xét hàm sortedCopy(xs).

Một đặc tả hữu ích có thể là: “Trả về một danh sách mới ys sao cho (1) ys được sắp tăng dần, và (2) ys chứa chính xác các phần tử của xs (số lượng tương ứng), và (3) xs không bị thay đổi.”

Bây giờ “đúng” nghĩa là mã thỏa ba điểm đó dưới các giả định đã nêu — không chỉ là kết quả trông có vẻ sắp xếp trong một vài test nhanh.

Cơ bản về Hoare logic: preconditions, postconditions, triple

Hoare logic là cách nói về mã giống như một hợp đồng: nếu bạn bắt đầu ở trạng thái thỏa một số giả định, và bạn chạy đoạn mã này, bạn sẽ kết thúc ở trạng thái thỏa một số đảm bảo.

Ký hiệu trung tâm là Hoare triple:

{precondition} program {postcondition}

Preconditions: điều bạn giả sử

Precondition nêu điều phải đúng trước khi đoạn mã chạy. Đây không phải điều bạn hy vọng; là điều mã cần.

Ví dụ: giả sử một hàm trả về trung bình của hai số mà không kiểm tra tràn.

• Precondition: a + b vừa trong kiểu số nguyên
• Program: avg = (a + b) / 2
• Postcondition: avg bằng trung bình toán học của a và b

Nếu precondition không đúng (tràn có thể xảy ra), lời hứa postcondition không còn áp dụng. Triple buộc bạn nói điều đó rõ ràng.

Postconditions: điều bạn đảm bảo

Postcondition nêu điều sẽ đúng sau khi mã chạy — với điều kiện precondition được thỏa. Postcondition tốt cụ thể và có thể kiểm tra. Thay vì “kết quả hợp lệ”, hãy nói rõ “hợp lệ” nghĩa là gì: đã sắp xếp, không âm, trong giới hạn, không thay đổi ngoài các trường cụ thể, v.v.

Gán và chuỗi bước (không quá ký hiệu)

Hoare logic mở rộng từ các câu nhỏ tới khối code nhiều bước:

• Gán thay đổi trạng thái một cách chính xác. Khi x = x + 1, suy luận là: sau đó những điều gì về x đúng?
• Chuỗi bước (“làm cái này, rồi làm cái kia”) nối các đảm bảo: nếu bước 1 thiết lập precondition cho bước 2, khối tổng thể dễ tin cậy hơn.

Ý chính không phải rắc dấu ngoặc nhọn khắp nơi. Là làm cho ý định dễ đọc: giả định rõ, kết quả rõ, bớt các cuộc trò chuyện “trông như hoạt động” trong review.

Bất biến vòng lặp mà đội thật sự có thể viết

Bất biến vòng lặp là một phát biểu đúng trước khi vòng lặp bắt đầu, vẫn đúng sau mỗi lần lặp, và còn đúng khi vòng kết thúc. Ý tưởng đơn giản mà lợi ích lớn: nó thay thế “trông như được” bằng một tuyên bố bạn có thể kiểm tra từng bước.

Tại sao bất biến ngăn suy luận sáo rỗng

Không có bất biến, review thường kiểu: “Chúng ta duyệt danh sách và dần dần sửa.” Bất biến buộc sự chính xác: điều gì chính xác đã đúng bây giờ, dù vòng chưa xong? Khi bạn nói rõ được điều đó, lỗi sai lệch một chỉ số và thiếu trường hợp sẽ dễ thấy, vì chúng làm bất biến bị phá vỡ.

Mẫu bất biến bạn có thể tái dùng

Hầu hết mã hàng ngày có thể dùng vài mẫu tin cậy.

1. Giới hạn / an toàn chỉ số

Giữ chỉ số trong khoảng an toàn.

• 0 <= i <= n
• low <= left <= right <= high

Loại bất biến này tốt để ngăn truy cập ngoài mảng và làm cho suy luận về mảng cụ thể.

2. Phần đã xử lý vs chưa xử lý

Chia dữ liệu thành vùng “xong” và “chưa”.

• “Mọi phần tử trong a[0..i) đã được kiểm tra.”
• “Mọi phần tử chuyển vào result thỏa predicate lọc.”

Điều này biến tiến độ mơ hồ thành một hợp đồng rõ ràng về “đã xử lý”.

3. Tiền tố đã sắp/xếp (hoặc phân vùng tiền tố)

Phổ biến trong sắp xếp, gộp, phân hoạch.

• “a[0..i) đã được sắp.”
• “Mọi phần tử trong a[0..i) là <= pivot, và mọi phần tử trong a[j..n) là >= pivot.”

Ngay cả khi toàn bộ mảng chưa sắp xong, bạn đã xác định rõ phần nào đã ổn.

Kết thúc vòng lặp nói theo ngôn ngữ đơn giản: một đại lượng giảm

Tính đúng đắn không chỉ là đúng; vòng phải kết thúc. Cách đơn giản lý luận là đặt tên một đại lượng giảm (variant) mỗi lần lặp và không thể giảm vô hạn.

Ví dụ:

• “n - i giảm 1 mỗi lần.”
• “Số phần tử chưa xử lý giảm.”

Nếu bạn không tìm được đại lượng giảm, bạn có thể đã phát hiện rủi ro thật sự: vòng vô hạn với một số đầu vào.

Quicksort làm ví dụ để suy luận về mã

Quicksort có lời hứa đơn giản: với một đoạn mảng, sắp xếp các phần tử theo thứ tự không giảm, không mất hay tạo giá trị mới. Hình dạng thuật toán dễ tóm tắt:

1. Chọn một pivot.
2. Phân hoạch đoạn để phần tử “nhỏ hơn pivot” nằm một bên và “lớn hơn pivot” nằm bên kia (với quy tắc cho “bằng”).
3. Đệ quy trên hai đoạn con.

Đây là ví dụ tốt cho tính đúng đắn vì nó đủ nhỏ để nắm trong đầu, nhưng đủ giàu để cho thấy suy luận không chính thức thất bại ở đâu. Một Quicksort “trông hoạt động” trên vài test ngẫu nhiên vẫn có thể sai với các đầu vào đặc biệt hoặc ở các điều kiện biên.

Những cạm bẫy làm vỡ cài đặt “hiển nhiên”

Một vài vấn đề gây hầu hết lỗi:

• Trùng lặp: nếu phân hoạch xử lý “bằng pivot” không nhất quán, bạn có thể rơi vào đệ quy vô hạn (đoạn con không nhỏ đi) hoặc phân hoạch vi phạm quy tắc.
• Đoạn rỗng hoặc một phần tử: base case phải chính xác; nếu không bạn sẽ truy cập ngoài chỉ số hoặc đệ quy vô hạn.
• Lệch một chỉ số: thuật toán phân hoạch thường dùng hai con trỏ; một so sánh hoặc tăng sai có thể bỏ sót phần tử hoặc hoán đổi ngoài phạm vi.

Cần chứng minh những gì thực sự

Để lập luận đúng theo kiểu Hoare, bạn thường tách bằng chứng thành hai phần:

• Tính đúng đắn của phân hoạch: sau khi phân hoạch, mọi phần tử bên trái thỏa quan hệ với pivot, mọi phần tử bên phải thỏa quan hệ ngược lại, và kết quả là một hoán vị của các phần tử ban đầu.
• Tính đúng đắn của đệ quy: các gọi đệ quy hoạt động trên các đoạn nhỏ hơn (kết thúc) và, nếu chúng sắp đúng các đoạn con, toàn bộ đoạn được sắp.

Việc tách này giữ suy luận có thể quản lý: làm phân hoạch đúng trước, rồi xây tính đúng đắn sắp trên đó.

Tính đúng đắn của phân hoạch: trái tim của Quicksort

Tốc độ Quicksort phụ thuộc vào một thủ tục nhỏ tưởng chừng đơn giản: partition. Nếu partition sai một chút, Quicksort có thể sắp sai, lặp vô hạn hoặc crash ở các trường hợp biên.

Hợp đồng của partition (những gì nó phải đảm bảo)

Ta dùng sơ đồ Hoare partition cổ điển (hai con trỏ tiến vào nhau).

Input: một đoạn mảng A[lo..hi] và một giá trị pivot được chọn (thường là A[lo]).

Output: một chỉ số p sao cho:

• mọi phần tử trong A[lo..p] là <= pivot
• mọi phần tử trong A[p+1..hi] là >= pivot

Chú ý điều không hứa: pivot không nhất thiết nằm ở p, và phần tử bằng pivot có thể ở cả hai bên. Điều đó ổn — Quicksort chỉ cần một tách đúng.

Bất biến then chốt khi quét và hoán đổi

Khi thuật toán tiến hai chỉ số — i từ trái, j từ phải — suy luận tốt tập trung vào những gì đã “khóa”. Một tập bất biến thực tế là:

• mọi phần tử trong A[lo..i-1] là <= pivot (bên trái sạch)
• mọi phần tử trong A[j+1..hi] là >= pivot (bên phải sạch)
• mọi thứ trong A[i..j] là chưa phân loại (chưa kiểm tra)

Khi ta thấy A[i] >= pivot và A[j] <= pivot, hoán đổi chúng giữ các bất biến đó và thu hẹp vùng chưa phân loại.

Các trường hợp biên cần che phủ

• Tất cả nhỏ hơn pivot: i chạy hết sang phải; partition vẫn phải kết thúc và trả p hợp lý.
• Tất cả lớn hơn pivot: j chạy sang trái; cùng mối quan tâm kết thúc.
• Nhiều phần tử bằng nhau: nếu so sánh không nhất quán (< vs <=), con trỏ có thể dừng lại. Sơ đồ của Hoare dựa vào quy tắc so sánh nhất quán để tiến độ tiếp tục.
• Đã sắp sẵn / sắp ngược: không nên phá vỡ hợp đồng, dù hiệu năng có giảm.

Có nhiều sơ đồ phân hoạch khác (Lomuto, Hoare, phân hoạch ba ngăn). Chìa khóa là chọn một, nêu hợp đồng của nó, và review mã theo hợp đồng đó một cách nhất quán.

Suy luận về đệ quy: base case và kết thúc

Đệ quy dễ tin hơn khi bạn trả lời rõ hai câu: khi nào dừng? và tại sao mỗi bước hợp lệ? Tư duy kiểu Hoare giúp vì buộc bạn nêu rõ điều gì phải đúng trước khi gọi, và điều gì sẽ đúng sau khi trả về.

Base case phải đúng

Hàm đệ quy cần ít nhất một base case nơi nó không gọi tiếp và vẫn thỏa kết quả hứa. Với sắp xếp, base case điển hình là “mảng độ dài 0 hoặc 1 đã được sắp”. Ở đây, “sắp” nên rõ: với quan hệ ≤, output là sắp nếu với mọi chỉ số i < j, ta có a[i] ≤ a[j]. (Tính giữ nguyên thứ tự của phần tử bằng nhau là tính chất riêng gọi là stability; Quicksort thường không ổn định trừ khi thiết kế để vậy.)

Bài toán con phải nhỏ lại

Mỗi bước đệ quy nên gọi trên input nhỏ hơn hẳn. “Nhỏ lại” là bằng chứng kết thúc: nếu kích thước giảm và không thể giảm dưới 0, bạn không thể đệ quy vô hạn.

Việc giảm cũng quan trọng cho an toàn ngăn xếp. Mã đúng vẫn có thể crash nếu độ sâu đệ quy quá lớn. Trong Quicksort, phân hoạch mất cân bằng có thể sản sinh đệ quy sâu. Đó là lời nhắc thực tế: chứng minh kết thúc và xem xét độ sâu trong thực tế.

Đúng trước, hiệu năng sau

Trường hợp xấu của Quicksort có thể xuống O(n²) khi phân hoạch rất mất cân bằng, nhưng đó là vấn đề hiệu năng — không phải lỗi tính đúng đắn. Mục tiêu suy luận là: giả sử phân hoạch giữ nguyên phần tử và tách theo pivot, việc đệ quy sắp các đoạn con nhỏ hơn hàm ý toàn bộ đoạn được sắp.

Tư duy theo kiểu bằng chứng và testing: chúng kết hợp thế nào

Testing và suy luận kiểu bằng chứng đều nhằm cùng mục tiêu — độ tin cậy — nhưng tới đó theo cách khác nhau.

Test tìm bug; suy luận loại trừ các lớp bug

Test rất tốt để bắt lỗi cụ thể: lệch chỉ số, thiếu trường hợp, regression. Nhưng bộ test chỉ lấy mẫu không gian đầu vào. Dù “100% coverage” cũng không có nghĩa là “tất cả hành vi đã được kiểm”, nó chủ yếu nghĩa là “tất cả dòng đã được thực thi”.

Suy luận kiểu bằng chứng bắt đầu từ đặc tả và hỏi: nếu các preconditions đúng, mã có luôn thiết lập postconditions không? Khi làm tốt, bạn không chỉ tìm một bug — thường loại bỏ cả một nhóm bug (như “truy cập mảng luôn trong giới hạn” hoặc “vòng không phá vỡ bất biến phân hoạch”).

Đặc tả tạo ra test tốt hơn

Một đặc tả rõ ràng là máy phát test.

Nếu postcondition nói “output được sắp và là một hoán vị của input”, bạn tự động có ý tưởng test:

• Biên: danh sách rỗng, một phần tử, đã sắp, sắp ngược.
• Bất biến: tính chất trung gian (ví dụ: phân hoạch giữ phần tử <= pivot ở trái).
• Đầu vào không hợp lệ: null, NaN, chỉ số ngoài phạm vi, comparator không nhất quán.

Đặc tả nói cho bạn biết “đúng” là gì, test kiểm tra thực tế có khớp không.

Test theo thuộc tính như cầu nối thực tế

Property-based testing nằm giữa bằng chứng và ví dụ. Thay vì chọn vài ca, bạn nêu thuộc tính và để công cụ sinh nhiều input.

Với sắp xếp, hai thuộc tính đơn giản nhưng mạnh là:

• Sortedness: kết quả ở thứ tự không giảm.
• Permutation: kết quả chứa chính xác các phần tử của input.

Những thuộc tính này là postconditions viết dưới dạng kiểm tra có thể chạy được.

Một workflow nhẹ đội có thể dùng

Thói quen nhẹ có thể mở rộng:

1. Viết đặc tả trước (preconditions, postconditions, bất biến chính).
2. Suy nghĩ về phần khó (vòng lặp, phân hoạch, biên đệ quy).
3. Biến đặc tả thành test (biên + property-based checks).
4. Giữ chúng cùng nơi trong code và review, để thay đổi sau này không lặng lẽ vi phạm ý định ban đầu.

Nếu muốn thể chế hoá, thêm “spec + notes suy luận + tests” vào template PR hoặc checklist review. (xem cũng blog/code-review-checklist.)

Nếu bạn dùng quy trình tạo mã từ giao diện chat, kỷ luật giống vậy còn quan trọng hơn. Trong Koder.ai, ví dụ, bạn có thể bắt đầu ở Planning Mode để khóa preconditions/postconditions trước khi sinh mã, rồi lặp với snapshot và rollback khi thêm property-based tests. Công cụ tăng tốc triển khai, nhưng đặc tả là thứ giữ cho “nhanh” không biến thành “dễ vỡ”.

Tư duy an toàn: tính đúng đắn có hậu quả đời thực

Tính đúng đắn không chỉ là “hàm trả về giá trị đúng”. Tư duy an toàn hỏi: những kết quả nào là không chấp nhận được, và làm sao ngăn chúng — ngay cả khi mã bị quá tải, sử dụng sai, hoặc hỏng một phần? Thực hành, an toàn là tính đúng đắn kèm hệ thống ưu tiên: một số thất bại chỉ khó chịu, số khác có thể gây tổn thất tài chính, mất riêng tư, hoặc tổn hại thể chất.

Nguy hại vs bug: tại sao hậu quả quan trọng

Một bug là lỗi trong mã hoặc thiết kế. Một hazard là tình huống có thể dẫn tới kết quả không chấp nhận được. Một bug có thể vô hại ở ngữ cảnh này nhưng nguy hiểm ở ngữ cảnh khác.

Ví dụ: một lệch một chỉ số trong gallery ảnh có thể gán nhầm nhãn; cùng lỗi trong máy tính liều lượng thuốc có thể gây hại cho bệnh nhân. Tư duy an toàn buộc bạn liên kết hành vi mã với hậu quả, không chỉ là “thỏa đặc tả”.

Kỹ thuật đơn giản ngăn hậu quả tồi tệ nhất

Bạn không cần phương pháp hình thức nặng để đạt lợi ích an toàn tức thời. Đội có thể áp dụng thói quen nhỏ, lặp lại:

• Fail-safe defaults: nếu hệ thống không chắc, chọn hành vi an toàn hơn. Ví dụ, từ chối truy cập khi kiểm tra phân quyền lỗi thay vì “cho phép khi có lỗi”.
• Validate input tại biên: coi input người dùng, nội dung file và dữ liệu mạng là không tin cậy. Kiểm tra kiểu, phạm vi, định dạng và bất biến sớm.
• Giới hạn và timeout: giới hạn bộ nhớ, kích thước yêu cầu, độ sâu đệ quy, số lần thử và thời gian thực thi. Nhiều sự cố là “mã đúng” chạy với input vô lý.

Những kỹ thuật này kết hợp tự nhiên với Hoare-style: bạn làm preconditions rõ (đầu vào chấp nhận được) và đảm bảo postconditions bao gồm thuộc tính an toàn (những gì không được xảy ra).

Đổi lấy: kiểm tra không miễn phí

Các kiểm tra vì an toàn tốn chi phí — CPU, độ phức tạp hoặc từ chối nhầm.

• Hiệu năng vs kiểm tra: đường dẫn nhanh có giá trị, nhưng biên quan trọng cần validation, rate limits, timeout.
• Khắt khe vs trải nghiệm: từ chối mọi input không hoàn hảo làm người dùng bực; chấp nhận mọi thứ có thể tạo mơ hồ và lỗ hổng. Thỏa hiệp thực tế là “khắt khe ở lõi, khoan dung ở rìa”, đồng thời log và đo tần suất các edge case.

Tư duy an toàn ít về chứng minh vẻ đẹp thuật toán mà nhiều về ngăn các chế độ thất bại bạn không chịu nổi.

Áp dụng tư duy Hoare trong code review

Code review là nơi tư duy tính đúng đắn đem lại lợi ích nhanh nhất, bởi bạn có thể phát hiện giả định thiếu sớm trước khi bug tới production. Động tác cốt lõi của Hoare — nêu điều gì phải đúng trước và điều gì sẽ đúng sau — chuyển thành các câu hỏi review dễ dùng.

Biến ý Hoare thành câu hỏi review

Khi đọc thay đổi, thử đóng khung mỗi hàm chính như một lời hứa nhỏ:

• Giả định (preconditions): điều gì phải đúng về input, trạng thái, môi trường? (ví dụ: “danh sách không rỗng”, “user đã xác thực”, “lock đang được giữ”).
• Đảm bảo (postconditions): điều gì đúng sau đó, bao gồm giá trị trả về và side effects? (ví dụ: “số dư giảm đi đúng số tiền”, “bản ghi được chèn đúng một lần”).
• Bất biến: điều gì phải còn đúng xuyên suốt vòng lặp, retry, hay workflow nhiều bước? (ví dụ: “processed_count ≤ total”, “tổng các khoản ghi nợ bằng tổng tín dụng tới lúc này”).
• Hành vi khi lỗi: khi có lỗi, hệ thống ở trạng thái an toàn chứ? Các cập nhật một phần có được rollback?

Thói quen đơn giản cho reviewer: nếu bạn không thể nói pre/post trong một câu, mã có thể cần cấu trúc rõ hơn.

“Contract comments” cho hàm quan trọng

Với hàm rủi ro hoặc trung tâm, thêm comment hợp đồng nhỏ ngay trên chữ ký. Giữ nó cụ thể: input, output, side effects và lỗi.

def withdraw(account, amount):
    """Contract:
    Pre: amount is an integer > 0; account is active.
    Post (success): returns new_balance; account.balance decreased by amount.
    Post (failure): raises InsufficientFunds; account.balance unchanged.
    """
    ...

Những comment này không phải bằng chứng chính thức, nhưng cho reviewer cái để kiểm tra so với mã.

Checklist nhẹ cho mã rủi ro

Hãy rõ hơn khi review mã xử lý:

• Parsing/validation (đường dẫn input hỏng, trường hợp biên)
• Concurrency (khóa, race, idempotency, retry)
• Tiền/quotas (làm tròn, tính phí đôi, tràn số)
• Quyền (ai được làm gì và vì sao)

Nếu thay đổi chạm vào các phần này, hỏi: “Preconditions là gì, và được thực thi ở đâu?” và “Chúng ta đảm bảo gì ngay cả khi có lỗi?”

Khi nào dùng công cụ hình thức — và checklist thực tế

Suy luận hình thức không có nghĩa là biến toàn bộ codebase thành bài toán toán học. Mục tiêu là bỏ thêm độ chắc chắn nơi nó mang lại giá trị: chỗ mà “trông ổn trong test” không đủ.

Khi nào formal methods hữu ích nhất

Chúng phù hợp khi bạn có một module nhỏ, then chốt mà mọi thứ khác phụ thuộc (auth, luật thanh toán, permissions, interlock an toàn), hoặc một thuật toán rắc rối nơi lỗi lệch chỉ số ẩn lâu (parsers, schedulers, caching/eviction, mã kiểu phân hoạch).

Qui tắc hữu ích: nếu một bug có thể gây tổn hại thực sự, mất tiền lớn, hoặc mất dữ liệu thầm lặng, bạn cần hơn review + test bình thường.

Công cụ nên cân nhắc (ở mức cao)

Bạn có thể chọn từ “nhẹ” đến “nặng”, và thường kết hợp cho kết quả tốt nhất:

• Types (hệ thống kiểu mạnh hơn, non-null, đơn vị/đo lường): ngăn các trạng thái không hợp lệ.
• Static analysis: tìm đường đi đáng ngờ, dùng API sai, data race, luồng dữ liệu nhiễm.
• Contracts (pre/postconditions, assertions): phiên bản có thể chạy của các tuyên bố Hoare.
• Model checking: khám phá máy trạng thái (tốt cho giao thức, concurrency, chuỗi “nếu thì” ).
• Formal verification: bằng chứng kiểm tra bởi máy cho các phần cần độ tin cậy cao nhất.

Đi sâu tới mức nào?

Quyết định độ hình thức bằng cách cân nhắc:

• Rủi ro: tác động × khả năng xảy ra. Rủi ro cao cần chứng nhận mạnh hơn.
• Chi phí: thời gian để mô tả, chứng minh và duy trì.
• Tốc độ thay đổi: mã thay đổi nhanh khó giữ chứng minh; ổn định API trước.
• Kỹ năng đội: bắt đầu bằng contracts và static analysis nếu bằng chứng sẽ làm chậm giao hàng.

Thực tế, bạn có thể thêm “hình thức” từng bước: bắt đầu bằng contract và bất biến rõ ràng, rồi dùng tự động hóa để giữ chúng.

Checklist thực tế

Dùng đây như cổng “chúng ta có nên formalize thêm không?” trong lập kế hoạch hoặc review:

1. Thất bại nghiêm trọng nhất là gì và ai bị ảnh hưởng (user, ops, regulator)?
2. Tests có phủ các trường hợp biên quan trọng không?
3. Logic có trạng thái, concurrency hay nặng bất biến/biên không?
4. Chúng ta có thể viết pre/post rõ ràng cho điểm vào công khai không?
5. Có core nhỏ nào để cô lập và xác minh sâu hơn không?
6. Công cụ nào mang lại lợi tức tốt nhất: kiểu mạnh, phân tích tĩnh, contracts, model checking hay chứng minh?
7. Điều gì sẽ thay đổi quý tới và làm sao giữ được đảm bảo không trôi?

Đọc thêm: design-by-contract, property-based testing, model checking cho máy trạng thái, static analyzers cho ngôn ngữ bạn dùng, và tài liệu giới thiệu về proof assistants và specification hình thức.