An Axiomatic Basis for Computer Programming

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

In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantages, both theoretical and practical, may follow from a pursuance of these topics.

KEY WORDS AND PHRASES: axiomatic method, theory of programming’ proofs of programs, formal language definition, programming language design, machine-independent programming, program documentation CR CATEGORY: 4.0, 4.21, 4.22, 5.20, 5.21, 5.23, 5.24

This section is missing here.

1 Introduction

This section is missing here.

2 Computer Arithmetic

This section is missing here.

3 Program Execution

This section is missing here.

4 General Reservations

This section is missing here.

5 Proofs of Program Correctness

This section is missing here.

Notes

This section is missing here.

6 Formal Language Definition