My Life, My Universe, My Everything

Ralph Miarka, John Derrick, and Eerke Boiten

In Didier Bert, Jonathan P. Bowen, Martin C. Henson, Ken Robinson, editors, ZB2002: Formal Specification and Development in Z and B / Second International Conference of B and Z Users, volume 2272 of Lecture Notes in Computer Science, pages 204-225. Springer-Verlag Berlin, January 2002.

Abstract

The aim of this paper is to discuss what formal support can be given to the process of living with inconsistencies in Z, rather than eradicating them. Logicians have developed a range of logics to continue to reason in the presence of inconsistencies. We present one representative of such paraconsistent logics, namely Hunter’s quasi-classical logic, and apply it to the analysis of inconsistent Z schemas. In the presence of inconsistency quasi-classical logic allows us to derive less, but more “useful”, information.

Consequently, inconsistent Z specifications can be analysed in more depth than at present. Part of the analysis of a Z operation is the calculation of the precondition. However, in the presence of an inconsistency, information about the intended application of the operation may be lost. It is our aim to regain this information. We introduce a new classification of precondition areas, based on the notions of definedness, overdefinedness and undefinedness. We then discuss two options to determine these areas both of which are based on restrictions of classical reasoning.

Download ZB2002.ps.gz