تولید برنامه از توصیف رسمی

Formal Program Development

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

اهداف درس

این درس برای دانش‌جویان کارشناسی ارشد و دکتری ارایه می‌شود و هدف از آن پرداختن به روش‌های تولید برنامه از توصیف رسمی سیستم‌ها به طور سیستماتیک است. در این درس تولید برنامه از توصیف صوری و به خصوص تقلید مورد بحث قرار می‌گیرد. روش‌های دیگر از جمله جبر پالایش مورگان، متدولوژی B، تئوری انواع (Type Theory) و نسخه ساختی Z معرفی می‌گردند. ضمناً در حد امکان ابزارهای لازم برای به‌کارگیری این روش‌ها معرفی می‌گردد.

ریز مواد

  1. مقدمه‌ای بر تولید برنامه (۱ جلسه)
    • چرا تولید برنامه از توصیف رسمی؟
    • تولید برنامه (تبدیل، پالایش، تقلید و تئوری انواع)
  2. چرا لزوما توصیف صوری مستقیما قابل اجرا نیست؟ (۲ جلسه)
  3. تقلید (Animation) توصیف صوری (۳ جلسه)
    • تقلید با استفاده از زبان‌های تابعی
    • تقلید با استفاده از زبان‌های منطقی
    • معرفی ابزارهای تقلید
  4. جبر پالایش مورگان (۸ جلسه)
    • برنامه‌ها و پالایش
    • انواع و اعلان‌ها
    • جایگزینی و ترکیب ترتیبی
    • جملات انتخابی
    • ثابت‌های منطقی
    • حلقه‌های تکرار
    • مثال
    • معنای قوانین پالایش
  5. متدولوژی B (۸ جلسه)
    • ماشین‌های انتزاعی
    • ساختن توصیف
    • طراحی و پالایش
    • اثبات و پیاده‌سازی
    • مثال
  6. تئوری انواع (۸ جلسه)
    • مقدمه‌ای بر ریاضیات ساختی (Constructive Mathematics)
    • زبان برنامه نویسی در تئوری انواع Martin-Löf
    • قواعد استنتاج در تئوری انواع Martin-Löf
    • تئوری مجموعه‌های ساختی CZ
    • اثبات درستی توصیف در CZ
    • ترجمه درخت اثبات در CZ به درخت اثبات در تئوری انواع Martin-Löf
    • استخراج برنامه از درخت اثبات در تئوری انواع Martin-Löf
    • مثال

ارزیابی

مراجع

  1. I. J. Hayes, and C. B. Jones. Specification are not (necessarily) executable. Technical report UMCS-89-12-1, Computer Science Department, University of Manchester, December, 1989.
  2. N. E. Fuchs. Specifications are(Preferably) Executable. Software Engineering Journal, Volume 7, No. 5, pp. 323-334, September, 1992.
  3. A. Diller. Z: An Introduction to Formal Methods. Wiley, 1992.
  4. X. Jia. A Tutorial of ZANS - A Z Animation System. Version 0.21, Electronically available from: ftp://ise.cs.depaul.edu, May, 1995.
  5. S. H. Valentine. Z–, an Executable Subset of Z. In John E. Nicholls, editor, Z User Workshop, York 1991, Workshops in Computing, Springer-Verlag, pp. 157-187, 1992.
  6. C. Morgan. Programming from Specifications. Prentice-Hall, 1990.
  7. K. Lano and H. Haughton. Specification in B: An Introduction Using the B Toolkit. Imperial College Press, 1996.
  8. B. Nordstrom, K. Petersson, and J. M. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, 1990.
  9. J. Woodcock, J. Davies. Using Z Specifications, Refinement, and Proof. Prentice-Hall Europe, 1996.
  10. D. Gries, and F. B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.