औपचारिक पद्यतियां: Difference between revisions

From Vigyanwiki
No edit summary
 
(8 intermediate revisions by 6 users not shown)
Line 1: Line 1:
{{Short description|Mathematical program specification intended to allow correctness proofs, including algorithmically}}
[[ कंप्यूटर विज्ञान |कंप्यूटर विज्ञान]] में, [[ सॉफ़्टवेयर |सॉफ़्टवेयर]] और [[ संगणक धातु सामग्री |कंप्यूटर धातु सामग्री,]] हार्डवेयर सिस्टम की विशिष्टता, विकास के '''औपचारिक पद्यतियां''' (फॉर्मल मेथड्स) के लिए गणित की जटिल तकनीकें हैं।<ref name="butler">{{cite web| first=R. W. | last=Butler | title=What is Formal Methods? | url=http://shemesh.larc.nasa.gov/fm/fm-what.html|date=2001-08-06|access-date=2006-11-16}}</ref> सॉफ्टवेयर और हार्डवेयर डिजाइन के लिए औपचारिक तरीकों का उपयोग इस आशा से प्रेरित है कि, अन्य इंजीनियरिंग विषयों की तरह, उपयुक्त गणितीय विश्लेषण करने से डिजाइन की विश्वसनीयता और दृढ़ता में योगदान हो सकता है<ref>{{cite journal| first=C. Michael | last=Holloway | title=Why Engineers Should Consider Formal Methods|url=http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf|publisher=16th Digital Avionics Systems Conference (27–30 October 1997)|access-date=2006-11-16|url-status=dead|archive-url=https://web.archive.org/web/20061116210448/http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf|archive-date=16 November 2006}}</ref>।
[[ कंप्यूटर विज्ञान | कंप्यूटर विज्ञान]] में, [[ सॉफ़्टवेयर |सॉफ़्टवेयर]] और [[ संगणक धातु सामग्री |कंप्यूटर धातु सामग्री,]] हार्डवेयर सिस्टम की विशिष्टता, विकास के [[ औपचारिक सत्यापन |औपचारिक सत्यापन]] के लिए गणित की कठोर तकनीकें हैं।<ref name="butler">{{cite web| first=R. W. | last=Butler | title=What is Formal Methods? | url=http://shemesh.larc.nasa.gov/fm/fm-what.html|date=2001-08-06|access-date=2006-11-16}}</ref> सॉफ्टवेयर और हार्डवेयर बनावट के लिए औपचारिक तरीकों का उपयोग इस उम्मीद से प्रेरित है कि,अन्य अभियांत्रिकी विषयों की तरह, उपयुक्त गणितीय विश्लेषण करने से बनावट की विश्वसनीयता और मजबूती में योगदान हो सकता है।<ref>{{cite journal| first=C. Michael | last=Holloway | title=Why Engineers Should Consider Formal Methods|url=http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf|publisher=16th Digital Avionics Systems Conference (27–30 October 1997)|access-date=2006-11-16|url-status=dead|archive-url=https://web.archive.org/web/20061116210448/http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf|archive-date=16 November 2006}}</ref>
औपचारिक विधियों में कंप्यूटर विज्ञान की गणना,विभिन्न प्रकार के [[ सैद्धांतिक कंप्यूटर विज्ञान |सैद्धांतिक कंप्यूटर विज्ञान]] के मूल सिद्धांतों को नियोजित करती हैं, जिनमें [[ औपचारिक भाषा |औपचारिक भाषा,]] [[ ऑटोमेटा सिद्धांत |ऑटोमेटा सिद्धांत]],[[ नियंत्रण सिद्धांत |  निमशीनण सिद्धांत]] ,[[ कार्यक्रम शब्दार्थ ]], प्रकार सिस्टम और[[ प्रकार सिद्धांत | प्रकार सिद्धांत]] में तर्क सहित विभिन्न बुनियादी बातों का उपयोग किया जाता है।<ref>Monin, pp.3-4</ref>
   
 


औपचारिक विधियाँ विभिन्न प्रकार के [[ सैद्धांतिक कंप्यूटर विज्ञान |सैद्धांतिक कंप्यूटर विज्ञा]] के बुनियादी सिद्धांतों को नियोजित करती हैं, जिनमें तर्क गणना, [[ औपचारिक भाषा |औपचारिक भाषा,]] [[ ऑटोमेटा सिद्धांत |ऑटोमेटा सिद्धांत]],[[ नियंत्रण सिद्धांत | नियंत्रण सिद्धांत]],[[ कार्यक्रम शब्दार्थ | कार्यक्रम शब्दार्थ]], प्रकार प्रणाली और [[ प्रकार सिद्धांत |प्रकार सिद्धांत]] सम्मिलित हैं।<ref>Monin, pp.3-4</ref>
==पृष्ठभूमि==
==पृष्ठभूमि==
अर्ध-औपचारिक तरीके, औपचारिकता और भाषाएं हैं जिन्हें पूरी तरह से "औपचारिक" नहीं माना जाता है। यह शब्दार्थ को बाद के चरण में पूरा करने के कार्य को स्थगित करता है, जो बाद में या तो मानव व्याख्या द्वारा या संकेत-लिपि (कोड) या टेस्ट केस जनरेटर जैसे सॉफ़्टवेयर के माध्यम से व्याख्या द्वारा किया जाता है।<ref>{{Cite book|title=X2R-2, deliverable D5.1}}</ref>
'''अर्ध-औपचारिक तरीके''' औपचारिकता और भाषाएं हैं जिन्हें पूरी तरह से "'''औपचारिक'''" नहीं माना जाता है। यह शब्दार्थ को बाद के चरण में पूरा करने के कार्य को स्थगित करता है, जो तब या तो मानव व्याख्या द्वारा या कोड या टेस्ट केस जनरेटर जैसे सॉफ़्टवेयर के माध्यम से व्याख्या द्वारा किया जाता है।<ref>{{Cite book|title=X2R-2, deliverable D5.1}}</ref>
 
 
 
==वर्गीकरण==
==वर्गीकरण==
{{unreferenced|section|date=April 2022}}
औपचारिक तरीकों का प्रयोग कई स्तरों पर किया जा सकता है:   
औपचारिक तरीकों का इस्तेमाल कई स्तरों पर किया जा सकता है:   


स्तर 0: औपचारिक विनिर्देश शुरू करके और फिर अनौपचारिक रूप से इससे एक कार्यक्रम विकसित किया जा सकता है। इसे 'औपचारिक तरीके लाइट' करार दिया गया है। यह कई मामलों में सबसे कम लागत विकल्प हो सकता है।  
'''स्तर 0:''' [[औपचारिक विनिर्देश]] शुरू करके और फिर अनौपचारिक रूप से इससे एक कार्यक्रम विकसित किया जा सकता है। इसे "'''औपचारिक विधि'''" कहा जाता है। यह कई मामलों में सबसे कम लागत विकल्प हो सकता है।  


स्तर 1: [[ औपचारिक विकास |औपचारिक विकास]] और औपचारिक सत्यापन का उपयोग किसी कार्यक्रम को अधिक औपचारिक तरीके से तैयार करने के लिए किया जा सकता है। उदाहरण के लिए, किसी कार्यक्रम के औपचारिक विनिर्देश से गुणों या कार्यक्रम के शोधन के प्रमाण किए जा सकते हैं। यह[[ सुरक्षा | सुरक्षा]] से जुड़े उच्च-अखंडता प्रणालियों में सबसे उपयुक्त हो सकता है।     
'''स्तर 1:''' [[ औपचारिक विकास |औपचारिक विकास]] और औपचारिक पद्यतियां का उपयोग किसी कार्यक्रम को अधिक औपचारिक विधि से तैयार करने के लिए किया जा सकता है। '''उदाहरण के लिए''', किसी कार्यक्रम के औपचारिक विनिर्देश से गुणों या कार्यक्रम के शोधन के प्रमाण किए जा सकते हैं। यह[[ सुरक्षा | सुरक्षा]] से जुड़े उच्च-अखंडता प्रणालियों में सबसे उपयुक्त हो सकता है।     


स्तर 2:  प्रमेय प्रोवर्स का उपयोग पूरी तरह से औपचारिक मशीन-चेक किए गए प्रमाणों को करने के लिए किया जा सकता है। यदि गलतियों की लागत बहुत अधिक है तो उपकरणों में सुधार और घटती लागत के बावजूद, यह बहुत महंगा हो सकता है जो की केवल व्यावहारिक रूप से सार्थक है (उदाहरण के लिए, क्रिया संचालन (ऑपरेटिंग) सिस्टम या माइक्रोसंसाधक बनावट के महत्वपूर्ण भागों में)।   
'''स्तर 2:''' प्रमेय प्रोवर्स का उपयोग पूरी तरह से औपचारिक मशीन-चेक किए गए प्रमाणों को करने के लिए किया जा सकता है। यदि त्रुटियों का मान बहुत अधिक है तो उपकरण सुधार और घटती लागत के बजाय, यह बहुत महंगा हो सकता है और केवल व्यावहारिक रूप से सार्थक है (उदाहरण के लिए, क्रिया संचालन (ऑपरेटिंग) सिस्टम या माइक्रोसंसाधक बनावट के महत्वपूर्ण भागों में है)।   


इसके बारे में अधिक जानकारी नीचे दी गई है।
इसके बारे में अधिक जानकारी नीचे दी गई है।
Line 24: Line 17:
[[ प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ | प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ]] के साथ,औपचारिक विधियों की शैलियों को मोटे तौर पर निम्नानुसार वर्गीकृत किया जा सकता है:  
[[ प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ | प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ]] के साथ,औपचारिक विधियों की शैलियों को मोटे तौर पर निम्नानुसार वर्गीकृत किया जा सकता है:  


* [[ सांकेतिक शब्दार्थ | सांकेतिक शब्दार्थ,]] जिसमें एक सिस्टम का अर्थ [[ डोमेन सिद्धांत |डोमेन सिद्धांत]] के गणितीय सिद्धांत में व्यक्त किया जाता है। इस तरह के तरीकों के समर्थक सिस्टम को अर्थ देने के लिए डोमेन की अच्छी तरह से समझी गई प्रकृति पर भरोसा करते हैं; आलोचकों का कहना है कि हर सिस्टम को सहज या स्वाभाविक रूप से एक कार्य के रूप में नहीं देखा जा सकता है। ऐसी विधियों के समर्थक सिस्टम को अर्थ देने के लिए डोमेन को अच्छी तरह से समझ कर ही उसकी प्रकृति पर भरोसा करते हैं;
* [[ सांकेतिक शब्दार्थ | सांकेतिक शब्दार्थ,]] जिसमें एक सिस्टम का अर्थ [[ डोमेन सिद्धांत |क्षेत्र (डोमेन) सिद्धांत]] के गणितीय सिद्धांत में व्यक्त किया जाता है। इस तरह के तरीकों के समर्थक सिस्टम को अर्थ देने के लिए क्षेत्र की अच्छी तरह से समझी गई प्रकृति पर भरोसा करते हैं; आलोचकों का कहना है कि हर सिस्टम को सहज या स्वाभाविक रूप से एक कार्य के रूप में नहीं देखा जा सकता है।
*[[ परिचालन शब्दार्थ |परिचालन शब्दार्थ]] , जिसमें एक सिस्टम का अर्थ एक (संभवतः) सरल अभिकलन प्रतिमान (कम्प्यूटेशनल मॉडल) की क्रियाओं के अनुक्रम के रूप में व्यक्त किया जाता है। इस तरह के तरीकों के समर्थक अपने प्रतिमान की सादगी को अभिव्यक्तिपूर्ण स्पष्टता के साधन के रूप में इंगित करते हैं; आलोचकों का कहना है कि शब्दार्थ की समस्या में अभी देरी हुई है (जो सरल प्रतिमान के शब्दार्थ को परिभाषित करता है?)   इस तरह के तरीकों के समर्थक अपने प्रतिमान की सादगी को अभिव्यक्तिपूर्ण स्पष्टता के साधन के रूप में इंगित करते हैं;
*[[ परिचालन शब्दार्थ |परिचालन शब्दार्थ]] , जिसमें एक सिस्टम का अर्थ एक (संभवतः) सरल अभिकलन मॉडल (कम्प्यूटेशनल मॉडल) की क्रियाओं के अनुक्रम के रूप में व्यक्त किया जाता है। इस तरह के तरीकों के समर्थक अपने मॉडल की सादगी को अभिव्यक्तिपूर्ण स्पष्टता के साधन के रूप में इंगित करते हैं; आलोचकों का कहना है कि शब्दार्थ की समस्या में अभी देरी हुई है (जो सरल मॉडल के शब्दार्थ को परिभाषित करता है)
* [[ स्वयंसिद्ध शब्दार्थ ]], जिसमें सिस्टम का अर्थ पूर्व शर्त और [[ शर्त के बाद |शर्त के बाद]] के संदर्भ में व्यक्त किया जाता है जो कि सिस्टम द्वारा किसी कार्य को करने से पहले और बाद में एक कार्य करता है। समर्थकों ने प्राचीन [[ तर्क |तर्क]] के संबंध पर ध्यान दिया; आलोचकों ने ध्यान दिया कि इस तरह के शब्दार्थ वास्तव में कभी भी यह वर्णन नहीं करते हैं कि एक सिस्टम ''क्या करती है''। (केवल वही जो पहले और बाद में सच है)
* [[ स्वयंसिद्ध शब्दार्थ ]], जिसमें सिस्टम का अर्थ पूर्व शर्त और [[ शर्त के बाद |शर्त के बाद]] के संदर्भ में व्यक्त किया जाता है जो कि सिस्टम द्वारा किसी कार्य को करने से पहले और बाद में एक कार्य करता है। समर्थकों ने प्राचीन [[ तर्क |तर्क]] के संबंध पर ध्यान दिया; आलोचकों ने ध्यान दिया कि इस तरह के शब्दार्थ वास्तव में कभी भी यह वर्णन नहीं करते हैं कि एक सिस्टम क्या करती है। (केवल वही जो पहले और बाद में सच है)


=== हल्के औपचारिक तरीके ===
=== सरल औपचारिक तरीके ===
कुछ चिकित्सकों का मानना ​​​​है कि औपचारिक तरीके समुदाय ने एक विनिर्देश या बनावट की पूर्ण औपचारिकता पर अधिक जोर दिया है।<ref>[[Daniel Jackson (computer scientist)|Daniel Jackson]] and [[Jeannette Wing]], [http://people.csail.mit.edu/dnj/publications/ieee96-roundtable.html "Lightweight Formal Methods"], ''IEEE Computer'', April 1996</ref><ref>Vinu George and Rayford Vaughn, [http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html "Application of Lightweight Formal Methods in Requirement Engineering"] {{webarchive|url=https://web.archive.org/web/20060301022259/http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html |date=2006-03-01 }}, ''Crosstalk: The Journal of Defense Software Engineering'', January 2003</ref> उनका तर्क है कि इसमें शामिल भाषाओं की अभिव्यंजना, साथ ही प्रतिरूपित की जा रही प्रणालियों की जटिलता, पूर्ण औपचारिकता को एक कठिन और महंगा कार्य बनाती है। एक विकल्प के रूप में, विभिन्न हल्के औपचारिक तरीके, जो आंशिक विनिर्देश और केंद्रित अनुप्रयोग पर जोर देते हैं, एक विकल्प के रूप में, प्रस्तावित किए गए हैं। औपचारिक तरीकों के लिए इस हल्के दृष्टिकोण के उदाहरणों में [[ मिश्र धातु भाषा ]](वस्तु प्रतिरूपण संकेतन) वस्तु  मॉडलिंग नोटेशन शामिल है,<ref>Daniel Jackson, [http://people.csail.mit.edu/dnj/publications/alloy-journal.pdf "Alloy: A Lightweight Object Modelling Notation"], ''ACM Transactions on Software Engineering and Methodology (TOSEM)'', Volume 11, Issue 2 (April 2002), pp. 256-290</ref>  Z संकेतन के कुछ पहलुओं का डेनी का संश्लेषण,<ref>Richard Denney, ''Succeeding with Use Cases: Working Smart to Deliver Quality'', Addison-Wesley Professional Publishing, 2005, {{ISBN|0-321-31643-6}}.</ref> उपयोग केस संचालित विकास, और सीएसके [[ वियना विकास विधि |वियना विकास विधि]] उपकरण्स।<ref>Sten Agerholm and Peter G. Larsen, [http://home0.inet.tele.dk/pgl/fmtrends98.pdf "A Lightweight Approach to Formal Methods"] {{webarchive|url=https://web.archive.org/web/20060309041943/http://home0.inet.tele.dk/pgl/fmtrends98.pdf |date=2006-03-09 }}, In ''Proceedings of the International Workshop on Current Trends in Applied Formal Methods'', Boppard, Germany, Springer-Verlag, October 1998</ref>
कुछ चिकित्सकों का मानना ​​​​है कि औपचारिक तरीके समुदाय ने एक विनिर्देश या बनावट की पूर्ण औपचारिकता पर अधिक जोर दिया है।<ref>[[Daniel Jackson (computer scientist)|Daniel Jackson]] and [[Jeannette Wing]], [http://people.csail.mit.edu/dnj/publications/ieee96-roundtable.html "Lightweight Formal Methods"], ''IEEE Computer'', April 1996</ref><ref>Vinu George and Rayford Vaughn, [http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html "Application of Lightweight Formal Methods in Requirement Engineering"] {{webarchive|url=https://web.archive.org/web/20060301022259/http://www.stsc.hill.af.mil/crosstalk/2003/01/George.html |date=2006-03-01 }}, ''Crosstalk: The Journal of Defense Software Engineering'', January 2003</ref> उनका तर्क है कि इसमें सम्मिलित भाषाओं की अभिव्यंजना, साथ ही प्रतिरूपित की जा रही प्रणालियों की जटिलता, पूर्ण औपचारिकता को एक कठिन और महंगा कार्य बनाती है। एक विकल्प के रूप में, विभिन्न हल्के औपचारिक तरीके, जो आंशिक विनिर्देश और केंद्रित अनुप्रयोग पर जोर देते हैं, एक विकल्प के रूप में, प्रस्तावित किए गए हैं। औपचारिक तरीकों के लिए इस हल्के दृष्टिकोण के उदाहरणों में [[ मिश्र धातु भाषा |मिश्र धातु भाषा]] (वस्तु प्रतिरूपण संकेतन) वस्तु  मॉडलिंग नोटेशन सम्मिलित है,<ref>Daniel Jackson, [http://people.csail.mit.edu/dnj/publications/alloy-journal.pdf "Alloy: A Lightweight Object Modelling Notation"], ''ACM Transactions on Software Engineering and Methodology (TOSEM)'', Volume 11, Issue 2 (April 2002), pp. 256-290</ref>  Z संकेतन के कुछ पहलुओं का डेनी का संश्लेषण,<ref>Richard Denney, ''Succeeding with Use Cases: Working Smart to Deliver Quality'', Addison-Wesley Professional Publishing, 2005, {{ISBN|0-321-31643-6}}.</ref> उपयोग केस संचालित विकास, और CSK (सीएसके) [[ वियना विकास विधि |VDM (वियना विकास विधि)]] उपकरण् है।<ref>Sten Agerholm and Peter G. Larsen, [http://home0.inet.tele.dk/pgl/fmtrends98.pdf "A Lightweight Approach to Formal Methods"] {{webarchive|url=https://web.archive.org/web/20060309041943/http://home0.inet.tele.dk/pgl/fmtrends98.pdf |date=2006-03-09 }}, In ''Proceedings of the International Workshop on Current Trends in Applied Formal Methods'', Boppard, Germany, Springer-Verlag, October 1998</ref>


== '''उपयोग''' ==
== '''उपयोग''' ==
Line 37: Line 30:
विकसित की जाने वाली सिस्टम का विवरण देने के लिए, चाहे किसी भी स्तर पर विवरण वांछित हो,औपचारिक तरीकों का इस्तेमाल किया जा सकता है। इस औपचारिक विवरण का उपयोग आगे की विकास गतिविधियों को निर्देशित करने के लिए किया जा सकता है (निम्नलिखित अनुभाग देखें); इसके अतिरिक्त, इसका उपयोग यह सत्यापित करने के लिए किया जा सकता है कि विकसित की जा रही सिस्टम की आवश्यकताओं को पूरी तरह और सटीक रूप से निर्दिष्ट किया गया है, या औपचारिक भाषा में उन्हें एक सटीक और स्पष्ट रूप से परिभाषित वाक्यविन्यास और शब्दार्थ के साथ औपचारिक भाषा में व्यक्त करके औपचारिक रूप दिया गया है।   
विकसित की जाने वाली सिस्टम का विवरण देने के लिए, चाहे किसी भी स्तर पर विवरण वांछित हो,औपचारिक तरीकों का इस्तेमाल किया जा सकता है। इस औपचारिक विवरण का उपयोग आगे की विकास गतिविधियों को निर्देशित करने के लिए किया जा सकता है (निम्नलिखित अनुभाग देखें); इसके अतिरिक्त, इसका उपयोग यह सत्यापित करने के लिए किया जा सकता है कि विकसित की जा रही सिस्टम की आवश्यकताओं को पूरी तरह और सटीक रूप से निर्दिष्ट किया गया है, या औपचारिक भाषा में उन्हें एक सटीक और स्पष्ट रूप से परिभाषित वाक्यविन्यास और शब्दार्थ के साथ औपचारिक भाषा में व्यक्त करके औपचारिक रूप दिया गया है।   


औपचारिक विनिर्देश प्रणालियों की आवश्यकता को वर्षों से नोट किया गया है। [[ ALGOL 58 |ALGOL 58]] आख्या (रिपोर्ट) में,<ref>{{cite conference | first = J.W. | last = Backus | title = The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference | book-title = Proceedings of the International Conference on Information Processing | publisher = UNESCO | year = 1959 }}</ref> [[ जॉन बैकस |जॉन बैकस]] ने प्रोग्रामिंग भाषा वाक्यविन्यास, का वर्णन करने के लिए एक औपचारिक संकेतन प्रस्तुत किया, जिसे बाद में [[ बैकस सामान्य रूप ]] नाम दिया गया और फिर इसका नाम बदलकर बैकस-नौर फॉर्म (बीएनएफ) कर दिया गया।<ref>[[Donald Knuth|Knuth, Donald E.]] (1964), Backus Normal Form vs Backus Naur Form. ''[[Communications of the ACM]]'', 7(12):735–736.</ref> बैकस ने यह भी लिखा है कि वाक्यात्मक रूप से मान्य ALGOL कार्यक्रमों के अर्थ का औपचारिक विवरण आख्या में शामिल करने के लिए समय पर पूरा नहीं किया गया था।" इसलिए कानूनी कार्यक्रमों के शब्दार्थ का औपचारिक उपचार बाद के पेपर में शामिल किया जाएगा।" यह कभी नहीं दिखाई दिया।   
औपचारिक विनिर्देश प्रणालियों की आवश्यकता को वर्षों से नोट किया गया है। [[ ALGOL 58 |ALGOL 58]] आख्या (रिपोर्ट) में,<ref>{{cite conference | first = J.W. | last = Backus | title = The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference | book-title = Proceedings of the International Conference on Information Processing | publisher = UNESCO | year = 1959 }}</ref> [[ जॉन बैकस |जॉन बैकस]] ने प्रोग्रामिंग भाषा वाक्यविन्यास, का वर्णन करने के लिए एक औपचारिक संकेतन प्रस्तुत किया, जिसे बाद में [[ बैकस सामान्य रूप |बैकस सामान्य रूप]] नाम दिया गया और फिर इसका नाम बदलकर बैकस-नौर फॉर्म (बीएनएफ) कर दिया गया।<ref>[[Donald Knuth|Knuth, Donald E.]] (1964), Backus Normal Form vs Backus Naur Form. ''[[Communications of the ACM]]'', 7(12):735–736.</ref> बैकस ने यह भी लिखा है कि वाक्यात्मक रूप से मान्य ALGOL कार्यक्रमों के अर्थ का औपचारिक विवरण आख्या में सम्मिलित करने के लिए समय पर पूरा नहीं किया गया था।" इसलिए कानूनी कार्यक्रमों के शब्दार्थ का औपचारिक उपचार बाद के पेपर में सम्मिलित किया जाएगा।" यह कभी नहीं दिखाई दिया।   


===विकास ===
===विकास ===
Line 45: Line 38:


* यदि औपचारिक विनिर्देश परिचालन शब्दार्थ में है, तो ठोस सिस्टम के देखे गए व्यवहार की तुलना विनिर्देश के व्यवहार से की जा सकती है (जो स्वयं निष्पादन योग्य या अनुकरणीय होना चाहिए)। इसके अतिरिक्त, विनिर्देशन के परिचालन आदेश निष्पादन योग्य संकेत-लिपि में अनुवाद को निर्देशित करने के लिए उपयुक्त हो सकते हैं।
* यदि औपचारिक विनिर्देश परिचालन शब्दार्थ में है, तो ठोस सिस्टम के देखे गए व्यवहार की तुलना विनिर्देश के व्यवहार से की जा सकती है (जो स्वयं निष्पादन योग्य या अनुकरणीय होना चाहिए)। इसके अतिरिक्त, विनिर्देशन के परिचालन आदेश निष्पादन योग्य संकेत-लिपि में अनुवाद को निर्देशित करने के लिए उपयुक्त हो सकते हैं।
* यदि औपचारिक विनिर्देश स्वयंसिद्ध शब्दार्थ में है, तो विनिर्देश की पूर्व शर्त और बाद की शर्तें निष्पादन योग्य संकेत-लिपि में [[ अभिकथन (कंप्यूटिंग) |अभिकथन (कंप्यूटिंग)]] बन सकती हैं।  
* यदि औपचारिक विनिर्देश स्वयंसिद्ध शब्दार्थ में है, तो विनिर्देश की पूर्व शर्त और बाद की शर्तें निष्पादन योग्य संकेत-लिपि में [[ अभिकथन (कंप्यूटिंग) |अभिकथन (कंप्यूटिंग)]] बन सकती हैं।


=== सत्यापन ===
=== पद्यतियां ===


औपचारिक सत्यापन एक औपचारिक विनिर्देश के गुणों को साबित करने के लिए सॉफ़्टवेयर उपकरण (टूल) का उपयोग है, या यह साबित करने के लिए कि सिस्टम कार्यान्वयन का एक औपचारिक  प्रतिमान इसके विनिर्देश को पूरा करता है।  
औपचारिक पद्यतियां एक औपचारिक विनिर्देश के गुणों को साबित करने के लिए सॉफ़्टवेयर उपकरण (टूल) का उपयोग है, या यह साबित करने के लिए कि सिस्टम कार्यान्वयन का एक औपचारिक  मॉडल इस के विनिर्देश को पूरा करता है।  


एक बार औपचारिक विनिर्देश विकसित हो जाने के बाद, विनिर्देश का उपयोग विनिर्देश के[[ गणितीय प्रमाण ]]गुणों के आधार के रूप में, अनुमान से, सिस्टम कार्यान्वयन के गुण के रूप में किया जा सकता है।
एक बार औपचारिक विनिर्देश विकसित हो जाने के बाद, विनिर्देश का उपयोग विनिर्देश के[[ गणितीय प्रमाण ]]गुणों के आधार के रूप में, अनुमान से, सिस्टम कार्यान्वयन के गुण के रूप में किया जा सकता है।  


==== साइन-ऑफ सत्यापन ====
==== साइन-ऑफ पद्यतियां ====
साइन-ऑफ सत्यापन एक औपचारिक सत्यापन उपकरण का उपयोग है जो अत्यधिक विश्वसनीय है। ऐसा उपकरण पारंपरिक सत्यापन विधियों को प्रतिस्थापित कर सकता है (उपकरण प्रमाणित भी हो सकता है)।   
साइन-ऑफ पद्यतियां एक औपचारिक पद्यतियां उपकरण का उपयोग है जो अत्यधिक विश्वसनीय है। ऐसा उपकरण पारंपरिक पद्यतियां विधियों को प्रतिस्थापित कर सकता है (उपकरण प्रमाणित भी हो सकता है)।   


==== मानव निर्देशित सबूत ====
==== मानव निर्देशित सबूत ====
कभी-कभी, सिस्टम की [[ शुद्धता (कंप्यूटर विज्ञान) |शुद्धता (कंप्यूटर विज्ञान)]] को साबित करने के लिए, सिस्टम की शुद्धता को साबित करने की स्पष्ट आवश्यकता नहीं है, बल्कि सिस्टम को बेहतर ढंग से समझने की इच्छा है। नतीजतन, गणितीय प्रमाण की शैली में शुद्धता के कुछ प्रमाण तैयार किए जाते हैं: ऐसे प्रमाणों के लिए सामान्य अनौपचारिकता के स्तर का उपयोग करते हुए, [[ प्राकृतिक भाषा |प्राकृतिक भाषा]] का उपयोग करते हुए हस्तलिखित (या टाइपसेट), एक अच्छा प्रमाण वह है जो अन्य मानव पाठकों द्वारा पठनीय और समझने योग्य हो।   
कभी-कभी, सिस्टम की [[ शुद्धता (कंप्यूटर विज्ञान) |शुद्धता (कंप्यूटर विज्ञान)]] को साबित करने के लिए, सिस्टम की शुद्धता को साबित करने की स्पष्ट आवश्यकता नहीं है, बल्कि सिस्टम को बेहतर ढंग से समझने की इच्छा है। नतीजतन, गणितीय प्रमाण की शैली में शुद्धता के कुछ प्रमाण तैयार किए जाते हैं: ऐसे प्रमाणों के लिए सामान्य अनौपचारिकता के स्तर का उपयोग करते हुए, [[ प्राकृतिक भाषा |प्राकृतिक भाषा]] का उपयोग, हस्तलिखित (या टाइपसेट), एक अच्छा प्रमाण वह है जो अन्य मानव पाठकों द्वारा पठनीय और समझने योग्य हो।   


इस तरह के दृष्टिकोण के आलोचक बताते हैं कि प्राकृतिक भाषा में निहित अस्पष्टता ऐसे प्रमाणों में त्रुटियों का पता लगाने की अनुमति नहीं देती है; अक्सर, सूक्ष्म त्रुटियाँ निम्न-स्तरीय विवरणों में मौजूद हो सकती हैं जिन्हें आमतौर पर ऐसे प्रमाणों द्वारा अनदेखा किया जाता है। इसके अतिरिक्त, इस तरह के एक अच्छे प्रमाण के निर्माण में शामिल कार्य के लिए उच्च स्तर के गणितीय परिष्कार और विशेषज्ञता की आवश्यकता होती है।   
इस तरह के दृष्टिकोण के आलोचक बताते हैं कि प्राकृतिक भाषा में निहित अस्पष्टता ऐसे प्रमाणों में त्रुटियों का पता लगाने की अनुमति नहीं देती है; अक्सर, सूक्ष्म त्रुटियाँ निम्न-स्तरीय विवरणों में मौजूद हो सकती हैं जिन्हें आमतौर पर ऐसे प्रमाणों द्वारा अनदेखा किया जाता है। इसके अतिरिक्त, इस तरह के एक अच्छे प्रमाण के निर्माण में सम्मिलित कार्य के लिए उच्च स्तर के गणितीय परिष्कार और विशेषज्ञता की आवश्यकता होती है।   


==== स्वचालित प्रमाण ====
==== स्वचालित प्रमाण ====
इसके विपरीत, स्वचालित साधनों द्वारा ऐसी प्रणालियों की शुद्धता के प्रमाण प्रस्तुत करने में रुचि बढ़ रही है। स्वचालित तकनीक तीन सामान्य श्रेणियों में आती है:   
इसके विपरीत, स्वचालित साधनों द्वारा ऐसी प्रणालियों की शुद्धता के प्रमाण प्रस्तुत करने में रुचि बढ़ रही है। स्वचालित तकनीक तीन सामान्य श्रेणियों में आती है:   
* [[ स्वचालित प्रमेय सिद्ध करना |स्वचालित प्रमेय सिद्ध करना]], जिसमें एक सिस्टम खरोंच से एक औपचारिक प्रमाण का उत्पादन करने का प्रयास करती है, सिस्टम का विवरण दिया जाता है, तार्किक स्वयंसिद्धों का एक समूह             (सेट) और अनुमान नियमों का एक समूह दिया जाता है।
* [[ स्वचालित प्रमेय सिद्ध करना |स्वचालित प्रमेय सिद्ध करना]], जिसमें एक सिस्टम खरोंच से एक औपचारिक प्रमाण का उत्पादन करने का प्रयास करती है, सिस्टम का विवरण दिया जाता है, तार्किक स्वयंसिद्धों का एक समूह (सेट) और अनुमान नियमों का एक समूह दिया जाता है।
* प्रतिमानजांच, जिसमें एक सिस्टम सभी संभावित स्तरों की विस्तृत खोज के माध्यम से कुछ गुणों का सत्यापन करता है जो एक सिस्टम अपने निष्पादन के दौरान दर्ज कर सकता है।
* मॉडल जांच, जिसमें एक सिस्टम सभी संभावित स्तरों की विस्तृत खोज के माध्यम से कुछ गुणों का पद्यतियां करता है जो एक सिस्टम अपने निष्पादन के दौरान दर्ज कर सकता है।
* [[ सार व्याख्या |सार व्याख्या]] , जिसमें एक सिस्टम कार्यक्रम की एक व्यवहारिक लक्षण के अति-सन्निकटन की पुष्टि करती है, इसका प्रतिनिधित्व करने वाले (संभवतः पूर्ण) जालक पर एक फिक्सपॉइंट गणना का उपयोग करके।
* [[ सार व्याख्या |सार व्याख्या]] , जिसमें एक सिस्टम कार्यक्रम की एक व्यवहारिक लक्षण के अति-सन्निकटन की पुष्टि करती है, इसका प्रतिनिधित्व करने वाले (संभवतः पूर्ण) जालक पर एक फिक्सपॉइंट गणना का उपयोग करके।


कुछ स्वचालित प्रमेय प्रोवर्स को मार्गदर्शन की आवश्यकता होती है कि कौन से गुण काफी रोचक हैं जो आगे बढ़ने के लिए पर्याप्त हैं, जबकि अन्य मानवीय हस्तक्षेप के बिना काम करते हैं। यदि पर्याप्त रूप से सार प्रतिमान (मॉडल) नहीं दिया जाता है, तो प्रतिमान चेकर्स (जाँच) लाखों अरोचक स्तरों की जाँच में जल्दी से फंस सकते हैं।   
कुछ स्वचालित प्रमेय प्रोवर्स को मार्गदर्शन की आवश्यकता होती है कि कौन से गुण काफी रोचक हैं जो आगे बढ़ने के लिए पर्याप्त हैं, जबकि अन्य मानवीय हस्तक्षेप के बिना काम करते हैं। यदि पर्याप्त रूप से सार मॉडल नहीं दिया जाता है, तो मॉडल चेकर्स (जाँच) लाखों अरोचक स्तरों की जाँच में जल्दी से फंस सकते हैं।   


ऐसी प्रणालियों के समर्थकों का तर्क है कि परिणामों में मानव-निर्मित प्रमाणों की तुलना में अधिक गणितीय निश्चितता है, क्योंकि सभी अरोचक विवरणों को एल्गोरिथम रूप से सत्यापित किया गया है। ऐसी प्रणालियों का उपयोग करने के लिए आवश्यक प्रशिक्षण भी हाथ से अच्छे गणितीय प्रमाण तैयार करने के लिए आवश्यक प्रशिक्षण से कम है, जिससे तकनीक बहुत से चिकित्सकों के लिए आसान  हो जाती है।   
ऐसी प्रणालियों के समर्थकों का तर्क है कि परिणामों में, मानव-निर्मित प्रमाणों की तुलना में अधिक गणितीय निश्चितता है, क्योंकि सभी अरोचक विवरणों को एल्गोरिथम रूप से सत्यापित किया गया है। ऐसी प्रणालियों का उपयोग करने के लिए आवश्यक प्रशिक्षण भी हाथ से अच्छे गणितीय प्रमाण तैयार करने के लिए आवश्यक प्रशिक्षण से कम है, जिससे तकनीक बहुत से चिकित्सकों के लिए आसान  हो जाती है।   


आलोचक ध्यान दें कि उनमें से कुछ प्रणालियाँ आकाशवाणी (ओरेकल) मशीनों की तरह हैं: वे सत्य का उच्चारण करती हैं, फिर भी उस सत्य का कोई स्पष्टीकरण नहीं देती हैं। ऐसी सिस्टम में "सत्यापनकर्ता के सत्यापन" की समस्या भी है ; यदि सत्यापन में सहायता करने वाला कार्यक्रम स्वयं अप्रमाणित है, तो उत्पादित परिणामों की सुदृढ़ता पर संदेह करने का कारण हो सकता है। कुछ आधुनिक[[ मॉडल जाँच | प्रतिमान जाँच]] उपकरण अपने प्रमाण में प्रत्येक चरण का विवरण देते हुए एक "प्रमाण लॉग" उत्पन्न करते हैं, जिससे स्वतंत्र सत्यापन दिए जाने ,उपयुक्त उपकरण का प्रदर्शन करना संभव हो जाता है।   
आलोचक ध्यान दें कि उनमें से कुछ प्रणालियाँ आकाशवाणी (ओरेकल) मशीनों की तरह हैं: वे सत्य का उच्चारण करती हैं, फिर भी उस सत्य का कोई स्पष्टीकरण नहीं देती हैं। ऐसी सिस्टम में "पद्यतियांकर्ता के पद्यतियां" की समस्या भी है ; यदि पद्यतियां में सहायता करने वाला कार्यक्रम स्वयं अप्रमाणित है, तो उत्पादित परिणामों की सुदृढ़ता पर संदेह करने का कारण हो सकता है। कुछ आधुनिक[[ मॉडल जाँच | मॉडल जाँच]] उपकरण अपने प्रमाण में प्रत्येक चरण का विवरण देते हुए एक "प्रमाण लॉग" उत्पन्न करते हैं, जिससे स्वतंत्र पद्यतियां दिए जाने, उपयुक्त उपकरण का प्रदर्शन करना संभव हो जाता है।   


अमूर्त व्याख्या दृष्टिकोण की मुख्य विशेषता यह है कि यह एक ध्वनि विश्लेषण प्रदान करता है, अर्थात कोई गलत नकारात्मक वापस नहीं किया जाता है। इसके अलावा, यह विश्लेषण की जाने वाली संपत्ति का प्रतिनिधित्व करने वाले अमूर्त डोमेन को ट्यून करके, और तेजी से अभिसरण प्राप्त करने के लिए व्यापक ऑपरेटरों को लागू करके, कुशलतापूर्वक विस्तार योग्य है।<ref>A. Cortesi and M. Zanioli, [http://www.dsi.unive.it/~cortesi/paperi/CL_2011.pdf Widening and Narrowing Operators for Abstract Interpretation]. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, {{ISSN|1477-8424}} (2011).</ref>
अमूर्त व्याख्या दृष्टिकोण की मुख्य विशेषता यह है कि यह एक ध्वनि विश्लेषण प्रदान करता है, अर्थात कोई गलत नकारात्मक वापस नहीं किया जाता है। इसके अलावा, यह विश्लेषण की जाने वाली संपत्ति का प्रतिनिधित्व करने वाले अमूर्त क्षेत्र को ट्यून करके, और तेजी से अभिसरण प्राप्त करने के लिए व्यापक ऑपरेटरों को लागू करके।<ref>A. Cortesi and M. Zanioli, [http://www.dsi.unive.it/~cortesi/paperi/CL_2011.pdf Widening and Narrowing Operators for Abstract Interpretation]. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, {{ISSN|1477-8424}} (2011).</ref>


== आवेदन ==
== आवेदन ==
राउटर, ईथरनेट स्विच, रूटिंग प्रोटोकॉल, सुरक्षा एप्लिकेशन और क्रिया संचालन सिस्टम माइक्रोकर्नेल जैसे [[ seL4 ]] सहित हार्डवेयर और सॉफ्टवेयर के विभिन्न क्षेत्रों में औपचारिक तरीके लागू होते हैं। ऐसे कई उदाहरण हैं जिनमें इनका उपयोग DC में प्रयुक्त हार्डवेयर और सॉफ़्टवेयर की कार्यक्षमता को सत्यापित करने के लिए किया गया है{{clarify|date=September 2015}}. [[ IBM ]] ने [[ AMD | AMD]] x86 संसाधक विकास प्रक्रिया में [[ ACL2 ]], एक प्रमेय प्रोवर का उपयोग किया।{{citation needed|date=September 2015}} इंटेल अपने हार्डवेयर और फ़र्मवेयर को सत्यापित करने के लिए ऐसे तरीकों का उपयोग करता है (स्थायी सॉफ़्टवेयर को केवल पठनीय स्मृति (रीड ऑनली मैमोरी) में प्रोग्राम किया जाता है){{citation needed|date=September 2015}}. [[ डेनिश सूचना विज्ञान केंद्र ]] ने 1980 के दशक में एडा (Ada) प्रोग्रामिंग भाषा के लिए एक कंपाइलर सिस्टम विकसित करने के लिए औपचारिक तरीकों का इस्तेमाल किया, जो एक लंबे समय तक चलने वाला व्यावसायिक उत्पाद बन गया।<ref>{{cite book | first1=Dines | last1=Bjørner | first2=Christian | last2=Gram | first3=Ole N. | last3=Oest | first4=Leif | last4=Rystrøm | chapter=Dansk Datamatik Center | editor-first= John | editor-last=Impagliazzo | editor2-first=Per | editor2-last=Lundin | editor3-first=Benkt | editor3-last=Wangler | title=History of Nordic Computing 3: IFIP Advances in Information and Communication Technology | publisher=Springer | year= 2011 | pages= 350–359 }}</ref><ref>{{cite conference | contribution=40 Years of Formal Methods: Some Obstacles and Some Possibilities? | first1=Dines | last1=Bjørner | first2=Klaus | last2=Havelund | title=FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings | publisher=Springer | pages=42–61 |url=http://www.imm.dtu.dk/~dibj/2014/tokyo/tokyo-s.pdf}}</ref>
राउटर, ईथरनेट स्विच, रूटिंग प्रोटोकॉल, सुरक्षा एप्लिकेशन और क्रिया संचालन सिस्टम माइक्रोकर्नेल जैसे [[ seL4 |seL4]] सहित हार्डवेयर और सॉफ्टवेयर के विभिन्न क्षेत्रों में औपचारिक तरीके लागू होते हैं। ऐसे कई उदाहरण हैं जिनमें इनका उपयोग DC में प्रयुक्त हार्डवेयर और सॉफ़्टवेयर की कार्यक्षमता को सत्यापित करने के लिए किया गया है. [[ IBM ]] ने [[ AMD | AMD]] x86 संसाधक विकास प्रक्रिया में [[ ACL2 ]], एक प्रमेय प्रोवर का उपयोग किया। इंटेल अपने हार्डवेयर और फ़र्मवेयर को सत्यापित करने के लिए ऐसे तरीकों का उपयोग करता है (स्थायी सॉफ़्टवेयर को केवल पठनीय स्मृति (रीड ऑनली मैमोरी) में प्रोग्राम किया जाता है) [[ डेनिश सूचना विज्ञान केंद्र |डेनिश सूचना विज्ञान केंद्र]] ने 1980 के दशक में एडा (Ada) प्रोग्रामिंग भाषा के लिए एक कंपाइलर सिस्टम विकसित करने के लिए औपचारिक तरीकों का इस्तेमाल किया, जो एक लंबे समय तक चलने वाला व्यावसायिक उत्पाद बन गया।<ref>{{cite book | first1=Dines | last1=Bjørner | first2=Christian | last2=Gram | first3=Ole N. | last3=Oest | first4=Leif | last4=Rystrøm | chapter=Dansk Datamatik Center | editor-first= John | editor-last=Impagliazzo | editor2-first=Per | editor2-last=Lundin | editor3-first=Benkt | editor3-last=Wangler | title=History of Nordic Computing 3: IFIP Advances in Information and Communication Technology | publisher=Springer | year= 2011 | pages= 350–359 }}</ref><ref>{{cite conference | contribution=40 Years of Formal Methods: Some Obstacles and Some Possibilities? | first1=Dines | last1=Bjørner | first2=Klaus | last2=Havelund | title=FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings | publisher=Springer | pages=42–61 |url=http://www.imm.dtu.dk/~dibj/2014/tokyo/tokyo-s.pdf}}</ref>[[ नासा ]]की कई अन्य परियोजनाएं हैं जिनमें औपचारिक तरीकों को लागू किया जाता है, जैसे [[ अगली पीढ़ी हवाई परिवहन प्रणाली |अगली पीढ़ी हवाई परिवहन]] सिस्टम राष्ट्रीय हवाई क्षेत्र सिस्टम में मानवरहित विमान सिस्टम का एकीकरण,<ref>Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.</ref> और एयरबोर्न को ऑर्डिनेटेड कॉन्फ्लिक्ट रेजोल्यूशन एंड डिटेक्शन (ACCoRD)।<ref>Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/</ref>[[ एटेलियर बी ]]के साथ [[ बी-विधि |बी-विधि]],<ref>{{cite web| url=http://www.atelierb.eu/en/ | title=Atelier B | website=www.atelierb.eu | lang=en }}</ref>[[ आल्सटॉम ]]और [[ सीमेंस |सीमेंस]] द्वारा दुनिया भर में स्थापित विभिन्न उपमार्ग के लिए सुरक्षा स्वचालितता विकसित करने के लिए उपयोग किया जाता है, और [[ सामान्य मानदंड |सामान्य मानदंड]] प्रमाणन और[[ एटीएमईएल | एटीएमईएल]] और [[ एसटीएमइक्रोइलेक्ट्रॉनिक्स |एसटीएमइक्रोइलेक्ट्रॉनिक्स]] द्वारा सिस्टम मॉडल के विकास के लिए भी उपयोग किया जाता है।   
[[ नासा ]] की कई अन्य परियोजनाएं हैं जिनमें औपचारिक तरीकों को लागू किया जाता है, जैसे [[ अगली पीढ़ी हवाई परिवहन प्रणाली |अगली पीढ़ी हवाई परिवहन]] सिस्टम {{citation needed|date=September 2015}}राष्ट्रीय हवाई क्षेत्र सिस्टम में मानवरहित विमान सिस्टम का एकीकरण,<ref>Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.</ref> और एयरबोर्न कोऑर्डिनेटेड कॉन्फ्लिक्ट रेजोल्यूशन एंड डिटेक्शन (ACCoRD)।<ref>Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/</ref>
[[ एटेलियर बी ]]के साथ [[ बी-विधि |बी-विधि]] ,<ref>{{cite web| url=http://www.atelierb.eu/en/ | title=Atelier B | website=www.atelierb.eu | lang=en }}</ref>[[ आल्सटॉम ]]और [[ सीमेंस |सीमेंस]] द्वारा दुनिया भर में स्थापित विभिन्न उपमार्ग के लिए सुरक्षा स्वचालितता विकसित करने के लिए उपयोग किया जाता है, और [[ सामान्य मानदंड |सामान्य मानदंड]] प्रमाणन और[[ एटीएमईएल | एटीएमईएल]] और [[ एसटीएमइक्रोइलेक्ट्रॉनिक्स |एसटीएमइक्रोइलेक्ट्रॉनिक्स]] द्वारा सिस्टम प्रतिमान के विकास के लिए भी उपयोग किया जाता है।   


अधिकांश जाने-माने हार्डवेयर विक्रेताओं, जैसे आईबीएम,[[ इंटेल | इंटेल]] और एएमडी द्वारा हार्डवेयर में औपचारिक सत्यापन अक्सर किया जाता है। हार्डवेयर के कई क्षेत्र हैं, जहां इंटेल ने उत्पादों के कामकाज को सत्यापित करने के लिए एफएम का उपयोग किया है, जैसे कैश-कोहेरेंट प्रोटोकॉल का पैरामीटरयुक्त सत्यापन,<ref>C. T. Chou, P. K. Mannava, S. Park, “[https://www.student.cs.uwaterloo.ca/~cs745/paper-pres/simparam.pdf A simple method for parameterized verification of cache coherence protocols]”, Formal Methods in Computer-Aided Design, pp. 382–398, 2004.</ref> इंटेल कोर i7 संसाधक निष्पादन इंजन सत्यापन <ref>Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371, accessed at Sep. 13, 2013.</ref> (प्रमेय सिद्ध करने,[[ द्विआधारी निर्णय आरेख | द्विआधारी निर्णय आरेख]],और प्रतीकात्मक मूल्यांकन का उपयोग करके), एचओएल प्रकाश प्रमेय प्रोवर का उपयोग करके इंटेल आईए -64 आर्किटेक्चर का इष्टतम उपयोग करके,<ref>J. Grundy, “Verified optimizations for the Intel IA-64 architecture”, In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.</ref> और ताल (केडेंस) का उपयोग करते हुए पीसीआई एक्सप्रेस प्रोटोकॉल और इंटेल अग्रिम प्रबंधन प्रौद्योगिकी के समर्थन के साथ उच्च-प्रदर्शन दोहरे पोर्ट गीगाबिट ईथरनेट निमशीनक का सत्यापन।<ref>E. Seligman, I. Yarom, “[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.108.2381&rep=rep1&type=pdf Best known methods for using Cadence Conformal LEC]”, at Intel.</ref> इसी तरह, आईबीएम ने पावर गेट्स के सत्यापन में औपचारिक तरीकों का इस्तेमाल किया है,<ref>C. Eisner, A. Nahir, K. Yorav, “[ftp://nozdr.ru/biblio/kolxo3/Cs/CsLn/Computer%20Aided%20Verification,%2020%20conf.,%20CAV%202008(LNCS5123,%20Springer,%202008)(ISBN%209783540705437)(573s)_CsLn_.pdf#page=449 Functional verification of power gated designs by compositional reasoning]”, Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.</ref> रजिस्टर,<ref>P. C. Attie, H. Chockler, “[https://core.ac.uk/download/pdf/82434920.pdf Automatic verification of fault-tolerant register emulations]”, Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.</ref> और IBM Power7 माइक्रोसंसाधक के सत्यापन<ref>K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “[https://ieeexplore.ieee.org/abstract/document/5756329/ Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems]”, IBM Journal of Research and Development, vol. 55, no 3.</ref> में औपचारिक तरीकों का इस्तेमाल किया है।  
अधिकांश जाने-माने हार्डवेयर विक्रेताओं, जैसे आईबीएम,[[ इंटेल | इंटेल]] और एएमडी द्वारा हार्डवेयर में औपचारिक पद्यतियां अक्सर किया जाता है। हार्डवेयर के कई क्षेत्र हैं, जहां इंटेल ने उत्पादों के कामकाज को सत्यापित करने के लिए एफएम का उपयोग किया है, जैसे कैश-कोहेरेंट प्रोटोकॉल का पैरामीटरयुक्त पद्यतियां,<ref>C. T. Chou, P. K. Mannava, S. Park, “[https://www.student.cs.uwaterloo.ca/~cs745/paper-pres/simparam.pdf A simple method for parameterized verification of cache coherence protocols]”, Formal Methods in Computer-Aided Design, pp. 382–398, 2004.</ref> इंटेल कोर i7 संसाधक निष्पादन इंजन पद्यतियां<ref>Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371, accessed at Sep. 13, 2013.</ref> (प्रमेय सिद्ध करने,[[ द्विआधारी निर्णय आरेख | द्विआधारी निर्णय आरेख]],और प्रतीकात्मक मूल्यांकन का उपयोग करके), एचओएल प्रकाश प्रमेय प्रोवर का उपयोग करके इंटेल आईए -64 आर्किटेक्चर का इष्टतम उपयोग करके,<ref>J. Grundy, “Verified optimizations for the Intel IA-64 architecture”, In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.</ref> और ताल (केडेंस) का उपयोग करते हुए पीसीआई एक्सप्रेस प्रोटोकॉल और इंटेल अग्रिम प्रबंधन प्रौद्योगिकी के समर्थन के साथ उच्च-प्रदर्शन दोहरे पोर्ट गीगाबिट ईथरनेट निमशीनक का पद्यतियां।<ref>E. Seligman, I. Yarom, “[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.108.2381&rep=rep1&type=pdf Best known methods for using Cadence Conformal LEC]”, at Intel.</ref> इसी तरह, आईबीएम ने पावर गेट्स के पद्यतियां में औपचारिक तरीकों का इस्तेमाल किया है,<ref>C. Eisner, A. Nahir, K. Yorav, “[ftp://nozdr.ru/biblio/kolxo3/Cs/CsLn/Computer%20Aided%20Verification,%2020%20conf.,%20CAV%202008(LNCS5123,%20Springer,%202008)(ISBN%209783540705437)(573s)_CsLn_.pdf#page=449 Functional verification of power gated designs by compositional reasoning]”, Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.</ref> रजिस्टर,<ref>P. C. Attie, H. Chockler, “[https://core.ac.uk/download/pdf/82434920.pdf Automatic verification of fault-tolerant register emulations]”, Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.</ref> और IBM Power7 माइक्रोसंसाधक के पद्यतियां<ref>K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “[https://ieeexplore.ieee.org/abstract/document/5756329/ Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems]”, IBM Journal of Research and Development, vol. 55, no 3.</ref> में औपचारिक तरीकों का इस्तेमाल किया है।  
== सॉफ्टवेयर विकास में ==
== सॉफ्टवेयर विकास में ==
सॉफ़्टवेयर विकास में, औपचारिक विधियाँ आवश्यकताओं, विनिर्देश और डिज़ाइन स्तरों पर सॉफ़्टवेयर (और हार्डवेयर) समस्याओं को हल करने के लिए गणितीय दृष्टिकोण हैं। औपचारिक तरीकों को सुरक्षा-महत्वपूर्ण या सुरक्षा-महत्वपूर्ण सॉफ़्टवेयर और प्रणाली, जैसे [[ एवियोनिक्स सॉफ्टवेयर |एवियोनिक्स सॉफ्टवेयर]] पर लागू होने की सबसे अधिक संभावना है। सॉफ़्टवेयर सुरक्षा आश्वासन मानक, जैसे [[ DO-178C ]] पूरकता के माध्यम से औपचारिक तरीकों के उपयोग की अनुमति देता है, और सामान्य मानदंड वर्गीकरण के उच्चतम स्तरों पर औपचारिक तरीकों को अनिवार्य करता है।  
सॉफ़्टवेयर विकास में, औपचारिक विधियाँ आवश्यकताओं, विनिर्देश और डिज़ाइन स्तरों पर सॉफ़्टवेयर (और हार्डवेयर) समस्याओं को हल करने के लिए गणितीय दृष्टिकोण हैं। औपचारिक तरीकों को सुरक्षा-महत्वपूर्ण या सुरक्षा-महत्वपूर्ण सॉफ़्टवेयर और प्रणाली, जैसे [[ एवियोनिक्स सॉफ्टवेयर |एवियोनिक्स सॉफ्टवेयर]] पर लागू होने की सबसे अधिक संभावना है। सॉफ़्टवेयर सुरक्षा आश्वासन मानक, जैसे [[ DO-178C ]] पूरकता के माध्यम से औपचारिक तरीकों के उपयोग की अनुमति देता है, और सामान्य मानदंड वर्गीकरण के उच्चतम स्तरों पर औपचारिक तरीकों को अनिवार्य करता है।  


अनुक्रमिक सॉफ़्टवेयर के लिए, औपचारिक तरीकों के उदाहरणों में बी-विधि, स्वचालित प्रमेय सिद्ध करने में उपयोग की जाने वाली विनिर्देश भाषाएँ, औद्योगिक सॉफ़्टवेयर अभियांत्रिकी के लिए कठोर दृष्टिकोण (RAISE) और Z संकेतन शामिल हैं।  
अनुक्रमिक सॉफ़्टवेयर के लिए, औपचारिक तरीकों के उदाहरणों में बी-विधि, स्वचालित प्रमेय सिद्ध करने में उपयोग की जाने वाली विनिर्देश भाषाएँ, औद्योगिक सॉफ़्टवेयर अभियांत्रिकी के लिए कठोर दृष्टिकोण (RAISE) और Z संकेतन सम्मिलित हैं।  


[[ कार्यात्मक प्रोग्रामिंग |कार्यात्मक प्रोग्रामिंग]] में, संपत्ति-आधारित परीक्षण ने व्यक्तिगत कार्यों के अपेक्षित व्यवहार के गणितीय विनिर्देश और [[ त्वरित जांच |त्वरित परीक्षण]] (यदि संपूर्ण परीक्षण नहीं) की अनुमति दी है।  
[[ कार्यात्मक प्रोग्रामिंग |कार्यात्मक प्रोग्रामिंग]] में, संपत्ति-आधारित परीक्षण ने व्यक्तिगत कार्यों के अपेक्षित व्यवहार के गणितीय विनिर्देश और [[ त्वरित जांच |त्वरित परीक्षण]] (यदि संपूर्ण परीक्षण नहीं) की अनुमति दी है।  
Line 90: Line 81:
यदि वस्तु -ओरिएंटेड (वस्तु उन्मुख) प्रणाली, औपचारिक रूप से सत्यापित नहीं किया गया है तो वस्तु (ऑब्जेक्ट) बाधा भाषा (और विशेषज्ञता जैसे[[ जावा मॉडलिंग भाषा | जावा मॉडलिंग भाषा]]) ने वस्तु -उन्मुख सिस्टम को औपचारिक रूप से निर्दिष्ट करने की अनुमति दी है।  
यदि वस्तु -ओरिएंटेड (वस्तु उन्मुख) प्रणाली, औपचारिक रूप से सत्यापित नहीं किया गया है तो वस्तु (ऑब्जेक्ट) बाधा भाषा (और विशेषज्ञता जैसे[[ जावा मॉडलिंग भाषा | जावा मॉडलिंग भाषा]]) ने वस्तु -उन्मुख सिस्टम को औपचारिक रूप से निर्दिष्ट करने की अनुमति दी है।  


समवर्ती सॉफ्टवेयर और सिस्टम के लिए,[[ पेट्री नेत | पेट्री नेत]], [[ प्रक्रिया बीजगणित |प्रक्रिया बीजगणित]], और परिमित स्टेट मशीन (जो ऑटोमेटा सिद्धांत पर आधारित हैं - वर्चुअल परिमित स्टेट मशीन या[[ घटना संचालित परिमित राज्य मशीन | घटना संचालित परिमित स्टेट मशीन]] भी देखें) निष्पादन योग्य सॉफ़्टवेयर विनिर्देश की अनुमति देता है और इसका उपयोग एप्लिकेशन व्यवहार को बनाने और मान्य करने के लिए किया जा सकता है। ऑटोमेटा एक गणितीय प्रतिमान है जिसका प्रयोग कंप्यूटर प्रोग्राम तथा क्रमबद्ध लॉजिक सर्किटों की रचना करने में किया जाता है।
समवर्ती सॉफ्टवेयर और सिस्टम के लिए,[[ पेट्री नेत | पेट्री नेत]], [[ प्रक्रिया बीजगणित |प्रक्रिया बीजगणित]], और परिमित स्टेट मशीन (जो ऑटोमेटा सिद्धांत पर आधारित हैं - वर्चुअल परिमित स्टेट मशीन या[[ घटना संचालित परिमित राज्य मशीन | घटना संचालित परिमित स्टेट मशीन]] भी देखें) निष्पादन योग्य सॉफ़्टवेयर विनिर्देश की अनुमति देता है और इसका उपयोग एप्लिकेशन व्यवहार को बनाने और मान्य करने के लिए किया जा सकता है। ऑटोमेटा एक गणितीय मॉडल है जिसका प्रयोग कंप्यूटर प्रोग्राम तथा क्रमबद्ध लॉजिक परिपथों की रचना करने में किया जाता है।
 
सॉफ्टवेयर विकास में औपचारिक तरीकों के लिए एक अन्य दृष्टिकोण तर्क के किसी रूप में एक विनिर्देश लिखना है - आमतौर पर[[ प्रथम-क्रम तर्क ]](एफओएल) की भिन्नता - और फिर तर्क को सीधे निष्पादित करना जैसे कि यह एक कार्यक्रम था। [[ विवरण तर्क |विवरण तर्क]] (DL), पर आधारित[[ वेब ओन्टोलॉजी भाषा | वेब ओन्टोलॉजी भाषा]] इसका एक उदाहरण है। साथ ही इसमें अंग्रेजी के कुछ संस्करण (या किसी अन्य प्राकृतिक भाषा) को तर्क से स्वचालित रूप से पता लगाने के साथ-साथ तर्क को सीधे निष्पादित करने पर भी काम होता है। उदाहरण हैं [[ नियंत्रित अंग्रेजी का प्रयास |निमशीनित अंग्रेजी का प्रयास]],और इंटरनेट बिजनेस लॉजिक,जो शब्दावली या वाक्य-रचना को निमशीनित करने की कोशिश नहीं करते हैं। सिस्टम की एक विशेषता जो द्विदिश अंग्रेजी-तर्क का पता लगाने के साथ-साथ तर्क के प्रत्यक्ष निष्पादन का समर्थन करती है, वह यह है कि उन्हें अपने परिणामों को अंग्रेजी में, व्यवसाय या वैज्ञानिक स्तर पर समझाने के लिए बनाया जा सकता है।{{citation needed|date=June 2016}}
 
 


सॉफ्टवेयर विकास में औपचारिक तरीकों के लिए एक अन्य दृष्टिकोण तर्क के किसी रूप में एक विनिर्देश लिखना है - आमतौर पर[[ प्रथम-क्रम तर्क ]](एफओएल) की भिन्नता - और फिर तर्क को सीधे निष्पादित करना जैसे कि यह एक कार्यक्रम था। [[ विवरण तर्क |विवरण तर्क]] (DL), पर आधारित[[ वेब ओन्टोलॉजी भाषा | वेब ओन्टोलॉजी भाषा]] इसका एक उदाहरण है। साथ ही इसमें अंग्रेजी के कुछ संस्करण (या किसी अन्य प्राकृतिक भाषा) को तर्क से स्वचालित रूप से पता लगाने के साथ-साथ तर्क को सीधे निष्पादित करने पर भी काम होता है। उदाहरण हैं [[ नियंत्रित अंग्रेजी का प्रयास |निमशीनित अंग्रेजी का प्रयास]],और इंटरनेट बिजनेस लॉजिक,जो शब्दावली या वाक्य-रचना को निमशीनित करने की कोशिश नहीं करते हैं। सिस्टम की एक विशेषता जो द्विदिश अंग्रेजी-तर्क का पता लगाने के साथ-साथ तर्क के प्रत्यक्ष निष्पादन का समर्थन करती है, वह यह है कि उन्हें अपने परिणामों को अंग्रेजी में, व्यवसाय या वैज्ञानिक स्तर पर समझाने के लिए बनाया जा सकता है।
==औपचारिक तरीके और संकेतन==
==औपचारिक तरीके और संकेतन==
विभिन्न प्रकार के औपचारिक तरीके और संकेतन उपलब्ध हैं।   
विभिन्न प्रकार के औपचारिक तरीके और संकेतन उपलब्ध हैं।   


=== विशिष्टता भाषाएं ===
=== विशिष्टता भाषाएं ===
* [[ सार राज्य मशीनें | सार राज्य मशीनें]]  (एएसएम)
* [[ सार राज्य मशीनें |सार राज्य मशीनें]]  (एएसएम)
* ACL2 (ACL2)
* ACL2 (ACL2)
*[[ अभिनेता मॉडल | अभिनेता  प्रतिमान]]
*[[ अभिनेता मॉडल |अभिनेता  मॉडल]]
* मिश्र धातु भाषा
* मिश्र धातु भाषा
* एएनएसआई/आईएसओ सी विशिष्टता भाषा (एसीएसएल)
* एएनएसआई/आईएसओ सी विशिष्टता भाषा (एसीएसएल)
Line 132: Line 120:
* जेड अंकन
* जेड अंकन


=== प्रतिमानचेकर्स ===
=== मॉडलचेकर्स ===
{{main|List of model checking tools}}
* ईएसबीएमसी<ref>{{cite web| url=http://esbmc.org/ | title=ESBMC | website=esbmc.org }}</ref>
* ईएसबीएमसी<ref>{{cite web| url=http://esbmc.org/ | title=ESBMC | website=esbmc.org }}</ref>
* [[ MALPAS सॉफ्टवेयर स्टेटिक एनालिसिस टूलसेट | MALPAS सॉफ्टवेयर स्टेटिक एनालिसिस उपकरण]]समूह - एक औद्योगिक-शक्ति  प्रतिमानचेकर जिसका उपयोग सुरक्षा-महत्वपूर्ण प्रणालियों के औपचारिक प्रमाण के लिए किया जाता है
* [[ MALPAS सॉफ्टवेयर स्टेटिक एनालिसिस टूलसेट | MALPAS सॉफ्टवेयर स्टेटिक एनालिसिस उपकरण]]समूह - एक औद्योगिक-शक्ति  मॉडलचेकर जिसका उपयोग सुरक्षा-महत्वपूर्ण प्रणालियों के औपचारिक प्रमाण के लिए किया जाता है
* [[ पीएटी (मॉडल चेकर) | पीएटी ( प्रतिमानचेकर)]]  - समवर्ती सिस्टम और सीएसपी एक्सटेंशन (जैसे, साझा चर, सरणियाँ, निष्पक्षता) के लिए एक मुफ्त  प्रतिमानचेकर, सिम्युलेटर और शोधन परीक्षक
* [[ पीएटी (मॉडल चेकर) | पीएटी ( मॉडलचेकर)]]  - समवर्ती सिस्टम और सीएसपी एक्सटेंशन (जैसे, साझा चर, सरणियाँ, निष्पक्षता) के लिए एक मुफ्त  मॉडलचेकर, सिम्युलेटर और शोधन परीक्षक
* [[ स्पिन मॉडल चेकर | स्पिन  प्रतिमानचेकर]]
* [[ स्पिन मॉडल चेकर | स्पिन  मॉडलचेकर]]
* [[ उप्पल मॉडल चेकर | उप्पल  प्रतिमानचेकर]]
* [[ उप्पल मॉडल चेकर | उप्पल  मॉडलचेकर]]


==संगठन==
==संगठन==
{{main|:Category:Formal methods organizations}}
* [[ बीसीएस-एफएसीएस ]]
* [[ बीसीएस-एफएसीएस ]]
*[[ औपचारिक तरीके यूरोप ]]
*[[ औपचारिक तरीके यूरोप ]]
Line 152: Line 138:
* :श्रेणी:औपचारिक तरीके लोग
* :श्रेणी:औपचारिक तरीके लोग
* औपचारिक विनिर्देश
* औपचारिक विनिर्देश
*औपचारिक सत्यापन
*औपचारिक पद्यतियां
*[[ औपचारिक प्रणाली | औपचारिक सिस्टम]]
*[[ औपचारिक प्रणाली | औपचारिक सिस्टम]]
*प्रतिमानचेकिंग
*मॉडलचेकिंग
* [[ सॉफ्टवेयर इंजीनियरिंग | सॉफ्टवेयर अभियांत्रिकी]]
* [[ सॉफ्टवेयर इंजीनियरिंग | सॉफ्टवेयर अभियांत्रिकी]]
*विनिर्देश भाषा
*विनिर्देश भाषा
Line 160: Line 146:
==संदर्भ==
==संदर्भ==
{{reflist}}
{{reflist}}
==इस पृष्ठ में अनुपलब्ध आंतरिक कड़ियों की सूची==
*विशिष्ट एकीकृत परिपथ आवेदन
*डिजिटल डाटा
*आंकड़े
*के माध्यम से (इलेक्ट्रॉनिक्स)
*संवहन दस्तावेज़ स्वरूप
*विनिर्माण क्षमता के लिए बनावट (आईसी)
*सिलिकॉन सत्यापन पोस्ट करें
*मास्क डेटा तैयारी
*असफलता विश्लेषण
*रजिस्टर ट्रांसफर लेवल
*सी (प्रोग्रामिंग भाषा)
*यात्रा
*मांग
*उत्पाद आवश्यकता दस्तावेज़
*बाज़ार अवसर
*जीवन का अंत (उत्पाद)
*निर्देश समुच्चय
*तर्क अनुकरण
*सिग्नल की समग्रता
*बनावट नियम की जाँच
*टाइमिंग क्लोजर
*औपचारिक तुल्यता जाँच
*सामान्य केन्द्रक
*ऑप एंप
*मेंटर ग्राफिक्स
*एकीकृत परिपथों और प्रणालियों के कंप्यूटरसहायता प्राप्त बनावट पर आईईईई लेनदेन
*असफलता विश्लेषण
*एन पी-सम्पूर्ण
*परीक्षण वेक्टर
*controllability
*observability
*प्रशंसक एल्गोरिदम
*कूट-यादृच्छिक
*पंक्ति का पिछला अंत
*बांड विशेषता
*दोहरी इन-लाइन पैकेज
*मरो (एकीकृत सर्किट)
*निर्माण (अर्धचालक)
*विद्युतचुंबकीय व्यवधान
*epoxy
*भली भांति बंद सील
*फ्लैटपैक (इलेक्ट्रॉनिक्स)
*पतली छोटी रूपरेखा पैकेज
*गोंद
*मेटलाइजिंग
*अनावर्ती अभियांत्रिकी
*बाजार के लिए समय
*तार का जोड़
*नमी
*विद्युतीय
*स्थानीय कर से मुक्ति
*साफ-सुथरे कमरे
*अवरोधित हो जाना
*HIRF
*एकीकृत परिपथ
*रूटिंग (इलेक्ट्रॉनिक बनावट ऑटोमेशन)
*प्रक्रिया के कोने
*मानक सेल
*आईसी बिजली की आपूर्ति पिन
*घड़ी की आवृत्ति
*सिग्नल की समग्रता
*उत्तम नस्ल
*रजिस्टर ट्रांसफर लेवल
*मूल्य संवर्धित
*पुस्तकालय (कंप्यूटरविज्ञान)
*प्रतिमानआधारित बनावट
*स्वत: निमशीनण
*राज्य मशीनें
*सोर्स संकेत-लिपि
*स्वचालित संकेत-लिपि पीढ़ी
*शून्य से विभाजन
*आवश्यकताओं का पता लगाने योग्यता
*प्रतिमानजांच
*औपचारिक तरीके
*प्रतिमानकेंद्र
*वेब आधारित अनुकरण
*Xcos
*साइलैब
*पूर्णांक
*मैक ओएस
*प्रयोक्ता इंटरफ़ेस
*समारोह (गणित)
*फोरट्रान
*स्थिर (कंप्यूटरविज्ञान)
*खिसकाना
*जादू वर्ग
*लैम्ब्डा कैलकुलस
*मेक्स फ़ाइल
*मेथेमेटिका
*तुम क्या सहन करते हो
*संख्यात्मक-विश्लेषण सॉफ्टवेयर की तुलना
*आईईईई मानक
*एक्सेलेरा
*जावा (प्रोग्रामिंग भाषा)
*पैक्ड सरणी
*कड़ा मुकाबला
*struct
*टाइपडीफ
*कुंडी (इलेक्ट्रॉनिक)
*रन टाइम (कार्यक्रम जीवनचक्र चरण)
*एकल विरासत
*टेम्पलेट विशेषज्ञता
*जानकारी छिपाना
*ऑपरेटर नया
*यादृच्छिक परीक्षण
*सामग्री निहितार्थ (अनुमान का नियम)
*पूर्ववृत्त (तर्क)
*फलस्वरूप
*सिमुलेशन
*स्वचालित प्रमेय सिद्ध करना
*कार्तीय गुणन
*परीक्षण के अंतर्गत उपकरण
*बनावट अंतरिक्ष सत्यापन
*टेस्ट कवरेज
*उदाहरण (कंप्यूटरविज्ञान)
*तुल्यकालन (कंप्यूटरविज्ञान)
*सशक्त टाइपिंग
*पाश के लिए
*बहाव को काबू करें
*लगातार (कंप्यूटरप्रोग्रामिंग)
*भाषा अंतरसंचालनीयता
*सी-परिवार प्रोग्रामिंग भाषाओं की सूची
*प्रक्रमण करने से पहले के निर्देश
*मूल फाइल
*लिंट (सॉफ्टवेयर)
*एकीकृत सर्किट बनावट
*एकीकृत सर्किट लेआउट
*एकीकृत परिपथ
*पूरा रिवाज
*इन्सुलेटर पर सिलिकॉन
*मुखौटा डेटा तैयारी
*उच्च स्तरीय संश्लेषण
*असतत घटना सिमुलेशन
*आईडिया1
*उच्च स्तरीय प्रोग्रामिंग भाषा
*कंप्यूटर वैज्ञानिक
*वितरित अभिकलन
*व्युत्पन्न वर्ग
*सीएलयू (प्रोग्रामिंग भाषा)
*अदा (प्रोग्रामिंग भाषा)
*कक्षा (कंप्यूटरप्रोग्रामिंग)
*कास्ट (कंप्यूटरविज्ञान)
*एक्सेप्शन हेंडलिंग
*सभा की भाषा
*अवधारणाएं (सी ++)
*सी ++ मानक पुस्तकालय
*एब्स्ट्रैक्शन (कंप्यूटरसाइंस)
*कक्षा (कंप्यूटरविज्ञान)
*संकलन समय
*सहयोगी सरणी
*सुविधा (सॉफ्टवेयर बनावट)
*अनवरत वृद्धि # अनिमशीनित विस्तार
*विशिष्ट एकीकृत परिपथ आवेदन
*अर्धचालक निर्माण
*एक चिप पर प्रणाली
*नि: शुल्क
*अनुक्रमिक तर्क
*स्थान और मार्ग
*रूटिंग (ईडीए)
*सेमीकंडक्टर
*आर्किटेक्ट
*फ्लोरेंस कैथेड्रल
*वास्तु सिद्धांत
*समसामयिक आर्किटेक्चर
*गोथिक वास्तुशिल्प
*फार्म समारोह के बाद
*मंजिल की योजना
*सुनहरा अनुपात
*वास्तुकला बनावट मूल्य
*पुनर्निर्माणवाद
*क्लासिकल एंटिक्विटी
*कैथेड्रल
*सौंदर्यशास्र
*अभिव्यंजनावादी वास्तुकला
*वास्तु घटना विज्ञान
*हरा भवन
*हरित बुनियादी ढाँचा
*संकल्पनात्मक निदर्श
*व्‍यवहार
*वास्तुकला प्रौद्योगिकी
*कटलरी
*बनावट के तरीके
*संकल्पनात्मक निदर्श
*झरना मॉडल
*शोध करना
*उत्पाद बनावट विनिर्देश
*संक्षिप्त आकार
*उत्पाद का परीक्षण करना
*समस्या को सुलझाना
*दस्तावेज़
*साइट पर
*आशुरचना
*चुस्त सॉफ्टवेयर विकास
*उपयोगकर्ता केंद्रित बनावट
*ग्राफक कला
*एप्लाइड आर्ट्स
*मुहावरा
*चिन्ह, प्रतीक
*जानबूझकर परिभाषा
*अंक शास्त्र
*सूक्तियों
*आवश्यक और पर्याप्त शर्तें
*लिंग-अंतर परिभाषा
*त्रिकोण
*चतुष्कोष
*पदार्थवाद
*संभव दुनिया
*कठोर अभिकर्ता
*संचालनगत परिभाषा
*समनाम
*निराकरण
*संकेत (सेमियोटिक्स)
*सेमे (शब्दार्थ)
*शब्द भावना
*अर्थ क्षेत्र
*अर्थ (भाषाविज्ञान)
*निओलगिज़्म
*अपरिष्कृत किस्म
*परिभाषा के अनुसार विस्तार
*आत्म संदर्भ
*चिकित्सा सहमति
*चिकित्सा वर्गीकरण
*शाब्दिक परिभाषा
*मतवाद
*प्राणी
*दार्शनिक जांच
*व्यक्तित्व का सिद्धांत
*विवरण का सिद्धांत
*शाऊल क्रिप्के
*अनिश्चितता (दर्शनशास्त्र)
*अर्थ विज्ञान
*जानकारी
*सरल भाषा
*भाषा: हिन्दी
*बातचीत का माध्यम
*सूचना प्रक्रम
*गुप्तता
*लिख रहे हैं
*आधार - सामग्री संकोचन
*हाव-भाव
*कुल कार्य
*कड़ी
*संकेत-लिपि वर्ड
*कम घनत्व समता-जांच संकेत-लिपि
*उच्चारण क्षमता
*चरित्र (कंप्यूटिंग)
*एचटीटीपी हेडर
*जेनेटिक संकेत-लिपि
*जीवविज्ञान
*अवरोध
*पत्रक संगीत
*क्रिप्टोग्राफी का इतिहास
*पाठ के प्रस्तुतिकरण के लिए प्रयुक्त भाषा
*टेक्स्ट एन्संकेत-लिपििंग पहल
*SECAM
*शब्दार्थ एन्संकेत-लिपििंग
*मेमोरी एन्संकेत-लिपििंग
*लेखन प्रणाली
*सांकेतिकता
*संकेत-लिपि (सेमियोटिक्स)
*असिमिक लेखन
*जाँचने का तरीका
*निहाई
*बरबाद करना
*प्रथम लेख निरीक्षण
*प्राथमिक धारा
*फाइल का प्रारूप
*फ़ाइल साझा करना
*सर्वाधिकार उल्लंघन
*संशोधित असतत कोसाइन परिवर्तन
*अंतरराष्ट्रीय मानकीकरण संगठन
*इंटरनेशनल इलेक्ट्रोटेक्नीकल कमीशन
*बुंदाडा इटाकुरा
*असतत कोसाइन परिवर्तन
*फिल्टर (सॉफ्टवेयर)
*धोखाधड़ी
*एमपीईजी-1 ऑडियो परत II
*झूठा
*नमूनाकरण दर
*संदर्भ कार्यान्वयन (कंप्यूटिंग)
*सोल
*धुन (ऑनलाइन संगीत सेवा)
*जॉइन्ट स्टीरियो
*त्रुटि की जांच कर रहा है
*पूर्व बनाया
*संपीड़न विरूपण साक्ष्य
*लाल किताब (ऑडियो सीडी मानक)
*आईएफए शो
*कार्य (ऑडियो प्रारूप)
*सेब दोषरहित
*एमपीईजी -4 भाग 14
*बयान (कंप्यूटरविज्ञान)
*सॉफ़्टवेयर परीक्षण
*एसीएम का संचार
*सुरक्षा महत्वपूर्ण
*परिमित अवस्था मशीन
*रुकने की समस्या
*ताल बनावट प्रणाली
*एफपीजीए प्रोटोटाइप
*कदम स्तर
*एम्यूलेटर
*उन्नत लघु उपकरण
*सेंट्रल प्रोसेसिंग यूनिट
*स्पर्धारोधी कानून
*शुरुआती सार्वजानिक प्रस्ताव
*क्रेग बैरेट (व्यापारी)
*एंटीट्रस्ट
*एआईएम गठबंधन
*किफायती इंटरनेट के लिए गठबंधन
*सेब सिलिकॉन
*EPROM
*विद्युत ऊर्जा की खपत
*एम्बर झील (सूक्ष्म वास्तुकला)
*Apple वर्ल्डवाइड डेवलपर्स कॉन्फ्रेंस
*स्वतंत्र रूप से पुनर्वितरण योग्य सॉफ्टवेयर
*प्रचार अभियान
*प्रतिस्पर्धी विरोधी प्रथाएं
*एथिलबेन्जीन
*संघर्ष संसाधन
*कन्फ्लिक्ट खनिज
*आयु भेदभाव
*बम्पलेस बिल्ड-अप परत
*उत्पाद वापसी
*प्रधान चौगुनी
*प्राइम ट्रिपलेट
*जुड़वां प्रधान
*प्रतीकात्मक प्रक्षेपवक्र मूल्यांकन
*कदम स्तर
*पुस्तकालय (कम्प्यूटिंग)
*औपचारिक विशिष्टता
*सिस्टम टाइप करें
*कंप्यूटरविज्ञान में तर्क
*शर्त लगाना
*कार्यक्रम परिशोधन
*स्वचालित प्रमेय प्रोवर
*जेड अंकन
*उदाहरण
*अनिश्चितता
*ओरेकल मशीन
*एडीए प्रोग्रामिंग भाषा
*वस्तु बाधा भाषा
*परिमित अवस्था मशीन
*आभासी परिमित राज्य मशीन
*औद्योगिक सॉफ्टवेयर अभियांत्रिकी के लिए कठोर दृष्टिकोण
*विशिष्टता और विवरण भाषा
*RAISE विनिर्देश भाषा
*विशिष्टता भाषा
==अग्रिम पठन==
==अग्रिम पठन==
{{refbegin}}
{{refbegin}}
Line 532: Line 166:


{{Computer science}}
{{Computer science}}
{{Software engineering}}
{{DEFAULTSORT:Formal Methods}}
[[Category:Machine Translated Page]]


{{DEFAULTSORT:Formal Methods}}
[[Category:Articles with hatnote templates targeting a nonexistent page|Formal Methods]]
[[Category:Articles with short description|Formal Methods]]
[[Category:CS1 English-language sources (en)]]
[[Category:CS1 errors]]
[[Category:Collapse templates|Formal Methods]]
[[Category:Navigational boxes| ]]
[[Category:Navigational boxes without horizontal lists|Formal Methods]]
[[Category:Pages with script errors|Formal Methods]]
[[Category:Short description with empty Wikidata description|Formal Methods]]
[[Category:Sidebars with styles needing conversion|Formal Methods]]
[[Category:Template documentation pages|Documentation/doc]]
[[Category:Templates generating microformats|Formal Methods]]
[[Category:Templates that are not mobile friendly|Formal Methods]]
[[Category:Templates using TemplateData|Formal Methods]]
[[Category:Webarchive template wayback links]]
[[Category:Wikipedia metatemplates|Formal Methods]]

Latest revision as of 17:10, 13 September 2023

कंप्यूटर विज्ञान में, सॉफ़्टवेयर और कंप्यूटर धातु सामग्री, हार्डवेयर सिस्टम की विशिष्टता, विकास के औपचारिक पद्यतियां (फॉर्मल मेथड्स) के लिए गणित की जटिल तकनीकें हैं।[1] सॉफ्टवेयर और हार्डवेयर डिजाइन के लिए औपचारिक तरीकों का उपयोग इस आशा से प्रेरित है कि, अन्य इंजीनियरिंग विषयों की तरह, उपयुक्त गणितीय विश्लेषण करने से डिजाइन की विश्वसनीयता और दृढ़ता में योगदान हो सकता है[2]।

औपचारिक विधियाँ विभिन्न प्रकार के सैद्धांतिक कंप्यूटर विज्ञा के बुनियादी सिद्धांतों को नियोजित करती हैं, जिनमें तर्क गणना, औपचारिक भाषा, ऑटोमेटा सिद्धांत, नियंत्रण सिद्धांत, कार्यक्रम शब्दार्थ, प्रकार प्रणाली और प्रकार सिद्धांत सम्मिलित हैं।[3]

पृष्ठभूमि

अर्ध-औपचारिक तरीके औपचारिकता और भाषाएं हैं जिन्हें पूरी तरह से "औपचारिक" नहीं माना जाता है। यह शब्दार्थ को बाद के चरण में पूरा करने के कार्य को स्थगित करता है, जो तब या तो मानव व्याख्या द्वारा या कोड या टेस्ट केस जनरेटर जैसे सॉफ़्टवेयर के माध्यम से व्याख्या द्वारा किया जाता है।[4]

वर्गीकरण

औपचारिक तरीकों का प्रयोग कई स्तरों पर किया जा सकता है:

स्तर 0: औपचारिक विनिर्देश शुरू करके और फिर अनौपचारिक रूप से इससे एक कार्यक्रम विकसित किया जा सकता है। इसे "औपचारिक विधि" कहा जाता है। यह कई मामलों में सबसे कम लागत विकल्प हो सकता है।

स्तर 1: औपचारिक विकास और औपचारिक पद्यतियां का उपयोग किसी कार्यक्रम को अधिक औपचारिक विधि से तैयार करने के लिए किया जा सकता है। उदाहरण के लिए, किसी कार्यक्रम के औपचारिक विनिर्देश से गुणों या कार्यक्रम के शोधन के प्रमाण किए जा सकते हैं। यह सुरक्षा से जुड़े उच्च-अखंडता प्रणालियों में सबसे उपयुक्त हो सकता है।

स्तर 2: प्रमेय प्रोवर्स का उपयोग पूरी तरह से औपचारिक मशीन-चेक किए गए प्रमाणों को करने के लिए किया जा सकता है। यदि त्रुटियों का मान बहुत अधिक है तो उपकरण सुधार और घटती लागत के बजाय, यह बहुत महंगा हो सकता है और केवल व्यावहारिक रूप से सार्थक है (उदाहरण के लिए, क्रिया संचालन (ऑपरेटिंग) सिस्टम या माइक्रोसंसाधक बनावट के महत्वपूर्ण भागों में है)।

इसके बारे में अधिक जानकारी नीचे दी गई है।

प्रोग्रामिंग भाषाओं के औपचारिक शब्दार्थ के साथ,औपचारिक विधियों की शैलियों को मोटे तौर पर निम्नानुसार वर्गीकृत किया जा सकता है:

  • सांकेतिक शब्दार्थ, जिसमें एक सिस्टम का अर्थ क्षेत्र (डोमेन) सिद्धांत के गणितीय सिद्धांत में व्यक्त किया जाता है। इस तरह के तरीकों के समर्थक सिस्टम को अर्थ देने के लिए क्षेत्र की अच्छी तरह से समझी गई प्रकृति पर भरोसा करते हैं; आलोचकों का कहना है कि हर सिस्टम को सहज या स्वाभाविक रूप से एक कार्य के रूप में नहीं देखा जा सकता है।
  • परिचालन शब्दार्थ , जिसमें एक सिस्टम का अर्थ एक (संभवतः) सरल अभिकलन मॉडल (कम्प्यूटेशनल मॉडल) की क्रियाओं के अनुक्रम के रूप में व्यक्त किया जाता है। इस तरह के तरीकों के समर्थक अपने मॉडल की सादगी को अभिव्यक्तिपूर्ण स्पष्टता के साधन के रूप में इंगित करते हैं; आलोचकों का कहना है कि शब्दार्थ की समस्या में अभी देरी हुई है (जो सरल मॉडल के शब्दार्थ को परिभाषित करता है)
  • स्वयंसिद्ध शब्दार्थ , जिसमें सिस्टम का अर्थ पूर्व शर्त और शर्त के बाद के संदर्भ में व्यक्त किया जाता है जो कि सिस्टम द्वारा किसी कार्य को करने से पहले और बाद में एक कार्य करता है। समर्थकों ने प्राचीन तर्क के संबंध पर ध्यान दिया; आलोचकों ने ध्यान दिया कि इस तरह के शब्दार्थ वास्तव में कभी भी यह वर्णन नहीं करते हैं कि एक सिस्टम क्या करती है। (केवल वही जो पहले और बाद में सच है)

सरल औपचारिक तरीके

कुछ चिकित्सकों का मानना ​​​​है कि औपचारिक तरीके समुदाय ने एक विनिर्देश या बनावट की पूर्ण औपचारिकता पर अधिक जोर दिया है।[5][6] उनका तर्क है कि इसमें सम्मिलित भाषाओं की अभिव्यंजना, साथ ही प्रतिरूपित की जा रही प्रणालियों की जटिलता, पूर्ण औपचारिकता को एक कठिन और महंगा कार्य बनाती है। एक विकल्प के रूप में, विभिन्न हल्के औपचारिक तरीके, जो आंशिक विनिर्देश और केंद्रित अनुप्रयोग पर जोर देते हैं, एक विकल्प के रूप में, प्रस्तावित किए गए हैं। औपचारिक तरीकों के लिए इस हल्के दृष्टिकोण के उदाहरणों में मिश्र धातु भाषा (वस्तु प्रतिरूपण संकेतन) वस्तु मॉडलिंग नोटेशन सम्मिलित है,[7] Z संकेतन के कुछ पहलुओं का डेनी का संश्लेषण,[8] उपयोग केस संचालित विकास, और CSK (सीएसके) VDM (वियना विकास विधि) उपकरण् है।[9]

उपयोग

सॉफ्टवेयर विकास प्रक्रिया के माध्यम से विभिन्न बिंदुओं पर औपचारिक तरीकों को लागू किया जा सकता है।

विशिष्टता

विकसित की जाने वाली सिस्टम का विवरण देने के लिए, चाहे किसी भी स्तर पर विवरण वांछित हो,औपचारिक तरीकों का इस्तेमाल किया जा सकता है। इस औपचारिक विवरण का उपयोग आगे की विकास गतिविधियों को निर्देशित करने के लिए किया जा सकता है (निम्नलिखित अनुभाग देखें); इसके अतिरिक्त, इसका उपयोग यह सत्यापित करने के लिए किया जा सकता है कि विकसित की जा रही सिस्टम की आवश्यकताओं को पूरी तरह और सटीक रूप से निर्दिष्ट किया गया है, या औपचारिक भाषा में उन्हें एक सटीक और स्पष्ट रूप से परिभाषित वाक्यविन्यास और शब्दार्थ के साथ औपचारिक भाषा में व्यक्त करके औपचारिक रूप दिया गया है।

औपचारिक विनिर्देश प्रणालियों की आवश्यकता को वर्षों से नोट किया गया है। ALGOL 58 आख्या (रिपोर्ट) में,[10] जॉन बैकस ने प्रोग्रामिंग भाषा वाक्यविन्यास, का वर्णन करने के लिए एक औपचारिक संकेतन प्रस्तुत किया, जिसे बाद में बैकस सामान्य रूप नाम दिया गया और फिर इसका नाम बदलकर बैकस-नौर फॉर्म (बीएनएफ) कर दिया गया।[11] बैकस ने यह भी लिखा है कि वाक्यात्मक रूप से मान्य ALGOL कार्यक्रमों के अर्थ का औपचारिक विवरण आख्या में सम्मिलित करने के लिए समय पर पूरा नहीं किया गया था।" इसलिए कानूनी कार्यक्रमों के शब्दार्थ का औपचारिक उपचार बाद के पेपर में सम्मिलित किया जाएगा।" यह कभी नहीं दिखाई दिया।

विकास

औपचारिक विकास एक उपकरण समर्थित सिस्टम विकास प्रक्रिया के एक एकीकृत भाग के रूप में औपचारिक तरीकों का उपयोग है।

एक बार औपचारिक विनिर्देश तैयार हो जाने के बाद, विनिर्देश को एक मार्गदर्शक के रूप में इस्तेमाल किया जा सकता है, जबकि ठोस सिस्टम सॉफ्टवेर रचना प्रक्रिया के दौरान विकसित हुआ था (यानी आम तौर पर, सॉफ्टवेयर में महसूस किया जाता है, लेकिन संभावित रूप से हार्डवेयर में भी)। उदाहरण के लिए:

  • यदि औपचारिक विनिर्देश परिचालन शब्दार्थ में है, तो ठोस सिस्टम के देखे गए व्यवहार की तुलना विनिर्देश के व्यवहार से की जा सकती है (जो स्वयं निष्पादन योग्य या अनुकरणीय होना चाहिए)। इसके अतिरिक्त, विनिर्देशन के परिचालन आदेश निष्पादन योग्य संकेत-लिपि में अनुवाद को निर्देशित करने के लिए उपयुक्त हो सकते हैं।
  • यदि औपचारिक विनिर्देश स्वयंसिद्ध शब्दार्थ में है, तो विनिर्देश की पूर्व शर्त और बाद की शर्तें निष्पादन योग्य संकेत-लिपि में अभिकथन (कंप्यूटिंग) बन सकती हैं।

पद्यतियां

औपचारिक पद्यतियां एक औपचारिक विनिर्देश के गुणों को साबित करने के लिए सॉफ़्टवेयर उपकरण (टूल) का उपयोग है, या यह साबित करने के लिए कि सिस्टम कार्यान्वयन का एक औपचारिक मॉडल इस के विनिर्देश को पूरा करता है।

एक बार औपचारिक विनिर्देश विकसित हो जाने के बाद, विनिर्देश का उपयोग विनिर्देश केगणितीय प्रमाण गुणों के आधार के रूप में, अनुमान से, सिस्टम कार्यान्वयन के गुण के रूप में किया जा सकता है।

साइन-ऑफ पद्यतियां

साइन-ऑफ पद्यतियां एक औपचारिक पद्यतियां उपकरण का उपयोग है जो अत्यधिक विश्वसनीय है। ऐसा उपकरण पारंपरिक पद्यतियां विधियों को प्रतिस्थापित कर सकता है (उपकरण प्रमाणित भी हो सकता है)।

मानव निर्देशित सबूत

कभी-कभी, सिस्टम की शुद्धता (कंप्यूटर विज्ञान) को साबित करने के लिए, सिस्टम की शुद्धता को साबित करने की स्पष्ट आवश्यकता नहीं है, बल्कि सिस्टम को बेहतर ढंग से समझने की इच्छा है। नतीजतन, गणितीय प्रमाण की शैली में शुद्धता के कुछ प्रमाण तैयार किए जाते हैं: ऐसे प्रमाणों के लिए सामान्य अनौपचारिकता के स्तर का उपयोग करते हुए, प्राकृतिक भाषा का उपयोग, हस्तलिखित (या टाइपसेट), एक अच्छा प्रमाण वह है जो अन्य मानव पाठकों द्वारा पठनीय और समझने योग्य हो।

इस तरह के दृष्टिकोण के आलोचक बताते हैं कि प्राकृतिक भाषा में निहित अस्पष्टता ऐसे प्रमाणों में त्रुटियों का पता लगाने की अनुमति नहीं देती है; अक्सर, सूक्ष्म त्रुटियाँ निम्न-स्तरीय विवरणों में मौजूद हो सकती हैं जिन्हें आमतौर पर ऐसे प्रमाणों द्वारा अनदेखा किया जाता है। इसके अतिरिक्त, इस तरह के एक अच्छे प्रमाण के निर्माण में सम्मिलित कार्य के लिए उच्च स्तर के गणितीय परिष्कार और विशेषज्ञता की आवश्यकता होती है।

स्वचालित प्रमाण

इसके विपरीत, स्वचालित साधनों द्वारा ऐसी प्रणालियों की शुद्धता के प्रमाण प्रस्तुत करने में रुचि बढ़ रही है। स्वचालित तकनीक तीन सामान्य श्रेणियों में आती है:

  • स्वचालित प्रमेय सिद्ध करना, जिसमें एक सिस्टम खरोंच से एक औपचारिक प्रमाण का उत्पादन करने का प्रयास करती है, सिस्टम का विवरण दिया जाता है, तार्किक स्वयंसिद्धों का एक समूह (सेट) और अनुमान नियमों का एक समूह दिया जाता है।
  • मॉडल जांच, जिसमें एक सिस्टम सभी संभावित स्तरों की विस्तृत खोज के माध्यम से कुछ गुणों का पद्यतियां करता है जो एक सिस्टम अपने निष्पादन के दौरान दर्ज कर सकता है।
  • सार व्याख्या , जिसमें एक सिस्टम कार्यक्रम की एक व्यवहारिक लक्षण के अति-सन्निकटन की पुष्टि करती है, इसका प्रतिनिधित्व करने वाले (संभवतः पूर्ण) जालक पर एक फिक्सपॉइंट गणना का उपयोग करके।

कुछ स्वचालित प्रमेय प्रोवर्स को मार्गदर्शन की आवश्यकता होती है कि कौन से गुण काफी रोचक हैं जो आगे बढ़ने के लिए पर्याप्त हैं, जबकि अन्य मानवीय हस्तक्षेप के बिना काम करते हैं। यदि पर्याप्त रूप से सार मॉडल नहीं दिया जाता है, तो मॉडल चेकर्स (जाँच) लाखों अरोचक स्तरों की जाँच में जल्दी से फंस सकते हैं।

ऐसी प्रणालियों के समर्थकों का तर्क है कि परिणामों में, मानव-निर्मित प्रमाणों की तुलना में अधिक गणितीय निश्चितता है, क्योंकि सभी अरोचक विवरणों को एल्गोरिथम रूप से सत्यापित किया गया है। ऐसी प्रणालियों का उपयोग करने के लिए आवश्यक प्रशिक्षण भी हाथ से अच्छे गणितीय प्रमाण तैयार करने के लिए आवश्यक प्रशिक्षण से कम है, जिससे तकनीक बहुत से चिकित्सकों के लिए आसान हो जाती है।

आलोचक ध्यान दें कि उनमें से कुछ प्रणालियाँ आकाशवाणी (ओरेकल) मशीनों की तरह हैं: वे सत्य का उच्चारण करती हैं, फिर भी उस सत्य का कोई स्पष्टीकरण नहीं देती हैं। ऐसी सिस्टम में "पद्यतियांकर्ता के पद्यतियां" की समस्या भी है ; यदि पद्यतियां में सहायता करने वाला कार्यक्रम स्वयं अप्रमाणित है, तो उत्पादित परिणामों की सुदृढ़ता पर संदेह करने का कारण हो सकता है। कुछ आधुनिक मॉडल जाँच उपकरण अपने प्रमाण में प्रत्येक चरण का विवरण देते हुए एक "प्रमाण लॉग" उत्पन्न करते हैं, जिससे स्वतंत्र पद्यतियां दिए जाने, उपयुक्त उपकरण का प्रदर्शन करना संभव हो जाता है।

अमूर्त व्याख्या दृष्टिकोण की मुख्य विशेषता यह है कि यह एक ध्वनि विश्लेषण प्रदान करता है, अर्थात कोई गलत नकारात्मक वापस नहीं किया जाता है। इसके अलावा, यह विश्लेषण की जाने वाली संपत्ति का प्रतिनिधित्व करने वाले अमूर्त क्षेत्र को ट्यून करके, और तेजी से अभिसरण प्राप्त करने के लिए व्यापक ऑपरेटरों को लागू करके।[12]

आवेदन

राउटर, ईथरनेट स्विच, रूटिंग प्रोटोकॉल, सुरक्षा एप्लिकेशन और क्रिया संचालन सिस्टम माइक्रोकर्नेल जैसे seL4 सहित हार्डवेयर और सॉफ्टवेयर के विभिन्न क्षेत्रों में औपचारिक तरीके लागू होते हैं। ऐसे कई उदाहरण हैं जिनमें इनका उपयोग DC में प्रयुक्त हार्डवेयर और सॉफ़्टवेयर की कार्यक्षमता को सत्यापित करने के लिए किया गया है. IBM ने AMD x86 संसाधक विकास प्रक्रिया में ACL2 , एक प्रमेय प्रोवर का उपयोग किया। इंटेल अपने हार्डवेयर और फ़र्मवेयर को सत्यापित करने के लिए ऐसे तरीकों का उपयोग करता है (स्थायी सॉफ़्टवेयर को केवल पठनीय स्मृति (रीड ऑनली मैमोरी) में प्रोग्राम किया जाता है) डेनिश सूचना विज्ञान केंद्र ने 1980 के दशक में एडा (Ada) प्रोग्रामिंग भाषा के लिए एक कंपाइलर सिस्टम विकसित करने के लिए औपचारिक तरीकों का इस्तेमाल किया, जो एक लंबे समय तक चलने वाला व्यावसायिक उत्पाद बन गया।[13][14]नासा की कई अन्य परियोजनाएं हैं जिनमें औपचारिक तरीकों को लागू किया जाता है, जैसे अगली पीढ़ी हवाई परिवहन सिस्टम राष्ट्रीय हवाई क्षेत्र सिस्टम में मानवरहित विमान सिस्टम का एकीकरण,[15] और एयरबोर्न को ऑर्डिनेटेड कॉन्फ्लिक्ट रेजोल्यूशन एंड डिटेक्शन (ACCoRD)।[16]एटेलियर बी के साथ बी-विधि,[17]आल्सटॉम और सीमेंस द्वारा दुनिया भर में स्थापित विभिन्न उपमार्ग के लिए सुरक्षा स्वचालितता विकसित करने के लिए उपयोग किया जाता है, और सामान्य मानदंड प्रमाणन और एटीएमईएल और एसटीएमइक्रोइलेक्ट्रॉनिक्स द्वारा सिस्टम मॉडल के विकास के लिए भी उपयोग किया जाता है।

अधिकांश जाने-माने हार्डवेयर विक्रेताओं, जैसे आईबीएम, इंटेल और एएमडी द्वारा हार्डवेयर में औपचारिक पद्यतियां अक्सर किया जाता है। हार्डवेयर के कई क्षेत्र हैं, जहां इंटेल ने उत्पादों के कामकाज को सत्यापित करने के लिए एफएम का उपयोग किया है, जैसे कैश-कोहेरेंट प्रोटोकॉल का पैरामीटरयुक्त पद्यतियां,[18] इंटेल कोर i7 संसाधक निष्पादन इंजन पद्यतियां[19] (प्रमेय सिद्ध करने, द्विआधारी निर्णय आरेख,और प्रतीकात्मक मूल्यांकन का उपयोग करके), एचओएल प्रकाश प्रमेय प्रोवर का उपयोग करके इंटेल आईए -64 आर्किटेक्चर का इष्टतम उपयोग करके,[20] और ताल (केडेंस) का उपयोग करते हुए पीसीआई एक्सप्रेस प्रोटोकॉल और इंटेल अग्रिम प्रबंधन प्रौद्योगिकी के समर्थन के साथ उच्च-प्रदर्शन दोहरे पोर्ट गीगाबिट ईथरनेट निमशीनक का पद्यतियां।[21] इसी तरह, आईबीएम ने पावर गेट्स के पद्यतियां में औपचारिक तरीकों का इस्तेमाल किया है,[22] रजिस्टर,[23] और IBM Power7 माइक्रोसंसाधक के पद्यतियां[24] में औपचारिक तरीकों का इस्तेमाल किया है।

सॉफ्टवेयर विकास में

सॉफ़्टवेयर विकास में, औपचारिक विधियाँ आवश्यकताओं, विनिर्देश और डिज़ाइन स्तरों पर सॉफ़्टवेयर (और हार्डवेयर) समस्याओं को हल करने के लिए गणितीय दृष्टिकोण हैं। औपचारिक तरीकों को सुरक्षा-महत्वपूर्ण या सुरक्षा-महत्वपूर्ण सॉफ़्टवेयर और प्रणाली, जैसे एवियोनिक्स सॉफ्टवेयर पर लागू होने की सबसे अधिक संभावना है। सॉफ़्टवेयर सुरक्षा आश्वासन मानक, जैसे DO-178C पूरकता के माध्यम से औपचारिक तरीकों के उपयोग की अनुमति देता है, और सामान्य मानदंड वर्गीकरण के उच्चतम स्तरों पर औपचारिक तरीकों को अनिवार्य करता है।

अनुक्रमिक सॉफ़्टवेयर के लिए, औपचारिक तरीकों के उदाहरणों में बी-विधि, स्वचालित प्रमेय सिद्ध करने में उपयोग की जाने वाली विनिर्देश भाषाएँ, औद्योगिक सॉफ़्टवेयर अभियांत्रिकी के लिए कठोर दृष्टिकोण (RAISE) और Z संकेतन सम्मिलित हैं।

कार्यात्मक प्रोग्रामिंग में, संपत्ति-आधारित परीक्षण ने व्यक्तिगत कार्यों के अपेक्षित व्यवहार के गणितीय विनिर्देश और त्वरित परीक्षण (यदि संपूर्ण परीक्षण नहीं) की अनुमति दी है।

यदि वस्तु -ओरिएंटेड (वस्तु उन्मुख) प्रणाली, औपचारिक रूप से सत्यापित नहीं किया गया है तो वस्तु (ऑब्जेक्ट) बाधा भाषा (और विशेषज्ञता जैसे जावा मॉडलिंग भाषा) ने वस्तु -उन्मुख सिस्टम को औपचारिक रूप से निर्दिष्ट करने की अनुमति दी है।

समवर्ती सॉफ्टवेयर और सिस्टम के लिए, पेट्री नेत, प्रक्रिया बीजगणित, और परिमित स्टेट मशीन (जो ऑटोमेटा सिद्धांत पर आधारित हैं - वर्चुअल परिमित स्टेट मशीन या घटना संचालित परिमित स्टेट मशीन भी देखें) निष्पादन योग्य सॉफ़्टवेयर विनिर्देश की अनुमति देता है और इसका उपयोग एप्लिकेशन व्यवहार को बनाने और मान्य करने के लिए किया जा सकता है। ऑटोमेटा एक गणितीय मॉडल है जिसका प्रयोग कंप्यूटर प्रोग्राम तथा क्रमबद्ध लॉजिक परिपथों की रचना करने में किया जाता है।

सॉफ्टवेयर विकास में औपचारिक तरीकों के लिए एक अन्य दृष्टिकोण तर्क के किसी रूप में एक विनिर्देश लिखना है - आमतौर परप्रथम-क्रम तर्क (एफओएल) की भिन्नता - और फिर तर्क को सीधे निष्पादित करना जैसे कि यह एक कार्यक्रम था। विवरण तर्क (DL), पर आधारित वेब ओन्टोलॉजी भाषा इसका एक उदाहरण है। साथ ही इसमें अंग्रेजी के कुछ संस्करण (या किसी अन्य प्राकृतिक भाषा) को तर्क से स्वचालित रूप से पता लगाने के साथ-साथ तर्क को सीधे निष्पादित करने पर भी काम होता है। उदाहरण हैं निमशीनित अंग्रेजी का प्रयास,और इंटरनेट बिजनेस लॉजिक,जो शब्दावली या वाक्य-रचना को निमशीनित करने की कोशिश नहीं करते हैं। सिस्टम की एक विशेषता जो द्विदिश अंग्रेजी-तर्क का पता लगाने के साथ-साथ तर्क के प्रत्यक्ष निष्पादन का समर्थन करती है, वह यह है कि उन्हें अपने परिणामों को अंग्रेजी में, व्यवसाय या वैज्ञानिक स्तर पर समझाने के लिए बनाया जा सकता है।

औपचारिक तरीके और संकेतन

विभिन्न प्रकार के औपचारिक तरीके और संकेतन उपलब्ध हैं।

विशिष्टता भाषाएं

मॉडलचेकर्स

संगठन

यह भी देखें

संदर्भ

  1. ↑ Butler, R. W. (2001-08-06). "What is Formal Methods?". Retrieved 2006-11-16.
  2. ↑ Holloway, C. Michael. "Why Engineers Should Consider Formal Methods" (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). Archived from the original (PDF) on 16 November 2006. Retrieved 2006-11-16. {{cite journal}}: Cite journal requires |journal= (help)
  3. ↑ Monin, pp.3-4
  4. ↑ X2R-2, deliverable D5.1.
  5. ↑ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996
  6. ↑ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering" Archived 2006-03-01 at the Wayback Machine, Crosstalk: The Journal of Defense Software Engineering, January 2003
  7. ↑ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290
  8. ↑ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
  9. ↑ Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods" Archived 2006-03-09 at the Wayback Machine, In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998
  10. ↑ Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.
  11. ↑ Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736.
  12. ↑ A. Cortesi and M. Zanioli, Widening and Narrowing Operators for Abstract Interpretation. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, ISSN 1477-8424 (2011).
  13. ↑ Bjørner, Dines; Gram, Christian; Oest, Ole N.; Rystrøm, Leif (2011). "Dansk Datamatik Center". In Impagliazzo, John; Lundin, Per; Wangler, Benkt (eds.). History of Nordic Computing 3: IFIP Advances in Information and Communication Technology. Springer. pp. 350–359.
  14. ↑ Bjørner, Dines; Havelund, Klaus. "40 Years of Formal Methods: Some Obstacles and Some Possibilities?". FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings (PDF). Springer. pp. 42–61.
  15. ↑ Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.
  16. ↑ Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/
  17. ↑ "Atelier B". www.atelierb.eu (in English).
  18. ↑ C. T. Chou, P. K. Mannava, S. Park, “A simple method for parameterized verification of cache coherence protocols”, Formal Methods in Computer-Aided Design, pp. 382–398, 2004.
  19. ↑ Formal Verification in Intel® Core™ i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371, accessed at Sep. 13, 2013.
  20. ↑ J. Grundy, “Verified optimizations for the Intel IA-64 architecture”, In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.
  21. ↑ E. Seligman, I. Yarom, “Best known methods for using Cadence Conformal LEC”, at Intel.
  22. ↑ C. Eisner, A. Nahir, K. Yorav, “Functional verification of power gated designs by compositional reasoning”, Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.
  23. ↑ P. C. Attie, H. Chockler, “Automatic verification of fault-tolerant register emulations”, Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.
  24. ↑ K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, “Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems”, IBM Journal of Research and Development, vol. 55, no 3.
  25. ↑ "ESBMC". esbmc.org.

अग्रिम पठन


बाहरी संबंध

Archival material
Retrieved from ‘https://www.vigyanwiki.in/index.php?title=औपचारिक_पद्यतियां&oldid=257700’