Phần 2 kết thúc với một bảng 24 ca mà tôi tự nghĩ ra. Bảng đó chỉ tốt bằng trí tưởng tượng của người viết: ca biên 16:00 có mặt vì tôi biết nó là biên. Lỗi thật thường nằm ở biên mà không ai nghĩ tới — số âm nhỏ hơn một đơn vị, hai ký tự lạ đứng cạnh nhau, danh sách có đúng một phần tử. Property-based testing đổi cách làm: thay vì liệt kê ví dụ, bạn phát biểu điều luôn đúng, để máy sinh hàng nghìn đầu vào, và khi tìm được phản ví dụ thì tự thu nhỏ nó về dạng nhỏ nhất còn làm lỗi. Bài này đo cả ba lời hứa đó trên bốn hàm có lỗi thật.

Bốn hàm, hai cách kiểm

Ảnh chụp đoạn mã nền tối property-based testing phát biểu tính chất để máy sinh ca và thu nhỏ với Go 1.23 pgregory.net rapid v1.1.0 có thu nhỏ testing quick stdlib không thu nhỏ 4 hàm thuần mỗi hàm 1 lỗi tinh vi, bốn hàm bốn lỗi mà ca hiển nhiên không chạm tới gồm FormatMoney cents với d c bằng cents chia 100 cents mod 100 nếu c âm thì đổi dấu nên -5 xu cho d bằng 0 thành 0.05 mất dấu, Slugify s gộp hai gạch trước khi thay ký tự lạ bằng gạch nên a hai dấu cách b thành a hai gạch b không luỹ đẳng, Paginate items n số trang bằng len chia n cộng 1 nên len chia hết cho n thừa 1 trang rỗng, Merge intervals gộp khi iv.A nhỏ hơn last.B nên 0 3 và 3 3 chạm biên không gộp, test ví dụ viết tay 42 dòng những ca người viết nghĩ ra gồm vòng lặp các xu 0 5 100 1234 100000 -1234 kiểm ParseMoney FormatMoney c bằng c, Slugify Hello World bằng hello-world Slugify x ba gạch y bằng x-y Slugify hai cách a hai cách bằng a, Paginate 1 tới 7 size 3 bằng ba trang và Paginate rỗng 3 bằng một trang rỗng với ghi chú người viết chấp nhận 1 trang rỗng, Merge 1 4 2 6 8 10 9 12 bằng 1 6 8 12, test tính chất 78 dòng nói điều luôn đúng thay vì nói ví dụ gồm rapid.Check với c bằng rapid.Int64Range âm 1e9 tới 1e9 Draw cents nếu ParseMoney FormatMoney c khác c thì t.Fatalf round-trip hỏng, Slug once bằng Slugify s và once bằng Slugify once và không chứa hai gạch và không bắt đầu kết thúc bằng gạch, Paginate không trang nào rỗng nếu có phần tử mỗi trang nhỏ hơn bằng size ghép lại đủ len items, Merge kết quả tăng dần và không chạm nhau tập điểm nguyên được phủ y hệt đầu vào, cách đo mã có lỗi test ví dụ ra sao rapid tìm được sau bao nhiêu ca phản ví dụ thu nhỏ còn gì quick phản ví dụ thô, mã đã sửa cả hai bộ ra sao thời gian với rapid.checks 100 1.000 10.000

Hình 1: Bốn lỗi được cấy ở biên; test ví dụ liệt kê ca, test tính chất phát biểu bất biến và giao việc sinh dữ liệu cho rapid.

Bốn hàm thuần kiểu hay gặp trong backend, mỗi hàm một lỗi:

  • FormatMoney/ParseMoney: xu sang chuỗi "đồng.xu" và ngược lại. Lỗi: với số âm nhỏ hơn một đồng, phần đồng là 0 nên dấu trừ biến mất — −5 xu thành "0.05".
  • Slugify: chữ thường, ký tự lạ thành gạch nối, gộp gạch nối liên tiếp, cắt hai đầu. Lỗi: gộp trước khi thay, nên hai ký tự lạ liền nhau sinh ra "--" mà không được gộp.
  • Paginate: chia danh sách thành trang. Lỗi: số trang tính bằng len/size + 1, đúng khi có dư, thừa một trang rỗng khi chia hết.
  • Merge: gộp các khoảng đóng chồng nhau. Lỗi: dùng < thay vì <=, nên hai khoảng chạm nhau ở biên không được gộp.

Test ví dụ (42 dòng) là những ca một người viết cẩn thận sẽ nghĩ ra: tiền 0, 5, 100, 1.234, −1.234; slug của "Hello World" và "x---y"; bảy phần tử chia ba; bốn khoảng chồng nhau. Có một chi tiết đáng chú ý ở ca Paginate([], 3): người viết chạy thử, thấy trả về một trang rỗng, thấy "cũng hợp lý", và ghi đúng hành vi đó vào test.

Test tính chất (78 dòng, dùng pgregory.net/rapid): tiền đi vòng qua định dạng rồi phân tích phải về đúng giá trị; slug phải luỹ đẳng (slug của slug bằng chính nó) và không chứa "--", không bắt đầu hay kết thúc bằng gạch; phân trang không có trang rỗng khi còn phần tử, mỗi trang không quá size, ghép lại đủ; gộp khoảng ra kết quả tăng dần, không chạm nhau, và phủ đúng tập điểm nguyên của đầu vào. Không một ví dụ cụ thể nào — chỉ có luật.

Thêm một bộ dùng testing/quick của thư viện chuẩn cho cùng tính chất slug, để so cái thiếu của nó: không thu nhỏ.

Đo thật: ai tìm được gì, và phản ví dụ dài bao nhiêu

Ảnh chụp output thật nền tối ví dụ xanh 4 trên 4 tính chất đỏ 4 trên 4 ngay ca đầu với go test trong go-lab rapid 100 ca mỗi tính chất PBT_FIX 1 bật bản sửa, mã có lỗi gồm FormatMoney Parse ví dụ PASS lọt rapid đỏ ở ca 1 phản ví dụ cents bằng -1 thành 0.01 thành 1, Slugify ví dụ PASS lọt rapid đỏ ở ca 1 s bằng A hỏi ᛮ A thành a hai gạch a thành a gạch a, Paginate ví dụ PASS lọt rapid đỏ ở ca 1 items bằng 0 size 1 thành 2 trang trang 1 rỗng, Merge ví dụ PASS lọt rapid đỏ ở ca 1 0 3 và 3 3 không gộp, tổng 0 trên 4 lỗi và 4 trên 4 lỗi với ghi chú ca đầu tiên rapid thử luôn là giá trị biên 0 -1 rỗng 1 phần tử, cùng tính chất Slug testing quick stdlib không thu nhỏ thất bại ở ca 1 phản ví dụ thô dài 20 rune là chuỗi mã Unicode không đọc nổi còn rapid sau khi thu nhỏ 4 rune A hỏi ᛮ A đủ để thấy ngay hai ký tự lạ liền nhau, mã đã sửa PBT_FIX 1 gồm 4 tính chất OK passed 100 tests 97 164 125 216 micro giây, rapid.checks 100 4 tính chất 0,002 s, 1000 0,006 s, 10000 0,044 s là 40.000 ca kiểm trong 44 ms, test ví dụ TestPaginateExamples đỏ rỗng bằng danh sách trống vì ví dụ đã đóng băng hành vi sai Paginate rỗng 3 bằng một trang rỗng, nói thẳng bốn lỗi này do tôi cấy nên PBT thắng 4-0 là tất yếu con số đáng nhớ là cách nó thắng ca đầu tiên đã trúng vì sinh giá trị biên trước và phản ví dụ 4 rune thay vì 20 ví dụ viết tay thì đóng băng cả lỗi

Hình 2: Kết quả thật. Bên trái là mã có lỗi, bên phải là sau khi sửa; dòng cuối là test ví dụ đỏ trên mã đúng.

hàm test ví dụ rapid phản ví dụ thu nhỏ
FormatMoney/Parse xanh (lọt) đỏ ở ca #1 -1 → "0.01" → 1
Slugify xanh (lọt) đỏ ở ca #1 "A?ᛮA" → "a--a"
Paginate xanh (lọt) đỏ ở ca #1 [0], size 1 → 2 trang
Merge xanh (lọt) đỏ ở ca #1 {0,3} {3,3} không gộp

Ví dụ xanh 4/4, tính chất đỏ 4/4 — ngay ca sinh đầu tiên. Không phải may mắn: rapid cố ý sinh giá trị biên trước — số 0 và −1, chuỗi rỗng rồi chuỗi ngắn, danh sách một phần tử, size nhỏ nhất. Bốn lỗi này đều nằm ở biên, nên ca đầu tiên đã trúng. Test ví dụ thì xanh vì người viết đã chọn các giá trị "bình thường": −1.234 thay vì −1, "x---y" thay vì "x y", bảy phần tử thay vì ba, các khoảng chồng rõ rệt thay vì chạm biên. Đó không phải người viết kém; đó là bản chất của ví dụ — bạn chỉ viết ra ca mà bạn đã nghĩ tới.

Phản ví dụ sau khi thu nhỏ đọc được ngay. -1 xu là đủ để thấy dấu trừ mất ở đâu. "A?ᛮA" — bốn ký tự, hai ký tự lạ liền nhau — chỉ thẳng vào thứ tự gộp và thay. [0] với size 1 chỉ vào phép chia hết. {0,3} {3,3} chỉ vào dấu <. So với testing/quick của thư viện chuẩn trên cùng tính chất slug: tìm được lỗi, cũng ở ca đầu, nhưng phản ví dụ là 20 rune ngẫu nhiên toàn ký tự Unicode không đọc nổi. Thu nhỏ là thứ biến "có lỗi ở đâu đó" thành "lỗi ở đây".

Sửa xong, 40.000 ca trong 44 ms. Bốn tính chất với 100 ca mỗi tính chất chạy trong 2 ms; với 10.000 ca, 44 ms. Vì hàm thuần, chi phí mỗi ca là micro-giây, nên mặc định 100 ca của rapid rẻ tới mức có thể để trong bộ test thường; 10.000 ca để chạy đêm hoặc trước khi phát hành.

Và test ví dụ Paginate đỏ trên mã đúng. Paginate([], 3) giờ trả về không trang nào, test ví dụ muốn một trang rỗng — vì nó được viết bằng cách chạy mã có lỗi rồi ghi lại kết quả. Test ví dụ đóng băng hành vi tại thời điểm viết, kể cả hành vi sai; test tính chất đóng băng ý định ("không có trang rỗng khi còn phần tử"), nên nó đỏ trên mã sai và xanh trên mã đúng. Đây là lý do mạnh nhất để có cả hai: ví dụ nói "nó phải làm thế này với đầu vào này", tính chất nói "dù đầu vào gì, điều này phải đúng".

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

Khó nhất là tìm ra tính chất. Bốn hàm ở đây có tính chất tự nhiên: vòng tròn (định dạng rồi phân tích), luỹ đẳng (slug của slug), bảo toàn (ghép trang lại đủ), bất biến cấu trúc (không chồng, phủ đúng). Nhiều hàm nghiệp vụ không có tính chất đẹp như vậy, hoặc tính chất duy nhất là "bằng với cài đặt tham chiếu" — khi đó PBT vẫn dùng được nếu bạn có một cài đặt chậm nhưng rõ ràng đúng (ví dụ: Merge so với cách đánh dấu từng điểm nguyên, như bài này làm).

PBT bổ sung ví dụ, không thay thế. Ví dụ ghi lại ca nghiệp vụ cụ thể mà người đọc hiểu ngay; tính chất bắt biên mà không ai nghĩ tới. Khi rapid tìm được phản ví dụ, hãy thêm nó vào bảng ví dụ — giữ lại như hồi quy, đọc được không cần chạy rapid.

Bộ sinh quyết định cái bạn kiểm. rapid.String() sinh đủ loại Unicode nên tìm ra ᛮ; nếu bạn chỉ sinh ASCII, lỗi vẫn tìm được nhưng với chuỗi khác. Ngược lại, bộ sinh quá rộng làm nhiều ca vô nghĩa (số âm cho một hàm chỉ nhận dương) — dùng Filter hoặc thu hẹp miền, và chấp nhận rằng miền bạn chọn là một giả định cần ghi rõ.

Phạm vi đo. Bốn lỗi do tôi cấy, đều ở biên — nên PBT thắng 4–0 là tất yếu, không phải phát hiện. Thứ đáng mang về là cơ chế: sinh biên trước, thu nhỏ, và tính chất không đóng băng hành vi sai. Với lỗi không ở biên (sai logic giữa miền), PBT cần nhiều ca hơn và tính chất đủ chặt mới bắt được.

Ba ý mang về

  1. Ví dụ kiểm ca bạn nghĩ tới; tính chất kiểm ca bạn không nghĩ tới. Bốn lỗi ở biên lọt qua 42 dòng ví dụ và đỏ ngay ca đầu tiên của rapid, vì rapid sinh giá trị biên trước.
  2. Thu nhỏ là nửa giá trị của PBT: cùng lỗi slug, testing/quick trả 20 rune không đọc nổi, rapid trả "A?ᛮA". Chọn thư viện có thu nhỏ; thêm phản ví dụ tìm được vào bảng ví dụ làm hồi quy.
  3. Test ví dụ đóng băng hành vi, kể cả hành vi sai (Paginate([],3) == [[]]); test tính chất đóng băng ý định. Hàm thuần rẻ tới mức 40.000 ca chạy trong 44 ms — không có lý do để bộ test thường thiếu vài tính chất.

Nguồn

Phần sau đi tiếp cùng hướng nhưng khác mục tiêu: thay vì tính chất nghiệp vụ, tìm panic và lỗi phân tích trong mã nhận đầu vào từ bên ngoài bằng go test -fuzz — đo thời gian tới lỗi đầu tiên và vai trò của corpus.