Phát triển các kỹ thuật tìm bất biến (Invariants) và biến (Variants) cho việc sử dụng Hoare Logic để chứng minh tính đúng đắn của chu trình Authors: Nguyễn, Minh Hải Bất biến là một công cụ quan trọng trong việc giải các bài toán Olympic, đặc biệt là các bài toán có nội dung tổ hợp. Hiện nay tôi đang viết một bài giảng về bất biến. Vì vậy đang cần đến một số ví dụ hay (cũng như các vấn đề lý thuyết hay) về ứng dụng của bất biến. Bài toán cơ bản sử dụng bất biến được phát biểu dưới dạng như sau: Bài toán 1. Có một tập hợp các trạng thái S và tập hợp các phép biến đổi T từ S vào S. Có hai trạng thái s và t thuộc S. Hỏi có thể dùng hữu hạn các phép biến đổi thuộc T để đưa trạng thái s về trạng thái t được không? Định nghĩa. Cho S là một tập hợp các trạng thái. T là tập hợp các phép biến đổi từ S vào S. Hàm số f: S --> R được gọi là bất biến trên tập các trạng thái đối với tập các phép biến đổi T nếu f(t(s)) = f(s) với mọi s thuộc S và t thuộc T. Như vậy, b...