Abstract
A software formal specification is useful if and only if it is consistent or non-conflictive. However, checking the correctness or consistency of a formal specification is a difficult task. This paper proposes a method to prove its consistency or correctness by generating relevant theorem proofs. Checking the correctness and consistency of Object-Z formal specification is the main goal, which can make the specifier to get confident. Because Object-Z has inheritance property, this paper discusses it from different aspects, and focuses on the reuse of theorem proof. Finally, theorem prover Z/EVES is used to analyze and verify the Object-Z theorem proofs (semi-)automatically.
Introduction
In software development process, the combination of object-oriented and formal method has become a tendency. Object-Z [1] is an extension of process-oriented formal specification language Z, that is able to describe large scale object-oriented formal specification. Mathematical logic and set theory are its theoretical foundation. Therefore, we can reason the behaviors and attributes of formal specification easily. Verification including theorem proving and mode checking can ensure the consistency and correctness for an Object-Z formal specification.
There have been many researches on theorem proof and formal verification at home and abroad that it is able to reason about the properties of formal specification. In paper [6], relevant inference rules and methods for Object-Z formal specification have been proposed. Generally, Object-Z class properties can be represented as a sequential form: A::
There are two parts of the work to check a formal specification: firstly, generating relevant theorem proofs (
In this section, a brief introduction to Object-Z will be introduced. The structure of Object-Z formal specification is composed of global definitions and class definitions. The set of global variables can be shared by all class definitions. The global definitions and the paragraphs in each class can be described with Z notation. The structure of Object-Z formal specification for a class definition is shown as follows:
A class structure of Object-Z may contain parameters, encapsulates types, constants, variables, operations, inherit property and so on.
Elevator operation systems
In this paper, as an example to illustrate check the consistency of Object-Z formal specification based on theorem proof, it can be described by an elevator operation system through. This elevator operation system includes state schema, initial state, and request operation, run operation and so on. This is the main parts of formal specifications of the elevator operation system as follows.
State schema
According to Object-Z syntax, this is the state schema of an elevator operation system as follows:
Initial state
This is the initial state of elevator operation system as follows:
Request operation
Request operation can be divided into two request operations (i.e. outrequest operation and inrequest operation), including press inside or outside keys of the elevator, hoping go to a certain floor.
The outrequest operation
The outrequest operation may be divided into up and down direction operations:
The Outrequest operation is composed of Outuprequest and Outdownrequest operations. Thus, it has: Outrequest
The inrequest operation
The inrequest operation of elevator is the request inside the elevator, hoping go to the floor.
Thus, the request operation may be composed of inrequest operation and outrequest operation, i.e. Request
Run operation
The run operation of elevator is composed of up-runing operation and down-runing operation:
Thus, the run operation has: Run
Theorem proof
Theorem proof has been applied in order to check the consistency or correctness of the developed formal system in paper [12, 13, 14]. In this section, we will generate relevant theorem proofs from a base class or operation of a formal specification. In order to check specification’s consistency, we should consider the specification is not conflictive first. Otherwise, the specification hasn’t any significance because it is conflictive. In this case, it is not taken into account in paper [9] at all. It is regarded as compatibility and non-confliction acquiescently. In addition to this, we will consider the partial functions or operators whether they are complete in this specification.
Consistency of Object-Z specification
If the invariant is consistent, there is at least one state space. An operation can transform one state into another in a state space. It is necessary to check the consistency between an operation and its state space. Therefore, if a formal specification itself is conflictive, there may be no state space or initial state. Furthermore, operations including initial operation may not be compatible with the state space.
State space existence
According to Object-Z syntax and semantics, there may be global or local definitions in a class, including constants, variables, types, function definitions and so on, which all can be regarded as context information identified as Context. Note that variables defined in the state schema cannot be considered as context information. Generally, the Context is assumed to be consistent. Variables defined in a state schema can be represented as
If an invariant of an Object-Z class is not conflictive, there exists a state space at least. From the context information, it may be true:
If this inference relationship does not exist, the invariant is conflictive. Hence, the theorem proof is true:
TP1’: Context
Here, Context
Initial state existence
Initial state is a state in a state space of Object-Z class. If an Object-Z specification is consistent or correct, the initial state should exist and satisfy its state invariant. There is a theorem proof:
There into, the context of initial state is: Context
[A
TP2’:
upset
Operation feasibility
In a state space, an operation can transform one state into another. If an operation is feasible in the formal specification, there should be a pre- and post-position state satisfying its invariant. Otherwise, the operation is incompatible or inconsistent with itself invariant. Invariant is implicitly included into any operation. Therefore, a theorem proof can be produced for each operation:
In TP3,
About the operation Outuprequest above, it may be true:
[A
TP3’:
((tag
About the operation Outdownrequest above, it may be true:
[A
TP3’:
((tag
Hence, if the inference relationship of above theorem proof does not exist, it means that the operation Outuprequest or Outdownrequest with this invariant may be conflictive. Other operations are similar.
Checking precondition or postcondition
Let the invariant of an Object-Z class be Invariant(x), here, x:X is the state variables and their corresponding types. The possible input & output variables and the corresponding types in an operation are input:INPUT, output:OUTPUT. Due to state invariant including in an operation implicitly, the precondition and postcondition of an operation may be regarded as two theorem proofs:
If an Object-Z formal specification is correctness or non-conflictive, there may exist pre- & post-conditions for each operation. Thus, the pre- & post-conditions of each operation above, for the outuprequest operation are:
[A
TP:
((tag
Generating TPs for relevant properties
For an Object-Z formal specification, there may hold several obvious properties. For example, for the Elevator operation system, there are two operations in class Elevator: Uprun and Downrun. If the operation Uprun may be executed first and the operation Downrun later, the story of floor should be unchanged, i.e., story”
Implicitly, invariant of a class can be included into every operation. Thus, the theorem proof TP6_1 above is simplified as the theorem proof TP6’:
TP6_1’: Context
Hence, this theorem proof is equivalent to:
[A
TP6_1’:
For another example, when the elevator runs up or down, the door of the elevator is closed. Therefore, there is:
Hence, this theorem proof is equivalent to:
[A
TP6_2’:
According to this method, we can generate relevant theorem proofs for other operations. Other properties are similar.
Checking TPs in Z/EVES automatically
According to theory foundation above, relevant theorem proofs for Object-Z formal specification can be generated in order to checking its consistency or correctness. In this section, a method is presented to generate theorem proof and export it to theorem prover Z/EVES [7] to be checked. Prover Z/EVES is a very excellent theorem prover, with general theorem proving function, and can prove non-Z theorems that should accord to Z/EVES syntax. Z/EVES have two styles: explorative and planned.
This section illustrates how to generate theorem proofs (TPs) from Object-Z formal specification and can be directly imported to theorem prover Z/EVES to be proved directly. In the process of explorative proof, a user without knowing how to prove, it begins with a certain target to prove. If lucky, the goal can be proved when various proof commands can be used to explore the proof space. In the process of planned proof, users need to spend some time before starting to work the Z/EVES to make informal evidence of their goals. Generally, checking a theorem proof can use planned proof method. That is to say, it requires manual interventions that need to do several works before proving it.
The theorem proofs generated in previous sections have been checked in prover Z/EVES. TP2 will be used to show how to check it.
Editing a theorem proof
First, we should edit the theorem to be proved in theorem prover Z/EVES. When we run the theorem prover Z/EVES, the main window (specification window) is displayed first shown in Fig. 2. Of course, the main window (specification window) is blank at first. Choosing the “New paragraph” command from “Edit” menu shown in Fig. 2, we can enter the edit window shown in Fig. 1 and type content. When input is finished, choosing the “Done” command from “File” menu can enter the main window. According to this, we can edit the theorem proofs that need to be proved in it.
Edit window.
In theorem prover Z/EVES, planned proof methods may be used, so it can suppose
After editing, we can use the prover Z/EVES to prove this theorem step and step. First, it can select “Check all paragraphs” from the “Command” menu to check whether its syntax meets the requirements. The “Y” notation in the syntax column indicates no syntax or type errors. The “N” notation in the “proof” column indicates that this theorem needs proof. In Fig. 2, the theorem Initial_state is checked, and the syntax status bar holds “Y” because there are no syntax or type errors, but the “Proof” column will hold “N”. We will prove this theorem in Section 5.3.
Specification window.
In proof window, there are three functions: inspection and modification of proof script, interactive construction proof and proof browsing shown in Fig. 3. In this section, we will prove the initial_state theorem in Z/EVES. The proof window will be displayed shown in Fig. 3, when we select the initial_ state theorem proof and choose “show proof” from the pop-up menu in Fig. 2.
Here, in order to prove this theorem proof Initial_state, the used commands are prove and prove by reduce. The proof steps are shown as follows:
Automatically proof:
prove prove by reduce
Proof window.
When running these two commands step by step, the notation “true” will be displayed in the formula window finally, indicating that the theorem Initial_state has been verified and the run status bar holds a “Y” for every command. So, the experiments with Z/EVES show that the theory above is correct.
A software formal specification is useful if and only if it is consistent or non-conflictive. However, in the development process formal specifications may not be consistent or conflictive. Moreover, formal specifications are generally not executable. Runtime syntax and semantic detection are not suitable. However, checking the correctness or consistency of formal specifications is a difficult task. This paper proposes a method to prove its consistency or correctness by generating relevant theorem proofs, requiring that the specification itself is not conflictive first. Next, it needs to verify some attribute. Finally, theorem prover Z/EVES is used to analyze and verify the theorem proofs that ensure the formal specification is consistent or non-conflictive.