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ất biến f có thể giúp chúng ta giải quyết trọn vẹn câu hỏi ìBằng các phép biến đổi T, có thể đưa từ trạng thái s về trạng thái t?” trong trường hợp mà f(s) khác f(t). Cụ thể câu trả lời sẽ là ìkhông”. Tuy nhiên, nếu f(s) = f(t) thì ta lại chưa có thể kết luận gì. Chính vấn đề này dẫn đến một khái niệm mới: bất biến toàn năng...

Chi tiết mời các bạn tham khảo tại: http://repository.vnu.edu.vn/handle/VNU_123/17204

Title:	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
Keywords:	Kỹ thuật phần mềm;Logic Hoare;Bất biến (Invariants);Bất biến (Invariants) -- Kỹ thuật tìm;Biến (Variants);Kỹ thuật tìm
Issue Date:	2016
Publisher:	Đại học Quốc gia Hà Nội
Citation:	63 tr.
URI:	http://repository.vnu.edu.vn/handle/VNU_123/17204
Appears in Collections:	Luận văn - Luận án (LIC)