روش‌های صوری: تفاوت میان نسخه‌ها

در ''راس الغول([[زبان برنامه‌نویسی]] الگول) '' ۶۰ گزارش، [http://en.wikipedia.org/wiki/John_Backus John Backus] یک نماد صوری (رسمی)ای در دستور این زبان برنامه نویسی ارائه کرده‌است (که بعداً شکل نرمال [http://en.wikipedia.org/wiki/Backus_normal_form Backus] یا [http://en.wikipedia.org/wiki/Backus-Naur_form Backus-Naur form] نامیده شد.

== تکامل ==

== مثال ==

# اگر ویژگی‌های صوری (رسمی) در یک عملیات معنایی است، رفتار مشاهده شدهٔ سامانه مجزا می‌تواند با رفتار ویژگی‌ها مقایسه شود (که خودش باید قابل اجرا یا قابل شبیه سازی باشد.) به علاوه، دستورهای عملیاتی ویژگی‌ها ممکن است که به کد قابل اجرا از طریق انتقال مستقیم، تبدیل شدنی باشد.

هر بار که یک ویژگی‌ها صوری (رسمی) توسعه می‌یابد، ویژگی‌ها ممکن است که به عنوان پایه‌هایی برای

=== اثبات انسانی ===

در بعضی مواقع، اقدام برای اثبات درستی یک سامانه مطلقاً نیاز به درستی سامانه ندارد، اما یک عاملی است برای بهتر فهمیدن سامانه. متناوباً بعضی اثبات‌ها از طریق [[اثبات ریاضی |اثبات‌های ریاضی]] انجام می‌شود. استفاده از [http://en.wikipedia.org/wiki/Natural_language زبان طبیعی] چه به صورت دست نوشته یا تایپ شده، از یک سطح فرمالیتهٔ از این اثبات‌ها استفاده می‌کنند. اثبات خوب اثباتی است که توسط دیگر خوانندگان، قابل خواندن و قابل فهم باشد.

=== اثبات خودکار ===

در مقابل، علاقهٔ زیادی به استفاده از اثبات‌های خودکار برای اثبات درستی چنین سامانه‌هایی وجود دارد.</br> ''اثبات‌های خودکار به دو دسته تقسیم می‌شوند: '' </br> # اثبات قضیهٔ اتومات شده،

شاخه روش‌های صوری انتقادهای خاص خود را دارد. در وضعیت حال هنر، دلایل درستی‌ها، چه با دست نوشته شود یا با رایانه برای تولید، با سود محدود به جای اطمینان درست، نیاز قابل توجهی به زمان دارند (و به پول).