Programming as a Mathematical Exercise [and Discussion]

This paper contains a formal framework within which logic, set theory and programming are presented together. These elements can be presented together because, in this work, we no longer regard a (procedural) programming notation (such as PASCAL) as a notation for expressing a computation; rather, w...

Full description

Saved in:
Bibliographic Details
Published in:Philosophical transactions of the Royal Society of London. Series A: Mathematical and physical sciences 1984-10, Vol.312 (1522), p.447-473
Main Authors: Abrial, J. R., Shepherdson, J. C., Hillmore, J. S., Constable, R. L.
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Logical proofs
Mathematical functions
Mathematical logic
Mathematical relations
Mathematical sequences
Mathematical set theory
Mathematical sets
Mathematics education
Natural numbers
Ordinal notation
Software
Software engineering
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper contains a formal framework within which logic, set theory and programming are presented together. These elements can be presented together because, in this work, we no longer regard a (procedural) programming notation (such as PASCAL) as a notation for expressing a computation; rather, we regard it as a mere extension to the conventional language of logic and set theory. The extension constitutes a convenient (economical) way of expressing certain relational statements. A consequence of this point of view is that the activity of program construction is transformed into that of proof construction. To ensure that this activity of proof construction can be given a sound mechanizable foundation, we present a number of theories in the form of some basic deduction and definition rules. For instance, such theories compose the two logical calculi, a weaker version of the standard Zermelo--Fraenkel set theory, as well as some other elementary mathematical theories leading up to the construction of natural numbers. This last theory acts as a paradigm for the construction of other types such as sequences or trees. Parallel to these mathematical constructions we axiomatize a certain programming notation by giving equivalents to its basic constructs within logic and set theory. A number of other non-logical theories are also presented, which allows us to completely mechanize the calculus of proof that is implied by this framework.
ISSN:1364-503X
0080-4614
1471-2962
2054-0272
DOI:10.1098/rsta.1984.0070