در علوم رایانه و مهندسی نرم‌افزار، روشهای صوری یا روش‌ها رسمی (به انگلیسی Formal methods) نوع خاصی از شگردهای ریاضی-پایه برای توصیف، تخصیص، ایجاد، توسعه، و تولید برنامه سامانه‌های سخت‌افزاری و نرم‌افزاری هستند. استفاده از روشهای صوری برای طراحی سخت‌افزار و نرم‌افزار تحت تأثیر خواسته‌ها و انتظارات قرار می‌گیرد.
مثل چهارچوب سایر مهندسی‌ها، به اجرا درآوردن تحلیل‌های ریاضی مناسب می‌تواند به استواری و قابل اعتماد بودن طرح کمک کند. به هر حال، مقیاس زیاد استفاده از روشهای صوری به این معنا است که به‌طور معمول فقط در توسعه سامانه‌های بی‌نقص، جایی که ایمنی یا تضمین سامانه اهمیت دارد مثل سیستم‌های مراقبت پرواز، استفاده می‌شود.
روشهای صوری می‌توانند در نقاط مختلف فرایند ایجاد و توسعه به کارگرفته شوند (برای راحتی و آسودگی، ما می‌توانیم از واژه‌ای مشترک به مدل آبشاری استفاده کنیم، گرچه هر فرایند پیشرفتی باید مورد استفاده قرار گیرد)
برای توسعه سامانه در هر سطح مطلوب، از تعریف‌های روشهای صوری می‌توان استفاده کرد. این تعریف رایج می‌تواند جهت هدایت فعالیت‌های توسعه استفاده شود علاوه بر این می‌تواند مشخص کند که نیازهای سامانه به‌طور کامل و دقیق تشخیص داده شده‌اند. نیاز برای ویژگی‌ها سامانه‌های صوری (رسمی) برای سالهاست که مشخص شده‌است. در راس الغول(زبان برنامه‌نویسی الگول) ۶۰ گزارش، John Backus یک نماد صوری (رسمی) ای در دستور این زبان برنامه‌نویسی ارائه کرده‌است (که بعداً شکل نرمال Backus یا Backus-Naur form نامیده شد. Backus همچنین یک نیاز به یک نماد برای توصیف معناشناسی این زبان توصیف کرد. گزارش معهود که یک نماد جدید بود، همانند BNF در آینده نزدیک ظاهر خواهد شد، یا ظاهر نخواهد شد.
فقط ویژگی‌های صوری (رسمی) توسعه یافته‌است، ویژگی‌ها ممکن است به عنوان راهنما باشد، وقتی که سامانه مجزا پیشرفت می‌کند. (به عبارت دیگر در سخت‌افزار یا نرم‌افزار تحقق می‌یابد)
- اگر ویژگی‌های صوری (رسمی) در یک عملیات معنایی است، رفتار مشاهده شدهٔ سامانه مجزا می‌تواند با رفتار ویژگی‌ها مقایسه شود (که خودش باید قابل اجرا یا قابل شبیه‌سازی باشد) به علاوه، دستورهای عملیاتی ویژگی‌ها ممکن است که به کد قابل اجرا از طریق انتقال مستقیم، تبدیل شدنی باشد.
- اگر ویژگی‌های صوری (رسمی) در یک معناشناسی بدیهی باشد، شرایط قبلی و شرایط بعدی ویژگی‌ها ممکن است که به ادعاهایی در کد قابل اجرا تبدیل شوند.
هر بار که یک ویژگی‌ها صوری (رسمی) توسعه می‌یابد، ویژگی‌ها ممکن است که به عنوان پایه‌هایی برای خواص اثباتِ ویژگی‌ها استفاده شود (و امیدوارانه با استنتاج سامانه پیشرفته).
اثبات انسانی
در بعضی مواقع، اقدام برای اثبات درستی یک سامانه مطلقاً نیاز به درستی سامانه ندارد، اما یک عاملی است برای بهتر فهمیدن سامانه. متناوباً بعضی اثبات‌ها از طریق اثبات‌های ریاضی انجام می‌شود. استفاده از زبان طبیعی چه به صورت دست نوشته یا تایپ شده، از یک سطح فرمالیتهٔ از این اثبات‌ها استفاده می‌کنند. اثبات خوب اثباتی است که توسط دیگر خوانندگان، قابل خواندن و قابل فهم باشد.
اثبات خودکار
در مقابل، علاقهٔ زیادی به استفاده از اثبات‌های خودکار برای اثبات درستی چنین سامانه‌هایی وجود دارد.
اثبات‌های خودکار به دو دسته تقسیم می‌شوند:
# اثبات قضیهٔ اتومات شده،
- بررسی نمونه،
شاخه روشهای صوری انتقادهای خاص خود را دارد. در وضعیت حال هنر، دلایل درستی‌ها، چه با دست نوشته شود یا با رایانه برای تولید، با سود محدود به جای اطمینان درست، نیاز قابل توجهی به زمان دارند (و به پول). این باعث می‌شود که روشهای صوری بیشتر در شاخه‌ها که سودهای داشتن چنین اثبات‌هایی به کار برده شوند، یا خطر افتادن در خطاهای کشف نشده، ارزش آنها را ذخیره می‌کند. در حال حاضر استدلال کننده‌های روشهای صوری ادعا کرده‌اند که تکنیک‌های آنها مانند گلوله نقره‌ای خواهد بود در بحران سخت‌افزاری. البته، به‌طور گسترده اعتقاد بر این است که هیچ گلوله نقره‌ای و هیچ راه‌حل جادویی برای پیشرفت نرم‌افزار وجود ندارد و بعضی‌ها خارج از روشهای رایج نوشته شده‌اند به خاطر برخی گزافه‌گویی‌ها و ادعاهای بیش از حد.
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
