Tính đúng đắn & Loop Invariant

Ba module tương tác: xem invariant được duy trì từng bước trong insertion sort & binary search, và theo dõi variant giảm dần chứng minh thuật toán dừng.

1 · Insertion sort — invariant "a[0..i−1] đã sắp xếp"

Vùng xanh luôn thỏa invariant: đã sắp xếp tăng dần. Bấm "Bước" để xem nó lớn dần tới khi phủ cả mảng.

a[0..i−1] đã sắp (invariant) key đang chèn đang dời/so sánh

2 · Binary search — invariant "target ∈ [lo, hi]"

Mảng đã sắp xếp. Vùng tím = đoạn [lo,hi] còn phải xét. Mỗi bước đoạn co lại (variant giảm) nhưng invariant "nếu target có thì nó nằm trong đoạn tím" luôn đúng.

target:

[lo,hi] còn xét mid đã loại tìm thấy

3 · Termination tracker — variant giảm dần tới chặn dưới

Chứng minh thuật toán dừng = tìm đại lượng số nguyên giảm chặt mỗi vòng & có chặn dưới. Vạch xanh là chặn dưới (0). Thanh rút ngắn dần → loop hữu hạn.

Loop: