Research And Implementation Of The First Order Predicate Logic Operator Automatic Refinement In Z Specification

The formal specification notation Z based on set-theory and first order predicate logic is useful for presenting computer-based system without unduly expressing the way in which these properties are achieved. Z is not an executable language generally, so there is no such thing as a Z compiler/link/etc. The models describing some information system in Z language can be reasoned and refined manually as it does in a traditional way. Some people make great efforts towards animating subset of Z while the work is preliminary. We attempt to impose requisite constrains on Z specification aimed at rapidly producing the prototype in specific programming language.The automatic refinement of first order predicate logic operators in Z language is the major point that this thesis focuses on. Firstly, the theoretical possibilities of data structures and calculus proceeding automatically must be proved where the generic computer model of Turning Machine is used and the author's view is pointed out that a computer can implement the algorithm on some level without outsides interference. Secondly, Smart Z the subset of Z language comes into being naturally and the design details and rules are introduced to improve the awareness of the notation's syntax, grammar and semantics. Finally, we employ compiler construction and STL utilities upon automatic refinement of the first order predicate logic operators in Z specification and the standard C++ serves as transient language illustrating how the transformer works.The conclusion of the automatic refinement of Smart Z specification contributes to the significant project of automatic programming.