Mathematical science of computation
and structured programming
Cultures of Programming — Part 4
Tomas Petricek, Charles University, Prague
Mathematical culture
Proving program properties
Mathematical science
of computation
Programs as formal entities
Algorithms as objects to study
Formal mathematical reasoning
Algol paradigm
Algol paradigm
Mathematical Science (McCarthy, 1962)
- Two procedures (functions) are equivalent
- Procedure terminates for all input data
- Translation correctly translates procedures
- Translation increases efficiency
McCarthy's factorial proof
Algol paradigm
Proving programs correct
-
Peter Naur (1966)
Proofs of algorithms by general snapshots -
Robert Floyd (1967)
Assigning meaning to programs -
Tony Hoare (1969)
An axiomatic basis for computer programming
Floyd (1967)
Cites McCarthy and uses a subset of Algol
But uses flowcharts!
Common visual representation of programs at the time
Hoare (1969)
Annotate programs using
tripes \(\{P\} \,c\, \{Q\}\) where:
- \(P\) pre-condition holds before
- \(c\) command to run
- \(Q\) post-condition holds afterwards
Using modern notation for
(now called) Hoare-triples
Hoare (1969)
Reasoning about programs
using Hoare triples
Composition rule!
If \(\{P\}\,c_1\,\{Q\}\)
and \(\{Q\}\,c_2\,\{R\}\)
then \(\{P\}\,c_1;c_2\,\{R\}\)
Proofs of programs in practice
Proofs of programs in practice
Prevention of deadlocks (1969)
- Abstract algorithm written as pseudocode
- Model using states and transitions
- Not actual source code!
Proof of FIND (1971)
- Part of Hoare's QuickSort algorithm
- Find \(f^{th}\) element in an array and rearrange
- \(A[1],\ldots,A[f-1]\leq A[f]\leq A[f+1],\ldots,A[N]\)
- ... it may be possible to enlist the aid of a computer
Mathematical culture
Structuring programs
TODO
Managerial culture
Structuring teams
TODO
Cultures of Programming
Home Continue to Part 5