Much current research in computer science is concerned with two questions: is a program correct? And how can we improve a correct program preserving correctness? This latter question is known as the refinement of programs and the purpose of this book is to consider these questions in a formal setting. In fact, correctness turns out to be a special case of refinement and so the focus is on refinement. Although a reasonable background knowledge is assumed from mathematics and CS, the (...) book is a self-contained introduction suitable for graduate students and researchers coming to this subject for the first time. There are numerous exercises provided of varying degrees of challenge. (shrink)

Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...) a predicative way by an inductive generation and thus their properties can be proved inductively. We show however that some natural complete Heyting algebra cannot be inductively defined. (shrink)