ON THE CORRECTNESS OF A TRANSLATION MAP BETWEEN SPECIFICATIONS IN Z AND SETL2 PROTOTYPE

Formal specification as a precise description of software requirements plays an important role in thesoftware development processes. it can be used as a measurement for validating the artifacts of almost all stages in thedevelopment process. hence, making effort on validating the correctness of the formal specification against therequirements in the very early stages of development is of a high value. extracting prototype from formalspecification can be a kind of such a validation. in this article, we propose a translation set of rules for buildingexecutable prototypes written in setl2 language from formal specification in z formal language. then, we investigatethe correctness of the translation with help of some lemmas based on weakest precondition predicate transformer andrefinement relationship.