حسن حقیقی - دانشجوی دکتری دانشکده مهندسی کامپیوتر دانشگاه صنعتی شریف
سیدحسن میریان حسین آبادی - استادیار دانشگاه صنعتی شریف

هدف از توصیف بیان دقیق و بدون ابهام نیازمندیهای نرم افزار با استفاده از زبان ریاضی است وجود عدم قطعیت در توصیف صوری به دلیل سطح تجرید مورد نیاز در توصیف نرم افزار و نیز توصیف سیستمهای همروند اجتناب ناپذیر است به همین دلیل بیان عدم قطعیت و معنای ساختارهای غیرحتمی در توصیف صوری اهمیت ویژه ای دارد دراین پژوهش رهیافتی برای استفاده از ساختارهای غیرحتمی و بیان معنای آنها در توصیفهای صوری تئوری انواع مارتین لوف ارایه خواهد شد استفاده ازا ین ساختارهای پیشنهادی موجب میشود که توصیف گر بتواند ضمن توصیف صریح عدم قطعیت در تئوریانواع اثرات آن را به طور مستقیم در برنامه استخراج شده از توصیف صوری مشاهده نماید.

توصیف صوری، عدم قطعیت، تئوری انواع مارتین لوف، نمایش عدم قطعیت در تئوری انواع مارتین لوف