In this paper two algorithms are presented: one which turns an executable OOZE specification into an algebraic specification and another which does the reverse operation. In this way, we shall be able to prove in a constructive way that executable OOZE and algebraic specification are equivalent and that, generally speaking, state-based specification is equivalent to algebraic specification. We shall discuss whether these results can be made to cover other object-oriented Z dialects.
CitationPalasi, V. "Equivalence between executable OOZE and algebraic specification". 1994.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: firstname.lastname@example.org