توصیف و وارسی برنامه‌ها

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.