Background draft 1.

1 files changed, 53 insertions, 0 deletions

diff --git a/thesis.bib b/thesis.bib
index 54b8b70..adf7e5e 100644
--- a/thesis.bib
+++ b/thesis.bib
@@ -91,3 +91,56 @@ abstract="We give an overview of Agda, the latest in a series of dependently typ
 isbn="978-3-642-03359-9",
 doi={10.1007/978-3-642-03359-9_6}
 }
+
+@article{10.1145/363235.363259,
+author = {Hoare, C. A. R.},
+title = {An Axiomatic Basis for Computer Programming},
+issue_date = {Oct. 1969},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {12},
+number = {10},
+issn = {0001-0782},
+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 advantage, both theoretical and practical, may follow from a pursuance of these topics.},
+journal = {Commun. ACM},
+date = {1969-10},
+pages = {576–580},
+numpages = {5},
+keywords = {machine-independent programming, theory of programming' proofs of programs, program documentation, axiomatic method, programming language design, formal language definition}
+}
+
+@article{10.1007/s001650050057,
+author = {Kleymann, Thomas},
+title = {Hoare Logic and Auxiliary Variables},
+issue_date = {Dec 1999},
+publisher = {Springer-Verlag},
+address = {Berlin, Heidelberg},
+volume = {11},
+number = {5},
+issn = {0934-5043},
+doi = {10.1007/s001650050057},
+abstract = {Auxiliary variables are essential for specifying programs in Hoare Logic. They are required to relate the value of variables in different states. However, the axioms and rules of Hoare Logic turn a blind eye to the role of auxiliary variables. We stipulate a new structural rule for adjusting auxiliary variables when strengthening preconditions and weakening postconditions. Courtesy of this new rule, Hoare Logic is adaptation complete, which benefits software re-use. This property is responsible for a number of improvements. Relative completeness follows uniformly from the Most General Formula property. Moreover, one can show that Hoare Logic subsumes Vienna Development Method's (VDM) operation decomposition rules in that every derivation in VDM can be naturally embedded in Hoare Logic. Furthermore, the new treatment leads to a significant simplification in the presentation for verification calculi dealing with more interesting features such as recursion.},
+journal = {Formal Aspects of Computing},
+date = {1999-12},
+pages = {541–566},
+numpages = {26},
+keywords = {Keywords: Hoare Logic; Auxiliary variables; Adaptation Completeness; Most General Formula; VDM}
+}
+
+@article{10.1007/s00165-019-00501-3,
+author = {Apt, Krzysztof R. and Olderog, Ernst-R\"{u}diger},
+title = {Fifty Years of Hoare’s Logic},
+issue_date = {Dec 2019},
+publisher = {Springer-Verlag},
+address = {Berlin, Heidelberg},
+volume = {31},
+number = {6},
+issn = {0934-5043},
+doi = {10.1007/s00165-019-00501-3},
+abstract = {We present a history of Hoare’s logic.},
+journal = {Formal Aspects of Computing},
+date = {2019-12},
+pages = {751–807},
+numpages = {57}
+}