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

جز
جز (حذف پیوند به خود مقاله با استفاده از AWB)
در [[علوم رایانه]] و [[مهندسی نرم‌افزار]]، '''روش‌های صوری''' یا '''روش‌ها رسمی''' (به [[زبان انگلیسی|انگلیسی]] '''Formal methods''') نوع خاصی از شگردهای [[ریاضی]]-پایه برای توصیف، تخصیص، ایجاد، توسعه، و تولید برنامه [[سامانه|سامانه‌های]]‌های [[سخت‌افزار|سخت‌افزاری]] و [[نرم‌افزار|نرم‌افزاری]] هستند. استفاده از روش‌های صوری برای طراحی [[سخت‌افزار]] و [[نرم‌افزار]] تحت تاثیرتأثیر خواسته‌ها و انتظارات قرار می‌گیرد.{{سخ}}
مثل چهارچوب سایر مهندسی‌ها، به اجرا در آوردندرآوردن [[تحلیل (ریاضی)|تحلیل‌های ریاضی]] مناسب می‌تواند به استواری و قابل اعتماد بودن طرح کمک کند. به هر حال، مقیاس زیاد استفاده از روش‌های صوری به این معنا است که به طوربه‌طور معمول فقط در توسعه سامانه‌های بی‌نقص، جایی که ایمنی یا تضمین سامانه اهمیت دارد مثل سیستم هایسیستم‌های [[مراقبت پرواز]]، استفاده می‌شود.
 
== کاربرد ==
 
== ویژگی‌ها ==
برای توسعه سامانه در هر سطح مطلوب، از تعریف‌های روش‌های صوری می‌توان استفاده کرد. این تعریف رایج می‌تواند جهت هدایت فعالیت‌های توسعه استفاده شود علاوه بر این می‌تواند مشخص کند که نیازهای سامانه به طوربه‌طور کامل و دقیق تشخیص داده شده‌اند.
نیاز برای ویژگی‌ها سامانه‌های صوری (رسمی) برای سالهاست که مشخص شده‌است.
در ''راس الغول([[زبان برنامه‌نویسی]] الگول) '' ۶۰ گزارش، [//[:en.wikipedia.org/wiki/John_Backus:John Backus|John Backus]] یک نماد صوری (رسمی) ای در دستور این زبان [[برنامه نویسیبرنامه‌نویسی]] ارائه کرده‌است (که بعداً شکل نرمال [//[:en.wikipedia.org/wiki/Backus_normal_form:Backus normal form|Backus]] یا [//[:en.wikipedia.org/wiki/:Backus-Naur_formNaur form|Backus-Naur form]] نامیده شد.
''Backus'' همچنین یک نیاز به یک نماد برای توصیف معناشناسی این زبان توصیف کرد.
گزارش معهود که یک نماد جدید بود، همانند ''BNF'' در آینده نزدیک ظاهر خواهد شد، یا ظاهر نخواهد شد.
 
== تکامل ==
فقط ویژگی‌های صوری (رسمی) توسعه یافته‌است، ویژگی‌ها ممکن است به عنوان راهنما باشد، وقتی که سامانه مجزا پیشرفت می‌کند. (به عبارت دیگر در سخت‌افزار یا نرم‌افزار تحقق می‌یابد)
 
== مثال ==
== اثبات ==
هر بار که یک ویژگی‌ها صوری (رسمی) توسعه می‌یابد، ویژگی‌ها ممکن است که به عنوان پایه‌هایی برای
خواص [//[:en.wikipedia.org/wiki/Mathematical_proof:Mathematical proof|اثباتِ]] ویژگی‌ها استفاده شود (و امیدوارانه با استنتاج سامانه پیشرفته).
 
=== اثبات انسانی ===
در بعضی مواقع، اقدام برای اثبات درستی یک سامانه مطلقاً نیاز به درستی سامانه ندارد، اما یک عاملی است برای بهتر فهمیدن سامانه. متناوباً بعضی اثبات‌ها از طریق [[اثبات ریاضی|اثبات‌های ریاضی]] انجام می‌شود. استفاده از [//[:en.wikipedia.org/wiki/Natural_language:Natural language|زبان طبیعی]] چه به صورت [[دست نوشته]] یا تایپ شده، از یک سطح فرمالیتهٔ از این اثبات‌ها استفاده می‌کنند. اثبات خوب اثباتی است که توسط دیگر خوانندگان، قابل خواندن و قابل فهم باشد.
 
=== اثبات خودکار ===
این باعث می‌شود که روش‌های صوری بیشتر در شاخه‌ها که سودهای داشتن چنین اثبات‌هایی به کار برده شوند، یا خطر افتادن در خطاهای کشف نشده، ارزش آنها را ذخیره می‌کند.
در حال حاضر استدلال کننده‌های روش‌های صوری ادعا کرده‌اند که تکنیک‌های آنها مانند گلوله نقره‌ای خواهد بود در بحران سخت‌افزاری.
البته، به طوربه‌طور گسترده اعتقاد بر این است که هیچ گلوله نقره‌ای و هیچ راه‌حل جادویی برای پیشرفت نرم‌افزار وجود ندارد و بعضی‌ها خارج از روش‌های رایج نوشته شده‌اند به خاطر برخی گزافه‌گویی‌ها و ادعاهای بیش از حد.
 
== منابع ==
{{پانویس}}
* Mohammad Reza Nami and Fatemeh Hassani. 2009. [[doi:10.1145/1527202.1527211|A comparative evaluation of the Z, CSP, RSL, and VDM languages]].  ''SIGSOFT Softw. Eng. Notes''  34, 3 (Mayمه 2009۲۰۰۹), 1-4۱–۴
* {{یادکرد-ویکی
|پیوند = http://en.wikipedia.org/wiki/Formal_methods
|بازیابی =
}}
 
* [http://ce.sharif.edu/courses/83-84/2/ce665/resources/root/last%20presentation/Formal%20Methods.ppt مروری بر روشهای رسمی تولید برنامه در مقایسه با روش‌های متداول]
* (انگلیسی) http://shemesh.larc.nasa.gov/fm/fm-what.html