Volume 1, Issue 2 (6-2009)                   2009, 1(2): 21-27 | Back to browse issues page

XML Print

Download citation:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:

Changizi B, Mirian Hossinabadi S H. ON THE CORRECTNESS OF A TRANSLATION MAP BETWEEN SPECIFICATIONS IN Z AND SETL2 PROTOTYPE . International Journal of Information and Communication Technology Research 2009; 1 (2) :21-27
URL: http://ijict.itrc.ac.ir/article-1-292-en.html
1- Coordination Languages Group Center of Mathematics and Informatics Amsterdam, The Netherlands
2- Computer Department Sharif University of technology Tehran, Iran
Abstract:   (2520 Views)

Formal specification as a precise description of software requirements plays an important role in the software development processes. It can be used as a measurement for validating the artifacts of almost all stages in the development process. Hence, making effort on validating the correctness of the formal specification against the requirements in the very early stages of development is of a high value. Extracting prototype from formal specification can be a kind of such a validation. In this article, we propose a translation set of rules for building executable prototypes written in SetL2 language from formal specification in Z formal language. Then, we investigate the correctness of the translation with help of some lemmas based on weakest precondition predicate transformer and refinement relationship.

Full-Text [PDF 1024 kb]   (1430 Downloads)    
Type of Study: Research | Subject: Information Technology

Add your comments about this article : Your username or Email:

Rights and permissions
Creative Commons License This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.