روش‌های صوری: تفاوت میان نسخه‌ها
محتوای حذف‌شده محتوای افزوده‌شده
جز ربات:انتقال رده > رده:اصول تولید نرمافزار به رده:فلسفههای توسعه نرمافزار به درخواست Calak |
|||
خط ۱۷:
== مثال ==
# اگر ویژگی‌های صوری (رسمی) در یک عملیات معنایی است، رفتار مشاهده شدهٔ سامانه مجزا می‌تواند با رفتار ویژگی‌ها مقایسه شود (که خودش باید قابل اجرا یا قابل [[شبیه‌سازی]] باشد) به علاوه، دستورهای عملیاتی ویژگی‌ها ممکن است که به کد قابل اجرا از طریق انتقال مستقیم، تبدیل شدنی باشد.
# اگر ویژگی‌های صوری (رسمی) در یک ''معناشناسی'' بدیهی باشد، شرایط قبلی و [[شرایط]] بعدی ویژگی‌ها ممکن است که به ادعاهایی در کد قابل اجرا تبدیل شوند.
== اثبات ==
خط ۳۱:
== انتقادها ==
شاخه [[روش‌های صوری]] انتقادهای خاص خود را دارد. در وضعیت حال هنر، دلایل درستی‌ها، چه با دست نوشته شود یا با رایانه برای تولید، با سود محدود به جای اطمینان درست، نیاز قابل توجهی به زمان دارند (و به پول).
این باعث می‌شود که روش‌های صوری بیشتر در شاخه‌ها که سودهای داشتن چنین اثبات‌هایی به کار برده شوند، یا خطر افتادن در خطاهای کشف نشده، ارزش آنها را ذخیره می‌کند.
در حال حاضر استدلال کننده‌های روش‌های صوری ادعا کرده‌اند که تکنیک‌های آنها مانند گلوله نقره‌ای خواهد بود در بحران سخت‌افزاری.
| |||