Property-based testing trong Go: khẳng định tính chất, để máy tìm phản ví dụ

Bài trước, fuzzing tìm bug bằng cách sinh input ngẫu nhiên — nhưng fuzzing trần chỉ bắt được panic. Còn một hàm chạy không sập mà trả về kết quả sai thì sao? Đó là nơi property-based testing tỏa sáng. Thay vì viết test kiểu "với input X, kết quả phải là Y" (test ví dụ), bạn khẳng định một tính chất luôn đúng với mọi input — rồi để máy sinh hàng vạn input tìm phản ví dụ.

Go có sẵn testing/quick trong thư viện chuẩn cho việc này. Bạn viết một hàm nhận input tùy ý và trả bool (tính chất có đúng không), quick.Check sẽ sinh input ngẫu nhiên và báo lỗi nếu tìm được ca làm tính chất sai. Bài này viết hai loại tính chất kinh điển — bất biến và round-trip — và để testing/quick thật tìm ra một bug logic mà fuzzing trần sẽ bỏ lọt.

Khác test ví dụ: khẳng định tính chất luôn đúng

// Test ví dụ: "với input X, kết quả phải là Y" - từng cặp cụ thể.
// Property test: "với MỌI input, TÍNH CHẤT này phải đúng".
// Máy tự sinh hàng vạn input ngẫu nhiên kiểm tính chất đó.

Điểm mạnh: bạn không cần biết trước kết quả đúng cho từng input — chỉ cần diễn đạt một quan hệ luôn phải giữ. Điều này bắt được cả những ca biên bạn chưa từng nghĩ tới.

Tính chất 1: bất biến của sắp xếp

Với hàm sắp xếp, ta không cần biết kết quả cụ thể — chỉ cần hai bất biến (invariant) luôn đúng: kết quả giữ nguyên độ dài, và thực sự tăng dần.

func TestSapXep_TinhChat(t *testing.T) {
	f := func(xs []int) bool {
		out := SapXep(xs)
		if len(out) != len(xs) { return false } // giữ độ dài
		return sort.IntsAreSorted(out)           // thực sự tăng dần
	}
	quick.Check(f, &quick.Config{MaxCount: 100000}) // thử 100k input
}

quick.Check tự sinh 100.000 slice ngẫu nhiên (đủ độ dài, đủ giá trị) và kiểm tính chất trên từng cái. Không cần liệt kê ví dụ nào.

Tính chất 2: round-trip

Round-trip là tính chất cực mạnh cho mọi cặp mã hóa/giải mã: decode(encode(x)) phải bằng x với mọi x. Áp dụng cho GhepChuoi/TachChuoi (list số ↔ chuỗi):

func TestGhepTach_RoundTrip(t *testing.T) {
	f := func(xs []int) bool {
		s := GhepChuoi(xs)     // mã hóa list -> chuỗi
		got := TachChuoi(s)    // giải mã ngược lại
		return bangNhau(got, xs) // PHẢI ra đúng list gốc
	}
	quick.Check(f, &quick.Config{MaxCount: 100000})
}

Round-trip đặc biệt giá trị vì nó bắt lỗi ở cả hai chiều mà không cần bạn liệt kê kết quả mong đợi — chỉ cần "đi rồi về phải ra chỗ cũ".

Hình 1: Property-based testing trong Go với testing/quick — khẳng định tính chất đúng với mọi input (bất biến của sắp xếp, round-trip của mã hóa/giải mã) thay vì kiểm từng ví dụ; mạnh hơn fuzzing trần vì bắt cả lỗi logic, không chỉ panic.

Đo thật: một PASS, một lộ bug

Chạy cả hai test:

=== RUN   TestSapXep_TinhChat
--- PASS: TestSapXep_TinhChat (0.13s)

Tính chất bất biến của sắp xếp PASS qua 100.000 input ngẫu nhiên — SapXep luôn giữ độ dài và thực sự tăng dần. Nhưng round-trip:

=== RUN   TestGhepTach_RoundTrip
    prop_test.go:31: round-trip THẤT BẠI: #167: failed on input []int{}
--- FAIL: TestGhepTach_RoundTrip

quick.Check thử tới lần thứ 167 thì tìm được input làm sai: []int{} — một list rỗng. Đây chính là ca biên ít ai nghĩ viết test ví dụ cho. Tái hiện trực tiếp:

xs gốc      = []int{} (len 0)
GhepChuoi   = ""
TachChuoi   = []int{0} (len 1)  <- SAI: phải là []int{}
round-trip đúng? false

xs=[5 -3 42] -> "5,-3,42" -> [5 -3 42] : round-trip đúng? true

Bug rõ ràng: list rỗng mã hóa thành chuỗi rỗng "", nhưng strings.Split("", ",") trả về [""] (một phần tử là chuỗi rỗng, không phải slice rỗng), rồi atoi("") trả 0 — nên giải mã ra [0] thay vì []. List thường ([5,-3,42]) round-trip đúng; chỉ list rỗng lộ bug.

Điểm cốt lõi: đây là lỗi logic, không phải panic. Hàm chạy trơn tru, trả về một kết quả trông hợp lệ ([0]) — fuzzing trần (bài trước) sẽ không bắt được vì không có crash. Property test bắt ngay vì nó so kết quả với tính chất phải đúng.

Hình 2: Đo thật — bất biến sắp xếp PASS qua 100.000 input ngẫu nhiên; round-trip FAIL khi quick.Check tìm ra phản ví dụ []int{} ở lần 167, tái hiện cho thấy list rỗng ra [0] (lỗi logic không panic, thứ fuzz trần bỏ lọt).

Đánh đổi cần cân nhắc

Phải nghĩ ra được tính chất đúng — đó là phần khó. Sức mạnh của property test đến từ tính chất bạn khẳng định, và nghĩ ra tính chất tốt cần tư duy. Một số mẫu tái dùng được: round-trip (encode/decode, marshal/unmarshal, serialize/deserialize), bất biến (độ dài, thứ tự, tổng bảo toàn), so với cài đặt tham chiếu đơn giản hơn (test bản tối ưu so với bản ngây thơ), và tính giao hoán/kết hợp. Nếu không nghĩ ra tính chất nào, property test không giúp được — quay lại test ví dụ.

testing/quick đơn giản nhưng hạn chế shrink. testing/quick của thư viện chuẩn sinh input ngẫu nhiên và báo phản ví dụ đầu tiên tìm được — nhưng nó không rút gọn (shrink) phản ví dụ xuống tối giản như fuzzing native hay các thư viện chuyên (gopter, rapid). Ở đây may mắn phản ví dụ đã tối giản ([]int{}), nhưng với input phức tạp, testing/quick có thể báo một ca lớn khó đọc. Các thư viện property-based chuyên nghiệp shrink tốt hơn nhiều — cân nhắc khi cần.

Property test bổ sung, không thay thế test ví dụ. Test ví dụ vẫn quan trọng: chúng tài liệu hóa hành vi cụ thể ("với đầu vào này, đầu ra chính xác là kia") và bắt lỗi hồi quy rõ ràng. Property test phủ không gian input rộng nhưng không nói kết quả đúng cụ thể là gì. Dùng cả hai: test ví dụ cho các ca quan trọng và tài liệu, property test cho độ phủ rộng và ca biên bất ngờ.

Ba ý mang về

1. Property-based testing khẳng định tính chất đúng với mọi input thay vì kiểm từng ví dụ — testing/quick (thư viện chuẩn) sinh hàng vạn input ngẫu nhiên: đo thật, bất biến sắp xếp (giữ độ dài + tăng dần) PASS qua 100k input mà không cần liệt kê ví dụ nào.
2. Round-trip là tính chất mạnh bắt lỗi logic: đo thật, quick.Check tìm ra phản ví dụ []int{} ở lần thứ 167 — list rỗng mã hóa thành "" rồi giải mã ra [0] thay vì [], một lỗi không panic mà fuzzing trần bỏ lọt.
3. Nêu rõ đánh đổi: phải tự nghĩ ra tính chất đúng (round-trip/bất biến/so bản tham chiếu là các mẫu tái dùng), testing/quick không shrink phản ví dụ tốt như thư viện chuyên (rapid, gopter), và property test bổ sung chứ không thay test ví dụ.

Bài tập làm thử

Bài 1 (đọc hiểu). Trong test tính chất sau, có hai điều kiện được kiểm tra trong hàm f. Hãy nêu tên gọi (invariant) của từng điều kiện và giải thích tại sao cả hai đều cần thiết để khẳng định "SapXep đúng".

f := func(xs []int) bool {
	out := SapXep(xs)
	if len(out) != len(xs) { return false }
	return sort.IntsAreSorted(out)
}

Bài 2 (sửa lỗi/chẩn đoán bug). Từ log đo thật của bài: TachChuoi khi nhận chuỗi rỗng trả về []int{0} thay vì []int{}. Dựa trên đoạn giải thích "strings.Split("", ",") trả về [""]", hãy viết lại logic sửa lỗi cho hàm TachChuoi để xử lý đúng trường hợp chuỗi rỗng.

func TachChuoi(s string) []int {
	if s == "" {
		return []int{} // xử lý riêng trường hợp biên: chuỗi rỗng
	}
	parts := strings.Split(s, ",")
	out := make([]int, len(parts))
	for i, p := range parts {
		out[i], _ = strconv.Atoi(p)
	}
	return out
}

Bài 3 (vận dụng thực tế). Đội của bạn viết một hàm NenChuoi/GiaiNen (compress/decompress). Theo mẫu tính chất round-trip trong bài, hãy viết một test tính chất bằng testing/quick để kiểm tra hàm này, không cần biết trước kết quả nén cụ thể là gì.

func TestNenGiaiNen_RoundTrip(t *testing.T) {
	f := func(data []byte) bool {
		nen := NenChuoi(data)
		got := GiaiNen(nen)
		return bytes.Equal(got, data) // phải ra đúng dữ liệu gốc
	}
	quick.Check(f, &quick.Config{MaxCount: 100000})
}

Bài 4 (bẫy/đánh đổi). Một lập trình viên nói: "Test tính chất round-trip đã PASS 100.000 lần, vậy hàm chắc chắn không có bug nào cả." Nhận định này có đúng theo tinh thần của bài không?

Bài 5 (đọc hiểu output Go). Log đo thật ghi: round-trip THẤT BẠI: #167: failed on input []int{}. Giải thích ý nghĩa của số #167 trong thông báo này, và tại sao đây là một ca biên mà test ví dụ truyền thống dễ bỏ sót.

Phần sau ta chuyển sang kiểm thử tích hợp thật: integration test với testcontainers trong Go — dựng database/Redis thật trong Docker ngay trong test, chạy rồi dọn tự động, thay vì mock.