Kiểm thử theo thuộc tính và thu nhỏ phản ví dụ

1. Từ ví dụ đơn lẻ đến mệnh đề kiểm thử

Trong lập lịch, biểu diễn ca bằng khoảng nửa mở [a,b) cho phép một lớp kết thúc đúng lúc lớp sau bắt đầu. Chẳng hạn [8,10) và [10,12) không giao nhau. Ta muốn phát hiện lỗi ở hàm kiểm tra giao nhau ngay cả khi người viết bộ ca quên tạo dữ liệu có đúng tình huống chạm đầu mút.

Một thuộc tính tự nhiên là tính đối xứng: đổi vị trí hai khoảng phải giữ nguyên kết quả. Tuy nhiên, hàm so sánh sai dùng <= thay cho < vẫn đối xứng. Thuộc tính cần kiểm chứng được các khía cạnh khác nhau của đặc tả, ví dụ hai khoảng kề nhau phải rời nhau, hoặc độ dài phần giao phải dương nếu hàm trả về đúng.

2. Xây dựng oracle bằng biểu diễn độc lập

Mã chính tính giao nhau bằng cách so sánh đầu mút. Oracle trên miền nguyên tạo tập các mốc thuộc mỗi khoảng và kiểm tra hai tập có phần tử chung hay không. Với đầu mút nguyên và khoảng khác rỗng, một giao có độ dài dương luôn chứa một mốc nguyên. Nhờ đó oracle tập hợp đồng ý với đặc tả nửa mở, đồng thời tránh sao chép phép so sánh có khả năng sai từ triển khai.

Bộ sinh chỉ tạo khoảng có đầu nhỏ hơn cuối. Nếu hệ thống cho phép khoảng rỗng, cần xác định riêng đầu ra kỳ vọng và mở rộng bộ sinh. Nếu có kiểu thời gian liên tục hoặc chuyển múi giờ, oracle dùng tập các mốc nguyên không còn đại diện cho toàn bộ miền. Tách phạm vi đó trước khi kết luận về tính đúng đắn của hàm.

3. Thu nhỏ phản ví dụ tới tình huống dễ đọc

Chạy bằng Python 3. Chương trình kiểm tra 1.296 cặp khoảng hợp lệ trong một miền hữu hạn, rồi chọn phản ví dụ đơn giản theo thước đo đã định. Cặp [0,1) và [1,2) vẫn bất đồng với hàm lỗi dù cả hai khoảng chỉ dài một đơn vị. Hàm đúng trả về sai, còn biến thể dùng <= nhận nhầm phần giao có độ dài 0. Mẫu rút gọn dễ chuyển thành ca hồi quy vì nêu chính xác trường hợp biên.

"""Phát hiện và thu nhỏ phản ví dụ cho hàm kiểm tra trùng ca."""
from itertools import combinations, product


def faulty(a, b):
    return max(a[0], b[0]) <= min(a[1], b[1])


def overlap(a, b):
    return max(a[0], b[0]) < min(a[1], b[1])


def oracle(a, b):
    # Oracle riêng cho các mốc nguyên và khoảng nửa mở.
    return bool(set(range(*a)) & set(range(*b)))


def shrink_failure(a, b):
    intervals = list(combinations(range(max(*a, *b) + 1), 2))
    smaller = (pair for pair in product(intervals, repeat=2)
               if faulty(*pair) != oracle(*pair))
    return min(smaller, key=lambda pair: (sum(sum(interval) for interval in pair), pair))


if __name__ == "__main__":
    original = ((3, 6), (6, 8))
    assert faulty(*original) != oracle(*original)
    smallest = shrink_failure(*original)
    assert smallest == ((0, 1), (1, 2))
    intervals = list(combinations(range(9), 2))
    for a, b in product(intervals, repeat=2):
        assert overlap(a, b) == overlap(b, a)
        assert overlap(a, b) == oracle(a, b)
    print("Phản ví dụ nhỏ:", smallest, "| số cặp đối chiếu:", len(intervals) ** 2)

4. Đánh giá chất lượng bộ sinh và thuộc tính

So sánh ba bộ kiểm thử có cùng ngân sách. Bộ thứ nhất dùng dữ liệu ngẫu nhiên đều, bộ thứ hai tăng tỷ lệ ca kề nhau và ca lồng nhau, bộ thứ ba phối hợp oracle độc lập với các thuộc tính đối xứng và bất biến qua phép tịnh tiến. Có thể dùng những lỗi được cài có chủ đích như đảo đầu mút, chuyển nhầm khoảng đóng, sai đơn vị thời gian để đo mức độ phát hiện.

Báo riêng số trường hợp hợp lệ, độ phủ các lớp quan hệ và kích thước phản ví dụ sau thu nhỏ. Khi một thuộc tính không bắt được một đột biến, kiểm tra xem bộ sinh đã tạo dữ liệu kích hoạt chưa. Kết quả duyệt hết ví dụ chỉ xác nhận trên miền hữu hạn được công bố. Khi triển khai ở quy mô lớn, có thể tham khảo tài liệu Hypothesis về sinh dữ liệu kiểm thử theo thuộc tính.