Handling Inconsistencies in Z Using Quasi-Classical Logic
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 Zsc hemas. 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 Zoperation 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.
KeywordsClassical Logic Proof Theory Operation Change Paraconsistent Logic Expansion Rule
Unable to display preview. Download preview PDF.
- Abrial, J.-R. (1996). The B-Book: Assigning Programs to Meanings. Cambridge University Press.Google Scholar
- Arthan, R. D. (1991). Formal Specification of a Proof Tool. In Prehn, S. and Toetenel, H., editors, Proceedings of Formal Software Development Methods (VDM’ 91), Lecture Notes in Computer Science 552, pages 356–370, Berlin, Germany. Springer.Google Scholar
- Balzer, R. (1991). Tolerating Inconsistency. In Proceedings of the 13th International Conference on Software Engineering, pages 158–165. IEEE Computer Society Press / ACM Press.Google Scholar
- Batens, D. (1999). Inconsistency-Adaptive Logics. In Orlowska, E., editor, Logic at Work. Essays Dedicated to the Memory of Helena Rasiowa, Studies in fuzziness and soft computing, Volume 24, pages 445–472, Heidelberg, New York. Physica-Verlag.Google Scholar
- Batens, D. (2000). A Survey of Inconsistency-Adaptive Logics. In (Batens et al., 2000), pages 49–73.Google Scholar
- Besnard, P. and Hunter, A. (1995). Quasi-Classical Logic: Non-Trivializable Classical Reasoning from Inconsistent Information. In Froidevaux, C. and Kohlas, J., editors, Proceedings of the ECSQARU European Conference on Symbolic and Quantitive Approaches to Reasoning and Uncertainty, Lecture Notes in Artificial Intelligence 946, pages 44–51, Berlin. Springer Verlag.Google Scholar
- da Costa, N. C. (2000). Paraconsistent Mathematics. In (Batens et al., 2000), pages 165–179.Google Scholar
- Fitting, M. C. (1996). First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science. Springer-Verlag, Berlin, 2nd edition.Google Scholar
- Ghezzi, C. and Nuseibeh, B. (1998). Guest Editorial: Introduction to the Special Section: Managing Inconsistency in Software Development. IEEE Transactions on Software Engineering, 24(11):906–907.Google Scholar
- Hunter, A. (1998). Paraconsistent Logic. In Besnard, P. and Hunter, A., editors, Reasoning with Actual and Potential Contradictions, Volume II of Handbook of Defeasible Reasoning and Uncertain Information (Gabbay, D. and Smets, Ph., editors), pages 13–44. Kluwer Academic Publishers, Dortrecht, The Netherlands.Google Scholar
- Hunter, A. (2001). A Semantic Tabeau Version of First-Order Quasi-Classical Logic. In Benferhat, S. and Besnard, P., editors, Symbolic and Quantitative Approaches to Reasoning with Uncertainty, Proceedings of the 6th European Conference, ECSQARU 2001, Toulouse, France, Lecture Notes in Artificial Intelligence 2143, pages 544–555. Springer Verlag.Google Scholar
- Hunter, A. and Nuseibeh, B. (1997). Analysing Inconsistent Specifications. In Proceedings of the 3rd International Symposium on Requirements Engineering (RE’97), pages 78–86. Annapolis, USA, IEEE Computer Society Press.Google Scholar
- Miarka, R., Boiten, E., and Derrick, J. (2000). Guards, Preconditions, and Refinement in Z. In Bowen, J. P., Dunne, S., Galloway, A., and King, S., editors, ZB2000: Formal Specification and Development in Z and B / First International Conference of B and Z Users, Lecture Notes in Computer Science 1878, pages 286–303, Berlin Heidelberg New York. Springer-Verlag Berlin.Google Scholar
- Mortensen, C. (1995). Inconsistent Mathematics. Kluwer Academic Publishers Group, Dordrecht, The Netherlands.Google Scholar
- Saaltink, M. (1997). The Z/EVES User’s Guide. Technical Report TR-97-5493-06, ORA Canada, 267 Richmond Road, Suite 100, Ottawa, Canada.Google Scholar
- Schwanke, R. W. and Kaiser, G. E. (1988). Living with Inconsistency in Large Systems. In Proceedings of the International Workshop on Software Version and Configuration Control, pages 98–118, Grassau, Germany.Google Scholar
- Smullyan, R. M. (1968). First-Order Logic, Volume 43 of Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, New York.Google Scholar
- Valentine, S. H. (1998). Inconsistency and Undefinedness in Z-A Practical Guide. In Bowen, J. P., Fett, A., and Hinchey, M. G., editors, ZUM’98: The Formal Specification Notation, Lecture Notes in Computer Science 1493, pages 233–249, Berlin Heidelberg New York. Springer Verlag.CrossRefGoogle Scholar
- Woodcock, J. and Davies, J. (1996). Using Z-Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Prentice Hall Europe. Online: http://softeng.comlab.ox.ac.uk/usingz/ (last access 18/10/2001).