International Journal of Information and Communication Technology Research
مجله بین المللی ارتباطات و فناوری اطلاعات
International Journal of Information and Communication Technology Research
Engineering & Technology
http://ijict.itrc.ac.ir
1
admin
2251-6107
2783-4425
doi
1652
25391
en
jalali
1388
3
1
gregorian
2009
6
1
1
2
online
1
fulltext
en
ON THE CORRECTNESS OF A TRANSLATION MAP BETWEEN SPECIFICATIONS IN Z AND SETL2 PROTOTYPE
فناوری اطلاعات
Information Technology
پژوهشي
Research
<p>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.</p>
Formal Specification, Prototyping, SetL2, Z, Weakest Precondition Predicate Transformer
21
27
http://ijict.itrc.ac.ir/browse.php?a_code=A-10-27-262&slc_lang=en&sid=1
Behnaz
Changizi
1003194753284600940
1003194753284600940
Yes
Coordination Languages Group Center of Mathematics and Informatics Amsterdam, The Netherlands
Seyyed Hassan
Mirian Hossinabadi
1003194753284600941
1003194753284600941
No
Computer Department Sharif University of technology Tehran, Iran