Cơ sở tiên đề cho lập trình máy tính
C. A. R. Hoare The Queen’s University of Belfast,* Northern Ireland
Trong bài báo này, một nỗ lực được thực hiện nhằm khảo sát các nền tảng logic của lập trình máy tính bằng cách sử dụng các kỹ thuật lần đầu tiên được áp dụng trong nghiên cứu hình học và sau đó đã được mở rộng sang các nhánh khác của toán học. Điều này bao gồm việc làm sáng tỏ các tập hợp tiên đề và các quy tắc suy luận có thể được sử dụng trong các chứng minh về các tính chất của các chương trình máy tính. Các ví dụ về những tiên đề và quy tắc như vậy được đưa ra, và một chứng minh hình thức của một định lý đơn giản được trình bày. Cuối cùng, bài báo lập luận rằng những lợi ích quan trọng, cả về mặt lý thuyết lẫn thực tiễn, có thể thu được từ việc theo đuổi các chủ đề này.
TỪ KHÓA VÀ CỤM TỪ: phương pháp tiên đề, lý thuyết lập trình, chứng minh chương trình, định nghĩa ngôn ngữ hình thức, thiết kế ngôn ngữ lập trình, lập trình độc lập với máy, tài liệu chương trình PHÂN LOẠI CR: 4.0, 4.21, 4.22, 5.20, 5.21, 5.23, 5.24