Name
Abstract | ||
|---|---|---|
This paper deals with logics of programs. The objective is to formalize a notion of program description and to give both plausible (semantic) and effective (syntactic) criteria for the notion of truth of a description. A novel feature of this treatment is the development of the mathematics underlying Floyd-Hoare axiom systems independently of such systems. Other directions that such research might take are also considered. This paper grew out of, and is intended to be usable as, class notes for an introductory semantics course. The three sections of the paper are: 1) A frame work for the logic of programs. Programs and their partial correctness theories are treated as binary relations on states and formulae respectively. Truth-values are assigned to partial correctness assertions in a plausible (Tarskian) but not directly usable way. 2) Particular Programs. Effective criteria for truth are established for some programs using the Tarskian criteria as a benchmark. This leads directly to a sound, complete, effective axiom system for the theories of these programs. The difficulties involved in finding such effective criteria for other programs are explored. 3) Variations and extensions of the framework. Alternatives to binary relations for both programs and theories are speculated on, and their possible roles in semantics are considered. We discuss a hierarchy of varieties of programs and the importance of this hierarchy to the issues of definability and describability. Modal logic is considered as a first-order alternative to Floyd-Hoare logic. We give an appropriate axiom system which is complete for loop-free programs and also puts conventional predicate calculus in a different light by lumping quantifiers with non-logical assignments rather than treating them as logical concepts. |
Year | DOI | Venue |
|---|---|---|
1976 | 10.1109/SFCS.1976.27 | FOCS |
Keywords | Field | DocType |
modal logic,paper deal,effective criterion,effective axiom system,floyo-hoare logic,floyd-hoare logic,binary relation,appropriate axiom system,tarskian criterion,semantical consideration,semantical considerations,floyd-hoare axiom system,introductory semantics course,hoare logic,writing,boolean functions,programming,flowcharts,additives,testing,upper bound,usability,principal component analysis,artificial intelligence,system performance,force,radiation detectors,calculus,stress,logic,copper,first order,mathematics,terminology | Discrete mathematics,Combinatorics,Programming language,Axiomatic semantics,Axiom,Computer science,Correctness,Hoare logic,First-order logic,Modal logic,Hierarchy,Semantics | Conference |
Citations | PageRank | References |
258 | 185.65 | 3 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vaughan R. Pratt | 1 | 2975 | 1287.06 |
| michael j fischer | 2 | 265 | 186.28 |
| Richard E. Ladner | 3 | 5502 | 1090.33 |
| Krister Segerberg | 4 | 577 | 245.32 |
| tadeuz traczyk | 5 | 258 | 185.65 |
| Rohit Parikh | 6 | 1510 | 540.65 |