تولید برنامه از توصیف رسمی
Formal Program Development
| شماره درس: ۴۰۶۸۴ | تعداد واحد: ۳ |
| مقطع: کارشناسی ارشد | نوع درس: نظری |
| پیش‌نیاز: – | هم‌نیاز: – |
اهداف درس
این درس برای دانشجویان کارشناسی ارشد و دکتری ارایه می‌شود و هدف از آن پرداختن به روش‌های تولید برنامه از توصیف رسمی سیستم‌ها به طور سیستماتیک است. در این درس تولید برنامه از توصیف صوری و به خصوص تقلید مورد بحث قرار می‌گیرد. روش‌های دیگر از جمله جبر پالایش مورگان، متدولوژی B، تئوری انواع (Type Theory) و نسخه ساختی Z معرفی می‌گردند. ضمناً در حد امکان ابزارهای لازم برای به‌کارگیری این روش‌ها معرفی می‌گردد.
ریز مواد
- مقدمه‌ای بر تولید برنامه (۱ جلسه)
- چرا تولید برنامه از توصیف رسمی؟
- تولید برنامه (تبدیل، پالایش، تقلید و تئوری انواع)
- چرا لزوما توصیف صوری مستقیما قابل اجرا نیست؟ (۲ جلسه)
- تقلید (Animation) توصیف صوری (۳ جلسه)
- تقلید با استفاده از زبان‌های تابعی
- تقلید با استفاده از زبان‌های منطقی
- معرفی ابزارهای تقلید
- جبر پالایش مورگان (۸ جلسه)
- برنامه‌ها و پالایش
- انواع و اعلان‌ها
- جایگزینی و ترکیب ترتیبی
- جملات انتخابی
- ثابت‌های منطقی
- حلقه‌های تکرار
- مثال
- معنای قوانین پالایش
- متدولوژی B (۸ جلسه)
- ماشین‌های انتزاعی
- ساختن توصیف
- طراحی و پالایش
- اثبات و پیاده‌سازی
- مثال
- تئوری انواع (۸ جلسه)
- مقدمه‌ای بر ریاضیات ساختی (Constructive Mathematics)
- زبان برنامه نویسی در تئوری انواع Martin-Löf
- قواعد استنتاج در تئوری انواع Martin-Löf
- تئوری مجموعه‌های ساختی CZ
- اثبات درستی توصیف در CZ
- ترجمه درخت اثبات در CZ به درخت اثبات در تئوری انواع Martin-Löf
- استخراج برنامه از درخت اثبات در تئوری انواع Martin-Löf
- مثال
ارزیابی
- تمرین (۱۵ درصد نمره) و پروژه (۱۵ درصد نمره):
- دانشجویان به گروه‌های ۲ یا ۳ نفره تقسیم می‌شوند و هر گروه سه صورت برنامه در اندازه‌های کوچک، متوسط و بزرگ را پیشنهاد می‌نماید. پس از تصویب برنامه‌ها، هر گروه تمرینات (حداقل ۳ تمرین) را در طول ترم براساس مسایل پیشنهادی خود پاسخ خواهد داد.
- برنامه بزرگ صورت پروژه هر گروه را مشخص می‌کند که یک ماه پس از پایان امتحانات فرصت دارند تا پروژه خود را تحویل نمایند.
- دانشجویان باید حتی‌الامکان با استفاده از نرم‌افزارهای موجود دراین زمینه کار کنند.
- سمینار: دانشجویان به طور اختیاری سمیناری را در ارتباط مطالب درس پس از گرفتن تایید ارایه می‌نمایند (۱۰ درصد نمره اضافه).
- آزمون: حدود ۷ آزمون کوچک به عنوان امتحان میان ترم (۱۵ درصد نمره)، و آزمون نهایی (۵۵ درصد نمره)
مراجع
- 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.
- N. E. Fuchs. Specifications are(Preferably) Executable. Software Engineering Journal, Volume 7, No. 5, pp. 323-334, September, 1992.
- A. Diller. Z: An Introduction to Formal Methods. Wiley, 1992.
- X. Jia. A Tutorial of ZANS - A Z Animation System. Version 0.21, Electronically available from: ftp://ise.cs.depaul.edu, May, 1995.
- 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.
- C. Morgan. Programming from Specifications. Prentice-Hall, 1990.
- K. Lano and H. Haughton. Specification in B: An Introduction Using the B Toolkit. Imperial College Press, 1996.
- B. Nordstrom, K. Petersson, and J. M. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, 1990.
- J. Woodcock, 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.