Specification of a program derivation editor

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

Specification of a program derivation editor

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

^*Korresponderande författare för detta arbete

Informationsteknologi

Forskningsoutput: Bok/tidskrift/rapport › Beställd rapport › Professionell

8 Nedladdningar (Pure)

Sammanfattning

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.

Originalspråk	Engelska
Förlag	Åbo Akademi University
Status	Publicerad - 1994
MoE-publikationstyp	D4 Publicerad utvecklings- eller forskningsrapport eller studie

Publikationsserier

Namn	Reports on Computer Science and Mathematics, Series A94 - 157

Åtkomst av dokument

tBuHeNiRuWaZ94Slutlig publicerad version, 249 KB

Citera det här

@book{9464df5ef7f74675b8dbb081f7dc0b95,

title = "Specification of a program derivation editor",

abstract = "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.",

author = "Michael Butler and Eric Hedman and Patrik Nilsson and Rimvydas Ruksenas and Marina Walden and Yi Zhao",

year = "1994",

language = "English",

series = "Reports on Computer Science and Mathematics, Series A94 - 157",

publisher = "{\AA}bo Akademi University",

}

TY - BOOK

T1 - Specification of a program derivation editor

AU - Butler, Michael

AU - Hedman, Eric

AU - Nilsson, Patrik

AU - Ruksenas, Rimvydas

AU - Walden, Marina

AU - Zhao, Yi

PY - 1994

Y1 - 1994

N2 - 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.

AB - 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.

Specification of a program derivation editor

Sammanfattning

Publikationsserier

Åtkomst av dokument

Fingeravtryck

Citera det här