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

Program Specification and Verification

شماره درس: ۴۰۷۴۵ تعداد واحد: ۳
مقطع: کارشناسی ارشد نوع درس: نظری
پیش‌نیاز: – هم‌نیاز: –

اهداف درس

این درس برای دانش‌جویان کارشناسی ارشد و دکتری ارایه می‌شود و هدف از آن پرداختن به روش‌های صوری برای توصیف و وارسی سیستم‌ها است. در این درس ابزارهای لازم برای به کارگیری این روش‌ها معرفی و در مورد رابطه بین توصیف صوری و پیاده‌سازی به طور اختصار بحث می‌گردد.

ریز مواد

  • مقدمه‌ای بر توصیف سیستم‌ها (۲ جلسه)
    • چرا توصیف صوری؟
    • توصیف صوری و مهندسی نرم‌افزار
    • تولید برنامه از توصیف (پالایش)
  • جبر گزاره‌ها، جبر مسندات (۲ جلسه)
  • تئوری مجموعه‌ها و زبان Z (۴ جلسه)
    • تساوی
    • انواع، مجموعه‌ها و عملیات روی آن‌ها
    • تعاریف
    • روابط و عملیات روی آن‌ها
    • توابع و عملیات روی آن‌ها
    • مثال
  • واحدهای ساختاری توصیف (۴ جلسه)
    • شِما (Schema) و نحوه مدل کردن سیستم
    • استفاده از شِما به عنوان اعلان، نوع و مسند
    • شِمای ژنریک
    • نحوه بیان اصول (Axiomatic Description)
    • مثال
  • جبر شِماها (Schema Calculus) (۴ جلسه)
    • تغییر متغیر (Renaming and Decoration)
    • ترکیب شِماها با استفاده از عملگرهای منطقی و Inclusion
    • مثال
  • ابزارگان ریاضی Z (۲ جلسه)
    • ردیف‌ها و Bagها و عملیات روی آن‌ها
    • نوع آزاد (Free Type)
    • مثال
  • توصیف با استفاده از ارتقا (Promotion) (۲ جلسه)
  • امکان پذیری توصیف و محاسبه پیش شرط‌ها (Precondition) (۲ جلسه)
  • وارسی (Verification)(۶ جلسه)
    • اصول تئوری مجموعه‌ها
    • قوانین استنتاج
    • قضیه حالت اولیه سیستم
    • ساده‌سازی پیش‌شرط‌ها
    • اثبات خصوصیات توصیف
    • مثال
  • تولید برنامه از توصیف صوری Z با استفاده از پالایش (Refinement) (۲ جلسه)
    • پالایش ساختارهای داده‌ای
    • پالایش عملیات
    • مثال

ارزیابی

  • تمرین (۱۵ درصد نمره) و پروژه (۱۵ درصد نمره):
    • دانشجویان به گروه‌های ۲ یا ۳ نفره تقسیم می‌شوند و هر گروه سه صورت برنامه در اندازه‌های کوچک، متوسط و بزرگ را پیشنهاد می‌نماید. پس از تصویب برنامه‌ها، هر گروه تمرینات (حداقل ۳ تمرین) را در طول ترم براساس مسایل پیشنهادی خود پاسخ خواهد داد.
    • برنامه بزرگ صورت پروژه هر گروه را مشخص می‌کند که یک ماه پس از پایان امتحانات فرصت دارند تا توصیف صوری کامل پروژه را تحویل نمایند.
    • دانشجویان باید با استفاده از نرم‌افزارهای کنترل کننده جامعیت و عدم تناقض و اثبات قضیه خصوصیات توصیف صوری خود را مورد ارزیابی قرار دهند.
  • سمینار: دانش‌جویان به طور اختیاری سمیناری را در ارتباط با مطالب درس پس از گرفتن تایید ارایه می‌نمایند (۱۰ درصد نمره اضافه).
  • آزمون: حدود ۷ آزمون کوچک به جای امتحان میان ترم (۱۵ درصد نمره)، و آزمون نهایی (۵۵ درصد نمره)

مراجع

  1. J. Woodcock and J. Davies. Using Z Specifications, Refinement, and Proof. Prentice-Hall Europe, 1996.
  2. D. Gries and F.B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.
  3. C. Morgan. Programming from Specifications. Prentice-Hall, 1990.