School of Computing

Handling inconsistencies in z using quasi-classical logic

Ralph Miarka, John Derrick, and Eerke Boiten

In Didier Bert, Jonathan P. Bowen, Martin C. Henson, and 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 182-196, Grenoble, France, January 2002. Springer-Verlag Berlin Heidelberg.

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 publication 92 kbytes

Bibtex Record

@inproceedings{1340,
author = {Ralph Miarka and John Derrick and Eerke Boiten},
title = {Handling Inconsistencies in Z using Quasi-Classical Logic},
month = {January},
year = {2002},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2002/1340},
    publication_type = {inproceedings},
    submission_id = {18268_1012228548},
    ISBN = {3-540-43166-7},
    booktitle = {ZB2002: Formal Specification and Development in Z and B / Second International Conference of B and Z Users},
    editor = {Didier Bert and Jonathan P. Bowen and Martin C. Henson and Ken Robinson},
    volume = {2272},
    series = {Lecture Notes in Computer Science},
    address = {Grenoble, France},
    publisher = {Springer-Verlag Berlin Heidelberg},
    ISSN = {0302-9743},
    refereed = {yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014