Theories of Operation and Data Refinement
Refinement is at the heart of formal approaches to program development. It concerns the relationship between an abstract and a more concrete specification of a computer system, and ensures that, as we move towards an implementation, all the properties required by the original specification are still met. There are, however, a multitude of possible refinement relations based on a variety of mathematical models: relational, partial relational, weakest preconditions, sets of implementations, to name just a few. It is really important to understand the similarities and differences between possible approaches. This project is undertaking a comprehensive and systematic mathematical survey of known and new approaches with a view to better understanding the mathematical landscape and developing practical techniques for program development.
|Monday, 25 October 2004|