In this paper, a tool for structuring and manipulating formal program derivation is specified using the Z  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 . 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  which provides a powerful way of dealing with the use of different relations in sub-derivations.
|Kustantaja||Åbo Akademi University|
|Tila||Julkaistu - 1994|
|OKM-julkaisutyyppi||D4 Julkaistut kehitykset tai tutkimusraportit tai tutkimukset|
|Nimi||Reports on Computer Science and Mathematics, Series A94 - 157|