This is the first of a series of papers devoted to the thorough investigation of refinement based on an underlying partial relational model. In this paper we restrict attention to operation refinement. We explore four theories of refinement based on an underlying partial relation model for specifications, and we show that they are all equivalent. This, in particular, sheds some light on the relational completion operator due to Woodcock which underlies data refinement in, for example, the specification language Z. It (...) further leads to two simple alternative models which are also equivalent to the others. (shrink)

An understanding of logic is essential to computer science. This book provides a highly accessible account of the logical basis required for reasoning about computer programs and applying logic in fields like artificial intelligence. The text contains extended examples, algorithms, and programs written in Standard ML and Prolog. No prior knowledge of either language is required. The book contains a clear account of classical first-order logic, one of the basic tools for program verification, as well as an introductory survey of (...) modal and temporal logics and possible world semantics. An introduction to intuitionistic logic as a basis for an important style of program specification is also featured in the book. (shrink)