ON THE CORRECTNESS OF A TRANSLATION MAP BETWEEN SPECIFICATIONS IN Z AND SETL۲ PROTOTYPE
سال انتشار: 1388
نوع سند: مقاله ژورنالی
زبان: انگلیسی
مشاهده: 113
فایل این مقاله در 7 صفحه با فرمت PDF قابل دریافت می باشد
- صدور گواهی نمایه سازی
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
JR_ITRC-1-2_005
تاریخ نمایه سازی: 23 فروردین 1401
چکیده مقاله:
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 SetL۲ 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.
کلیدواژه ها:
نویسندگان
Behnaz Changizi
Coordination Languages Group Center of Mathematics and Informatics Amsterdam, The Netherlands
Seyyed Hassan Mirian Hossinabadi
Computer Department Sharif University of technology Tehran, Iran