Skip Navigation

The Computer Journal 1975 18(1):55-62; doi:10.1093/comjnl/18.1.55
© 1975 by British Computer Society
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Lanzarone, G. A.
Right arrow Articles by Ornaghi, M.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Program construction by refinements preserving correctness

G. A. Lanzarone * and M. Ornaghi

Gruppo di Elettronic e Cibernetica, Istituto di Fisica dell'Università di Milano, Via Viotti, 5-20133, Milano, Italy

This paper deals with the problem of constructing the final version Pt of a flowchart program through successive refinements P2, ..., Pt–1 that preserve correctness proved on its first version P1.

Correctness conditions are associated with P1 in the frame of Manna's formalism. With each refinement Pi a relational (data) structure Si is associated, and given representation functions {tau}i relate structures Si, Si+1 of refinements Pi, Pi+1.

Construction of Pi+1 from Pi proceeds as follows: (a) every block of Pi is considered as an elementary program over Si and its correctness conditions are expressed with terms of Si; (b) these correctness conditions are translated by using the representation function {tau}i; (c) the translated correctness conditions are transformed into expansion conditions, expressed with terms of Si+1 only, for every block of Pi; (d) by means of these expansion conditions, expansions of blocks are constructed and connected to obtain Pi+1.

The constructive character of the above process is emphasised with a detailed example.

In the appendix a discussion relates this paper to other works connecting constructivism and program theory.

Received July 1973.

* Honeywell Information Systems Italia (HISI).

§ Gruppo di Elettronic e Cibernetica, Istituto di Fisica dell'Università di Milano, Via Viotti, 5-20133, Milano, Italy


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.