Handling Inconsistencies in Z using Quasi-Classical Logic

Miarka, Ralph and Derrick, John and Boiten, Eerke Albert (2002) Handling Inconsistencies in Z using Quasi-Classical Logic. In: Berto, Didier and Bowen, Jonathan P. and Henson, Martin C. and Robinson, Ken, eds. ZB 2002:Formal Specification and Development in Z and B. Lecture Notes in Computer Science, 2272. Springer-Verlag Berlin Heidelberg, Grenoble, France pp. 204-225. ISBN 3-540-43166-7. (doi:https://doi.org/10.1007/3-540-45648-1_11) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided. (Contact us about this Publication)
Official URL


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.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Z, Quasi-classical logic, Inconsistency
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: E.A. Boiten
Date Deposited: 24 Nov 2008 18:00 UTC
Last Modified: 20 Oct 2015 14:22 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/13830 (The current URI for this page, for reference purposes)
Boiten, Eerke Albert: https://orcid.org/0000-0002-9184-8968
  • Depositors only (login required):