توصیف و وارسی برنامه‌ها
Program Specification and Verification
| شماره درس: ۴۰۷۴۵ | تعداد واحد: ۳ |
| مقطع: کارشناسی ارشد | نوع درس: نظری |
| پیش‌نیاز: – | هم‌نیاز: – |
اهداف درس
این درس برای دانشجویان کارشناسی ارشد و دکتری ارایه می‌شود و هدف از آن پرداختن به روش‌های صوری برای توصیف و وارسی سیستم‌ها است. در این درس ابزارهای لازم برای به کارگیری این روش‌ها معرفی و در مورد رابطه بین توصیف صوری و پیاده‌سازی به طور اختصار بحث می‌گردد.
ریز مواد
- مقدمه‌ای بر توصیف سیستم‌ها (۲ جلسه)
- چرا توصیف صوری؟
- توصیف صوری و مهندسی نرم‌افزار
- تولید برنامه از توصیف (پالایش)
- جبر گزاره‌ها، جبر مسندات (۲ جلسه)
- تئوری مجموعه‌ها و زبان Z (۴ جلسه)
- تساوی
- انواع، مجموعه‌ها و عملیات روی آن‌ها
- تعاریف
- روابط و عملیات روی آن‌ها
- توابع و عملیات روی آن‌ها
- مثال
- واحدهای ساختاری توصیف (۴ جلسه)
- شِما (Schema) و نحوه مدل کردن سیستم
- استفاده از شِما به عنوان اعلان، نوع و مسند
- شِمای ژنریک
- نحوه بیان اصول (Axiomatic Description)
- مثال
- جبر شِماها (Schema Calculus) (۴ جلسه)
- تغییر متغیر (Renaming and Decoration)
- ترکیب شِماها با استفاده از عملگرهای منطقی و Inclusion
- مثال
- ابزارگان ریاضی Z (۲ جلسه)
- ردیف‌ها و Bagها و عملیات روی آن‌ها
- نوع آزاد (Free Type)
- مثال
- توصیف با استفاده از ارتقا (Promotion) (۲ جلسه)
- امکان پذیری توصیف و محاسبه پیش شرط‌ها (Precondition) (۲ جلسه)
- وارسی (Verification)(۶ جلسه)
- اصول تئوری مجموعه‌ها
- قوانین استنتاج
- قضیه حالت اولیه سیستم
- ساده‌سازی پیش‌شرط‌ها
- اثبات خصوصیات توصیف
- مثال
- تولید برنامه از توصیف صوری Z با استفاده از پالایش (Refinement) (۲ جلسه)
- پالایش ساختارهای داده‌ای
- پالایش عملیات
- مثال
ارزیابی
- تمرین (۱۵ درصد نمره) و پروژه (۱۵ درصد نمره):
- دانشجویان به گروه‌های ۲ یا ۳ نفره تقسیم می‌شوند و هر گروه سه صورت برنامه در اندازه‌های کوچک، متوسط و بزرگ را پیشنهاد می‌نماید. پس از تصویب برنامه‌ها، هر گروه تمرینات (حداقل ۳ تمرین) را در طول ترم براساس مسایل پیشنهادی خود پاسخ خواهد داد.
- برنامه بزرگ صورت پروژه هر گروه را مشخص می‌کند که یک ماه پس از پایان امتحانات فرصت دارند تا توصیف صوری کامل پروژه را تحویل نمایند.
- دانشجویان باید با استفاده از نرم‌افزارهای کنترل کننده جامعیت و عدم تناقض و اثبات قضیه خصوصیات توصیف صوری خود را مورد ارزیابی قرار دهند.
- سمینار: دانشجویان به طور اختیاری سمیناری را در ارتباط با مطالب درس پس از گرفتن تایید ارایه می‌نمایند (۱۰ درصد نمره اضافه).
- آزمون: حدود ۷ آزمون کوچک به جای امتحان میان ترم (۱۵ درصد نمره)، و آزمون نهایی (۵۵ درصد نمره)
مراجع
- J. Woodcock and J. Davies. Using Z Specifications, Refinement, and Proof. Prentice-Hall Europe, 1996.
- D. Gries and F.B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.
- C. Morgan. Programming from Specifications. Prentice-Hall, 1990.