Towards a formal theory of program construction.


Christoph Kreitz.  
Revue d' intelligence artificielle 4(3):5379, 1990. 

Abstract 

A unified framework for formal reasoning about programs and
deductive mechanisms involved in programming is developed. Within it
principal approaches to program synthesis are formally investigated.
We will show that a high degree of abstraction opens a way to combine
their strengths, simplifies formal proofs, and leads to clearer
insights into the metamathematics of program construction. All
definitions and theorems are presented completely formal which allows
to straightforwardly implement them with a proof system for the
underlying calculus and derive verified implementations of programming
methods from them.

Back to overview of papers 

Bibtex Entry 

@Article{ar:Kreitz90a, author = "Christoph Kreitz", title = "Towards a formal theory of program construction", journal = "Revue d' intelligence artificielle", year = 1990, volume = "4", number = "3", pages = "5379" } 