AN INCONSISTENCY IN PROCEDURES, PARAMETERS, AND SUBSTITUTION IN THE REFINEMENT CALCULUS

Authors
CAVALCANTI A SAMPAIO A WOODCOCK J
Citation
A. Cavalcanti et al., AN INCONSISTENCY IN PROCEDURES, PARAMETERS, AND SUBSTITUTION IN THE REFINEMENT CALCULUS, Science of computer programming, 33(1), 1999, pp. 87-96
Citations number
14
Categorie Soggetti
Computer Science Software Graphycs Programming","Computer Science Software Graphycs Programming
Journal title
Science of computer programming → ACNP
ISSN journal
01676423
Volume
33
Issue
1
Year of publication
1999
Pages
87 - 96
Database
ISI
SICI code
0167-6423(1999)33:1<87:AIIPPA>2.0.ZU;2-Z
Abstract
Morgan and Back have proposed different formalisations of procedures a nd parameters in the context of techniques of program development base d on refinement. In this paper, we investigate a surprising and intric ate relationship between these works and the substitution operator tha t renames the free variables of a program. In this study, we reveal an inconsistency in Morgan's refinement calculus and show that Back's fo rmalisation of procedures does not have the same problem. (C) 1999 Els evier Science B.V. All rights reserved.