ابزار کاربر

ابزار سایت


درس:۴۰۷۴۵

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

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.
درس/۴۰۷۴۵.txt · آخرین ویرایش: 2019/12/26 01:59 (ویرایش خارجی)