Specification of a program derivation editor

Michael Butler, Eric Hedman, Patrik Nilsson, Rimvydas Ruksenas, Marina Walden*, Yi Zhao

*Corresponding author for this work

Research output: Book/Journal/ReportCommissioned reportProfessional

3 Downloads (Pure)


In this paper, a tool for structuring and manipulating formal program derivation is specified using the Z [13] notation. A program derivation style based on (transitive) relations between programs, as found in the refinement calculus [1, 8, 9], is assumed. The structuring and manipulation of derivations is based on the notion of refinement diagrams proposed by Back [3]. This allows for a style of derivation that is much more flexible than top-down refinement and is more suited to large-scale program development. The original refinement diagram notion is also extended with ideas from window inference [12] which provides a powerful way of dealing with the use of different relations in sub-derivations.
Original languageEnglish
PublisherÅbo Akademi University
Publication statusPublished - 1994
MoE publication typeD4 Published development or research report or study

Publication series

NameReports on Computer Science and Mathematics, Series A94 - 157


Dive into the research topics of 'Specification of a program derivation editor'. Together they form a unique fingerprint.

Cite this