A method to convert Z specification into algebraic specification using Skolem normal form

摘要

The formal specification language Z has been used to specify a wide spectrum of software systems. Specifications expressed using the Z notation have to be checked whether they satisfy some requirement or not. As the scale of software systems are growing, it is difficult to check manually. To clear the problem, there are many approaches to proof support for Z. We have suggested how to convert specifications in Z into the representation of an algebraic specification language that has an implementation. Some restricted specifications are allowed to convert. In this paper, we suggest how to convert the predicate part of the scheme including quantifiers into the representation of an algebraic specification language using Skolem Normal Form. In present, we have to edit a part of the algebraic specifications generated such a method. By improving our method, we can expect an efficient computer-assisted checking for the specification of large and/or complicated software systems.