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

تولید نرم افزار به روش های سنتی با مشکلاتی نظیر عدم اطمینان از دسترسی عملکرد آن همراه است. استفاده از روش های صوری برای توصیف سیستم های نرم افزاری موجب کاهش این عدم اطمینان خواهد شد. از سوی دیگر، خلا موجود بین فازهای توصیف و تولید برنامه باعث شده تا به اطمینان از درستی عملکرد، در مرحله ی تبدیل توصیف به برنامه خدشه وارد شود. روش های مختلفی برای رسیدن به برنامه از توصیف صوری پیشنهاد شده که استخراج برنامه از اثبات درستی توصیفی یکی از این روش هاست. در این نوشتار، محیطی برای تولید نرم افزار مطمئن معرفی و پیشنهاد می شود که استخراج برنامه از اثبات توصیف صوری نرم افزار است. توصیف های صوری در قالب نسخه یی از زبان z، با علامت اختصاری cz، نوشته می شوند و اثبات درستی این توصیف ها به اثبات درستی در نظریه ی انواع مارتین لوف ترجمه می گردند. در نهایت برنامه از درخت اثبات ترجمه شده درستی تاییده شده استخراج می شود.