An Axiomatic Basis for Computer Programming. Hoare, C. A. R. 12(10):576–580. doi abstract bibtex 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.
@article{hoareAxiomaticBasisComputer1969,
title = {An {{Axiomatic Basis}} for {{Computer Programming}}},
volume = {12},
issn = {00010782},
doi = {10.1145/363235.363259},
abstract = {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.},
number = {10},
journaltitle = {Communications of the ACM},
date = {1969},
pages = {576--580},
keywords = {0,20,21,22,23,24,4,5,and phrases,axiomatic method,cr category,design,formal language definition,machine-independent programming,program documentation,programming language,proofs of programs,theory of programming},
author = {Hoare, C. A. R.},
file = {/home/dimitri/Nextcloud/Zotero/storage/CQIK4EBT/Hoare - 1969 - An Axiomatic Basis for Computer Programming.pdf}
}
Downloads: 0
{"_id":"Q787inCyMvGq5SHkW","bibbaseid":"hoare-anaxiomaticbasisforcomputerprogramming","authorIDs":[],"author_short":["Hoare, C. A. R."],"bibdata":{"bibtype":"article","type":"article","title":"An Axiomatic Basis for Computer Programming","volume":"12","issn":"00010782","doi":"10.1145/363235.363259","abstract":"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.","number":"10","journaltitle":"Communications of the ACM","date":"1969","pages":"576–580","keywords":"0,20,21,22,23,24,4,5,and phrases,axiomatic method,cr category,design,formal language definition,machine-independent programming,program documentation,programming language,proofs of programs,theory of programming","author":[{"propositions":[],"lastnames":["Hoare"],"firstnames":["C.","A.","R."],"suffixes":[]}],"file":"/home/dimitri/Nextcloud/Zotero/storage/CQIK4EBT/Hoare - 1969 - An Axiomatic Basis for Computer Programming.pdf","bibtex":"@article{hoareAxiomaticBasisComputer1969,\n title = {An {{Axiomatic Basis}} for {{Computer Programming}}},\n volume = {12},\n issn = {00010782},\n doi = {10.1145/363235.363259},\n abstract = {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.},\n number = {10},\n journaltitle = {Communications of the ACM},\n date = {1969},\n pages = {576--580},\n keywords = {0,20,21,22,23,24,4,5,and phrases,axiomatic method,cr category,design,formal language definition,machine-independent programming,program documentation,programming language,proofs of programs,theory of programming},\n author = {Hoare, C. A. R.},\n file = {/home/dimitri/Nextcloud/Zotero/storage/CQIK4EBT/Hoare - 1969 - An Axiomatic Basis for Computer Programming.pdf}\n}\n\n","author_short":["Hoare, C. A. R."],"key":"hoareAxiomaticBasisComputer1969","id":"hoareAxiomaticBasisComputer1969","bibbaseid":"hoare-anaxiomaticbasisforcomputerprogramming","role":"author","urls":{},"keyword":["0","20","21","22","23","24","4","5","and phrases","axiomatic method","cr category","design","formal language definition","machine-independent programming","program documentation","programming language","proofs of programs","theory of programming"],"downloads":0},"bibtype":"article","biburl":"https://raw.githubusercontent.com/dlozeve/newblog/master/bib/all.bib","creationDate":"2020-01-08T20:39:39.052Z","downloads":0,"keywords":["0","20","21","22","23","24","4","5","and phrases","axiomatic method","cr category","design","formal language definition","machine-independent programming","program documentation","programming language","proofs of programs","theory of programming"],"search_terms":["axiomatic","basis","computer","programming","hoare"],"title":"An Axiomatic Basis for Computer Programming","year":null,"dataSources":["3XqdvqRE7zuX4cm8m"]}