Inconsistency and Underdefinedness in Z Specifications

Abstract In software engineering, formal methods are meant to capture the requirements of software yet to be built using notations based on logic and mathematics. The formal language Z is such a notation. It has been found that in large projects inconsistencies are inevitable. It is also said, however, that consistency is required for Z specifications to have any useful meaning. Thus, it seems, Z is not suitable for large projects. Inconsistencies are a fact of life. We are constantly challenged by inconsistencies and we are able to manage them in a useful manner. Logicians recognised this fact and developed so called paraconsistent logics to continue useful, non-trivial, reasoning in the presence of inconsistencies. Quasi-classical logic is one representative of these logics. It has been designed such that the logical connectives behave in a classical manner and that standard inference rules are valid. As such, users of logic, like software engineers, should find it easy to work with QCL. The aim of this work is to investigate the support that can be given to reason about inconsistent Z specifications using quasi-classical logic. Some of the paraconsistent logics provide an extra truth value which we use to handle underdefinedness in Z. It has been observed that it is sometimes useful to combine the guarded and precondition approach to allow the representation of both refusals and underspecification. This work contributes to the development of quasi-classical logic by providing a notion of strong logical equivalence, a method to reason about equality in QCL and a tableau-based theorem prover. The use of QCL to analyse Z specifications resulted in a refined notion of operation applicability. This also led to a revised refinement condition for applicability. Furthermore, we showed that QCL allows fewer but more useful inferences in the presence of inconsistency. Our work on handling underdefinedness in Z led to an improved schema representation combining the precondition and the guarded interpretation in Z. Our inspiration comes from a non-standard three-valued interpretation of operation applicability. Based on this semantics, we developed a schema calculus. Furthermore, we provide refinement rules based on the concept that refinement means reduction of underdefinedness. We also show that the refinement conditions extend the standard rules for both the guarded and precondition approach in Z.