Verification of partial properties-introduction

By "partial property" we mean a partial representation of the behaviour of a system, which abstracts from details which are considered as irrelevant for that representation. The main purpose of this chapter is to define notions of correctness given by partial properties, in order to complement the usual notion of correctness as an equivalence of two complete specifications, studying in detail the possible roles, advantages and application techniques of partial properties in the context of correctness preserving transformations. This concept is opposed to that of a "total" representation of the behaviour of the system, such as that considered, for instance, when we want to verify the equivalence of a given specification and its implementation. In this sense, the other chapters of this document on Correctness Preserving Transformations are mostly concerned with the preservation of "total" properties.