Cited By
View all- Mueller C(2007)Alternative dataflow modelProceedings of the third conference on IASTED International Conference: Advances in Computer Science and Technology10.5555/1322468.1322469(1-6)Online publication date: 2-Apr-2007
Axiomatic computational model
Abstract
A new model of computation is explored based on axiomatic logic. The significant difference from other models is how reasoning about variables is expressed. The computation is described only by defining variables in terms of other variables. The benefit is the simplicity of the semantics of the axiomatic logic. The model is described in the form of a tutorial using a simple language to illustrate how a program can be expressed in this model.
References
[1]
A. V. Aho, R. Sethi and J. D. Ulman: Compilers: Principles, Techniques and Tools; pp 466, Addison-Wesley, 1985.
[2]
R. L. Baber, "Comparison of Electrical 'Engineering' of Heaviside's time and Software 'Engineering' of our time", IEEE Annal of the History of Computing pp 5--17, 19(4), 1997.
[3]
J. Backus: "Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs", pp 613--641, Communications of the ACM, 21(8), 1977.
[4]
O. Dahl: Verifiable Programming; Prentice Hall, 1992.
[5]
J. R. Gurd, C. C. Kirkham, I. Watson "The Manchester prototype dataflow computer", Communications of the ACM, 28(1), 1985.
[6]
C. A. R. Hoare: "An Axiomatic Basis for Computer Programming"; pp. 576--580, Communications of the ACM, 12(10) 1969.
[7]
Z. Manna and R. Waldinger, "Fundamentals of deductive program synthesis", IEEE Trans Software Eng, 18, 674--703, 1992.
[8]
Z. Manna and R. Waldinger, Deductive foundations of Computer Programming, Addison Wesley, 1993.
[9]
C. Morgan, Programming from specification, Prentice Hall, 1991.
[10]
The Concise Oxford Dictionary; Ninth Edition, 1995.
[11]
A. Plotkin,"A Tree Structured Architecture for Semantic Gap Reduction". ACM SIGARCH 11(4) 1983.
[12]
J Rattner, Hardware/Software cooperation in the iAPX-432", Proc of the 1st International Symposium on Architectural Support for Programming Languages and Operating Systems, 1982 Palo Alto, California.
[13]
I Sommerville, Software Engineering, 6th Edition, Addison-Welsey, 2001.
[14]
A. N. Whitehead and B. Russell: Principia Mathematica; 2nd edition, Cambridge, 1927.
Index Terms
- Axiomatic computational model
Recommendations
Floyd--hoare logic for quantum programs
Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build ...
Axiomatic Temporal Logic Programs Verification
TASE '10: Proceedings of the 2010 4th IEEE International Symposium on Theoretical Aspects of Software EngineeringIn this paper, we investigate the axiomatic system of Modeling Simulation and Verification Language (MSVL). To this end, a set of state axioms and state inference rules is given. They are useful to deduce a program into its normal form. Further, a ...
One-Path Reachability Logic
LICS '13: Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer ScienceThis paper introduces *(one-path) reach ability logic*, a language-independent proof system for program verification, which takes an operational semantics as axioms and derives *reach ability rules*, which generalize Hoare triples. This system improves ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2005 Author.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 March 2005
Published in SIGPLAN Volume 40, Issue 3
Check for updates
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 218Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 12 Nov 2024
Other Metrics
Citations
Cited By
View all- Mueller C(2007)Alternative dataflow modelProceedings of the third conference on IASTED International Conference: Advances in Computer Science and Technology10.5555/1322468.1322469(1-6)Online publication date: 2-Apr-2007
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in