Title :
Modular refinement in novel schema calculi
Author :
Deutsch, Moshe ; Henson, Martin C. ; Kajtazi, Besnik
Author_Institution :
Dept. of Comput. Sci., Essex Univ., Colchester, UK
Abstract :
Using the language Z for more than specification is hindered by the fact that its algebra of schemas is not monotonic with respect to refinement; so specification is modular, but development is not. We isolate the reasons why Z suffers from these problems and we describe alternative models for specifications and schema operations, which are monotonic. This leads us to explore a number of theoretical and pragmatic questions: the former concern logics for modular refinement; the latter explore the use of novel schema calculi in practice.
Keywords :
formal specification; reasoning about programs; refinement calculus; specification languages; Z specification language; formal specification; modular reasoning; modular refinement calculus; schema calculi; Algebra; Calculus; Computer science; Layout; Logic functions; Modular construction; Software engineering; Specification languages; Stress; Terminology;
Conference_Titel :
Software Engineering Conference, 2003. Tenth Asia-Pacific
Print_ISBN :
0-7695-2011-1
DOI :
10.1109/APSEC.2003.1254372