Title
An inconsistency in procedures, parameters, and substitution in the refinement calculus
Abstract
Morgan and Back have proposed different formalisations of procedures and parameters in the context of techniques of program development based on refinement. In this paper, we investigate a surprising and intricate relationship between these works and the substitution operator that renames the free variables of a program. In this study, we reveal an inconsistency in Morgan's refinement calculus and show that Back's formalisation of procedures does not have the same problem.
Year
DOI
Venue
1999
10.1016/S0167-6423(97)00015-4
Sci. Comput. Program.
Keywords
Field
DocType
parameters,procedures,refinement calculus,program development,formal methods,formal method,computer programming
Programming language,Refinement calculus,Free variables and bound variables,Computer science,Theoretical computer science,Formal specification,Program development,Operator (computer programming),Formal methods,Computer programming,Software development
Journal
Volume
Issue
ISSN
33
1
Science of Computer Programming
Citations 
PageRank 
References 
14
1.16
4
Authors
3
Name
Order
Citations
PageRank
Ana Cavalcanti166859.95
Augusto Sampaio250143.38
Jim Woodcock353477.08