Skip to main content
Kent Academic Repository

Inconsistency and underdefinedness in Z specifications

Miarka, Ralph (2002) Inconsistency and underdefinedness in Z specifications. Doctor of Philosophy (PhD) thesis, University of Kent. (doi:10.22024/UniKent/01.02.86002) (KAR id:86002)

PDF (miarka_inconsistency.pdf)
Language: English


Download this file
(PDF/22MB)
[thumbnail of miarka_inconsistency.pdf]
Preview
Postscript (miarka_inconsistency.ps)
Language: English


Download this file
(Postscript/1MB)
[thumbnail of miarka_inconsistency.ps]
Preview
Official URL:
https://doi.org/10.22024/UniKent/01.02.86002

Abstract

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.

Item Type: Thesis (Doctor of Philosophy (PhD))
Thesis advisor: Derrick, John
Thesis advisor: Boiten, Eerke Albert
DOI/Identification number: 10.22024/UniKent/01.02.86002
Additional information: This thesis has been digitised by EThOS, the British Library digitisation service, for purposes of preservation and dissemination. It was uploaded to KAR on 09 February 2021 in order to hold its content and record within University of Kent systems. It is available Open Access using a Creative Commons Attribution, Non-commercial, No Derivatives (https://creativecommons.org/licenses/by-nc-nd/4.0/) licence so that the thesis and its author, can benefit from opportunities for increased readership and citation. This was done in line with University of Kent policies (https://www.kent.ac.uk/is/strategy/docs/Kent%20Open%20Access%20policy.pdf). If you feel that your rights are compromised by open access to this thesis, or if you would like more information about its availability, please contact us at ResearchSupport@kent.ac.uk and we will seriously consider your claim under the terms of our Take-Down Policy (https://www.kent.ac.uk/is/regulations/library/kar-take-down-policy.html).
Uncontrolled keywords: Software, computer programming
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
SWORD Depositor: SWORD Copy
Depositing User: SWORD Copy
Date Deposited: 29 Oct 2019 16:24 UTC
Last Modified: 15 Dec 2022 06:34 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/86002 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.