सॉफ्टवेयर इंजीनियरिंग स्टैक एक्सचेंज में, मैंने इस प्रश्न को देखा: "औपचारिक तरीकों को व्यापक रूप से अपनाने से क्या रोक रहा है?" प्रश्न पक्षपाती के रूप में बंद कर दिया गया था, और अधिकांश जवाब "बहुत महंगा !!!" जैसी टिप्पणियां थीं। या "एक साइट एक विमान नहीं है !!!" एक तरह से, यह सच है, लेकिन यह बहुत स्पष्ट नहीं करता है। मैंने औपचारिक तरीकों (एफएम) की एक व्यापक ऐतिहासिक तस्वीर देने के लिए यह लेख लिखा था, कि वे वास्तव में उपयोग क्यों नहीं किए जाते हैं, और हम स्थिति को सही करने के लिए क्या कर रहे हैं।

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

स्पष्टता के लिए, हम सत्यापन को कोड सत्यापन (CV) और डिज़ाइन सत्यापन (DV) में विभाजित करेंगे और उसी तरह CS और DS में विनिर्देशों को विभाजित करेंगे। इस तरह के शब्दों का आमतौर पर व्यापक एफएम समुदाय में उपयोग नहीं किया जाता है। चलो सीएस और सीवी से शुरू करते हैं, फिर डीएस और डीवी पर आगे बढ़ते हैं।

इसके अलावा, आंशिक सत्यापन संभव है, जहां केवल विनिर्देशन का सबसेट चेक किया गया है, या पूर्ण सत्यापन है । यह आरोपों के प्रमाण के बीच अंतर हो सकता है "सिस्टम कभी भी क्रैश नहीं करता है और गलत पासवर्ड को स्वीकार नहीं करता है" या "सिस्टम कभी भी क्रैश नहीं करता है और यदि आप तीन बार गलत पासवर्ड दर्ज करते हैं तो खाता लॉक हो जाता है"। मूल रूप से, हम मान लेंगे कि हम पूरी जाँच कर रहे हैं।

आपको उस सॉफ़्टवेयर के प्रकार को भी स्पष्ट करना चाहिए जिसे हम औपचारिक रूप दे रहे हैं। अधिकांश लोग स्पष्ट रूप से चिकित्सा उपकरणों और हवाई जहाज जैसे अत्यधिक विश्वसनीय कार्यक्रमों की पहचान करते हैं। लोग मानते हैं कि औपचारिक तरीके उनके लिए व्यापक रूप से उपयोग किए जाते हैं, लेकिन उन्हें बाकी के लिए आवश्यक नहीं है। यह बहुत आशावादी है : अधिकांश अत्यधिक विश्वसनीय सॉफ्टवेयर औपचारिक तरीकों का उपयोग नहीं करते हैं। इसके बजाय, हम "नियमित" सॉफ्टवेयर पर ध्यान केंद्रित करेंगे।

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

औपचारिक प्रोग्रामिंग

विनिर्देशन प्राप्त करना

कोड की शुद्धता साबित करने से पहले, आपको सच्चाई का मानक प्राप्त करने की आवश्यकता है। इसका अर्थ है कि कोड क्या करना चाहिए, इसके कुछ विनिर्देश । हमें निश्चित रूप से पता होना चाहिए कि परिणाम विनिर्देश से मेल खाता है। यह कहना पर्याप्त नहीं है कि सूची "क्रमबद्ध" है: हम नहीं जानते कि हम क्या छाँट रहे हैं, हम किन मानदंडों का उपयोग करते हैं और यहां तक ​​कि "छँटाई" से हमारा क्या मतलब है। इसके बजाय, हम कह सकते हैं: "पूर्णांक l की सूची किसी भी दो सूचकांकों i और j के लिए आरोही क्रम में क्रमबद्ध है , अगर i < j , तो l[i] <= l[j] ।"

कोड विनिर्देशों को तीन मुख्य प्रकारों में विभाजित किया गया है:

1. पहला कोड-इंडिपेंडेंट स्टेटमेंट लिखना है। हम अपना छँटाई कार्य लिखते हैं, और एक अलग फाइल में हम प्रमेय लिखते हैं "यह रिटर्न क्रमबद्ध सूची"। यह विनिर्देशन का सबसे पुराना रूप है, लेकिन इसाबेल और एसीएल 2 अभी भी इस तरह से काम करते हैं (एमएल को विशेष रूप से ऐसे विनिर्देशों को लिखने में मदद करने के लिए आविष्कार किया गया था)।
   
2. दूसरा कोड में पूर्व और पोस्टकंडिशन, स्टेटमेंट और इनवेरिएंट के रूप में विनिर्देशों को लागू करता है। आप फ़ंक्शन में एक पोस्टकंडिशन जोड़ सकते हैं कि "वापसी मूल्य एक सॉर्ट की गई सूची है।" दावा-आधारित विशिष्टताओं को शुरुआत में होर के तर्क के रूप में औपचारिक रूप दिया गया था। वे पहली बार 1970 के दशक की शुरुआत में यूक्लिड प्रोग्रामिंग भाषा में दिखाई दिए (यह स्पष्ट नहीं है कि पहली बार उनका उपयोग किसने किया: यूक्लिड या एसपीवी , लेकिन जहां तक ​​मुझे पता है, यूक्लिड को पहले जनता के लिए पेश किया गया था)। इस शैली को अनुबंध प्रोग्रामिंग भी कहा जाता है - आधुनिक उद्योग में सत्यापन का सबसे लोकप्रिय रूप (यहां, अनुबंध कोड विनिर्देशों के रूप में उपयोग किए जाते हैं)।
   
3. अंत में, टाइप सिस्टम हैं। करी द्वारा - हावर्ड पत्राचार, किसी भी गणितीय प्रमेय या प्रमाण को आश्रित प्रकार के रूप में एन्कोड किया जा सकता है। हम सॉर्ट की गई सूचियों को परिभाषित करेंगे और फ़ंक्शन के लिए [Int] -> Sorted [Int] प्रकार की घोषणा करेंगे।

लेट्स प्रूव लेफ्टपैड पर, आप देख सकते हैं कि यह कैसा दिखता है। HOL4 और इसाबेल "स्वतंत्र प्रमेय" की विशिष्टताओं के अच्छे उदाहरण हैं, स्पार्क और डैनी "नेस्टेड स्टेटमेंट" के विनिर्देश हैं, और कॉक और एजडा "आश्रित प्रकार" हैं।

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

कौन से विनिर्देश सही हैं?

सत्यापन यह पुष्टि करता है कि कोड विनिर्देश के अनुरूप है। सवाल उठता है: हम कैसे जानते हैं कि हमारे पास सही विनिर्देश हैं? सही विनिर्देश ढूंढना औपचारिक तरीकों में सबसे बड़ी समस्याओं में से एक है। यह उनके लिए मुख्य आपत्तियों में से एक है। लेकिन यहां संशय का मतलब यह नहीं है कि औपचारिक विशेषज्ञों के दिमाग में क्या है।

जब बाहरी लोग पूछते हैं, "आपको सही विनिर्देश कैसे मिलते हैं?" वे आमतौर पर सत्यापन के बारे में सोचते हैं, अर्थात् , ऐसे विनिर्देश जो ग्राहक की आवश्यकताओं को पूरा नहीं करते हैं। यदि आप औपचारिक रूप से साबित करते हैं कि आपका कोड सूची को क्रमबद्ध करता है, और ग्राहक वास्तव में Uber for soups (tm) चाहता है, तो आपने बस एक टन का समय बिताया है। जैसे, केवल तेज़ पुनरावृत्तियों और लघु प्रतिक्रिया छोरों से आपकी आवश्यकताओं की पुष्टि हो सकती है।

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

सही विनिर्देश खोजने की समस्या अधिक मौलिक है: हम अक्सर नहीं जानते कि वहाँ क्या लिखना है । हम मानव में अपनी आवश्यकताओं के बारे में सोचते हैं, गणितीय के बारे में नहीं। अगर मैं कहता हूं: "कार्यक्रम को पक्षियों से पेड़ों को अलग करना चाहिए," तो इसके बारे में क्या है? मैं इसे पेड़ों और पक्षियों के चित्रों का एक गुच्छा दिखाकर किसी व्यक्ति को समझा सकता हूं, लेकिन ये केवल ठोस उदाहरण हैं, विचार का विवरण नहीं। वास्तव में, इसे औपचारिक विनिर्देश में अनुवाद करने के लिए, मानवीय अवधारणाओं को औपचारिक रूप देना आवश्यक है, और यह एक गंभीर समस्या है।

मुझे गलत मत समझो। प्रासंगिक विनिर्देशों को यहां परिभाषित किया जा सकता है, और विशेषज्ञ हर समय ऐसा करते हैं। लेकिन उपयुक्त विशिष्टताओं को लिखना एक कौशल है जिसे विकसित करने की आवश्यकता है, साथ ही साथ प्रोग्रामिंग कौशल भी। यही कारण है कि कोड सत्यापन की हालिया सफलताओं में से कई को स्पष्ट मानचित्रण द्वारा समझाया गया है कि हम क्या व्यक्त कर सकते हैं। उदाहरण के लिए, CompCert एक औपचारिक रूप से सत्यापित सी कंपाइलर है। इसके लिए विनिर्देशन है: "संकलन त्रुटियों से बचें"।

लेकिन इन सबका सत्यापन से कोई लेना-देना नहीं है। जब आपके पास एक विनिर्देश होता है, तो आपको अभी भी यह साबित करना होगा कि कोड इसे मेल खाता है।

विनिर्देशन का प्रमाण

पहली बार कोड सत्यापन उपकरण है दिक्जस्त्र-शैली "इस बारे में सोचें कि यह क्यों सच है" विधि है, जो मुख्य रूप से ALGOL के लिए है। उदाहरण के लिए, मैं सम्मिलित विधि द्वारा छँटाई की शुद्धता को "सिद्ध" कर सकता हूँ:

1. मूल विकल्प : यदि आप खाली सूची में एक तत्व जोड़ते हैं, तो यह एकमात्र तत्व होगा, इसलिए इसे सॉर्ट किया जाएगा।
   
2. यदि हमारे पास k तत्वों के साथ एक क्रमबद्ध सूची है और एक तत्व जोड़ते हैं, तो हम तत्व को सम्मिलित करते हैं ताकि यह सभी छोटी संख्याओं के बाद और सभी बड़ी संख्याओं से पहले हो। इसका मतलब सूची अभी भी क्रमबद्ध है।
   
3. प्रेरण से, प्रविष्टि सॉर्टिंग पूरी सूची को सॉर्ट करेगी।

जाहिर है, वास्तव में, प्रमाण अधिक कठोर दिखाई देगा, लेकिन यह एक सामान्य विचार है। डीजकस्ट्रा और अन्य लोगों ने इस शैली का उपयोग कई एल्गोरिदम की शुद्धता को साबित करने के लिए किया, जिसमें कई संगणक की मूल बातें भी शामिल हैं। यह वह शैली भी है जिसके साथ नथ के शब्द जुड़े हुए हैं: “इस कोड में त्रुटियों से सावधान रहें; मैंने केवल यह साबित किया कि यह सही था, लेकिन इसे शुरू नहीं किया। ” आप आसानी से एक गणितीय प्रमाण को बर्बाद कर सकते हैं ताकि कोई भी नोटिस न करे। कुछ अनुमानों के अनुसार , लगभग 20% प्रकाशित गणितीय प्रमाणों में त्रुटियां हैं। पीटर गुटमैन के पास एक हास्यास्पद कार्यक्रम के स्वास्थ्य के साक्ष्य पर एक उत्कृष्ट निबंध है, जहां "परीक्षण" कोड के टन तुरंत गिर जाते हैं यदि आप उन्हें चलाते हैं।

उसी समय, हमने गणितीय प्रमेयों को स्वतः सिद्ध करने के तरीकों का अध्ययन किया। प्रमेयों को सिद्ध करने वाला पहला कार्यक्रम 1967 में प्रकाशित हुआ था। 1970 के दशक की शुरुआत में, पास्कल कोड का परीक्षण करने के लिए इस तरह के कार्यक्रमों का इस्तेमाल किया जाने लगा और दशक के मध्य में विशेष औपचारिक भाषाएं सामने आईं। प्रोग्रामर कोड के कुछ गुणों का निर्माण करता है, और फिर यह पुष्टि करता है कि कोड में ये गुण हैं। प्रमेय साबित करने के लिए पहले कार्यक्रमों ने लोगों को बस साक्ष्यों को सत्यापित करने में मदद की, जबकि अधिक परिष्कृत उपकरण स्वतंत्र रूप से प्रमेय के कुछ हिस्सों को साबित कर सकते थे।

जिससे निम्न समस्या हो जाती है।

साक्ष्य मिलना मुश्किल है

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

एक ही प्रविष्टि सॉर्टिंग उदाहरण लें जहां हमने इंडक्शन लागू किया था। कोई भी गणितज्ञ तुरंत समझ जाएगा कि प्रेरण क्या है, यह सामान्य रूप से कैसे काम करता है, और इस मामले में यह कैसे काम करता है। लेकिन प्रमेयों को साबित करने के लिए कार्यक्रम में सब कुछ सख्ती से औपचारिक रूप देने की आवश्यकता है। विरोधाभास से प्रमाण के साथ भी यही सच है, प्रतिवाद के माध्यम से प्रमाण, आदि इसके अलावा, सभी मान्यताओं को औपचारिक रूप दिया जाना चाहिए, यहां तक ​​कि जहां अधिकांश गणितज्ञ प्रमाण के साथ परेशान नहीं करते हैं। उदाहरण के लिए, a + (b + c) = (a + b) + c । प्रमेय की जाँच करने का कार्यक्रम एक प्राथमिकता को नहीं जानता है कि यह सच है। आपको या तो इसे (मुश्किल) साबित करना होगा, या इसके अलावा (खतरनाक) के साहचर्य कानून के अनुसार इसे सत्य घोषित करना होगा, या किसी ऐसे व्यक्ति से प्रमेय का पुस्तकालय खरीदना होगा जो पहले से ही इसे (महंगा) साबित करने में सक्षम हो। प्रारंभिक प्रमेय साबित करने वाले कार्यक्रम अंतर्निहित प्रमाण रणनीति और संबंधित प्रमेय पुस्तकालयों की संख्या में प्रतिस्पर्धा करते हैं। पहले व्यापक स्प्रेड कार्यक्रमों में से एक ने मुख्य लाभ के रूप में पूर्ण अंकगणित पुस्तकालय प्रस्तुत किया।

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

• गणित;
  
• कंप्यूटर विज्ञान;
  
• वह क्षेत्र जिसमें आप काम करते हैं: संकलक, हार्डवेयर, आदि;
  
• अपने कार्यक्रम और विशेषज्ञता की बारीकियों;
  
• आपके द्वारा उपयोग किए जाने वाले प्रमेयों को साबित करने के लिए कार्यक्रम की बारीकियां, जो अपने आप में एक संपूर्ण विशेषता है।

इससे भी बदतर, कंप्यूटर-विशिष्ट छड़ें पहियों में लगाई जाती हैं। याद रखें, मैंने कहा कि इसके अलावा एक साहचर्य कानून को मानना ​​खतरनाक था? कुछ भाषाएं इसका अनुपालन नहीं करती हैं। उदाहरण के लिए, C ++ INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. ((-1) + INT_MAX) + 1 INT_MAX. -1 + (INT_MAX + 1) INT_MAX. -1 + (INT_MAX + 1) , जो कि undetectable है। C ++ में साहचर्य जोड़ को मानते हुए, आपका प्रमाण गलत होगा, और कोड टूट जाएगा। आपको इस कथन से बचना चाहिए या यह साबित करना चाहिए कि आपके विशेष अंश के लिए अतिप्रवाह कभी नहीं होगा।

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

 a = true; b = false; f(a); assert a; 

क्या हमेशा ऐसा ही होता है? एक तथ्य नहीं। शायद f बदल जाएगा। शायद यह समानांतर प्रवाह को बदल देगा। शायद b एक अन्य नाम b a , इसलिए इसे बदलने से a भी बदल जाएगा (नोट: उपनामों को साक्ष्य लिखना इतना मुश्किल हो जाता है कि जॉन सी। रेनॉल्ड्स को इस समस्या से निपटने के लिए एक पूरी तरह से नया जुदाई तर्क तैयार करना पड़ा)। यदि आपकी भाषा में ऐसा कुछ संभव है, तो आपको स्पष्ट रूप से साबित करना चाहिए कि यहां ऐसा नहीं होता है। स्वच्छ कोड यहां मदद करेगा, एक अन्य मामले में, यह सबूत को नष्ट कर सकता है, क्योंकि यह आपको उच्च क्रम के पुनरावृत्ति और कार्यों का उपयोग करने के लिए मजबूर करता है। वैसे, दोनों अच्छे कार्यात्मक कार्यक्रम लिखने का आधार हैं। प्रोग्रामिंग के लिए जो अच्छा है वह सबूत के लिए बुरा है! (नोट: इस व्याख्यान में, एडमंड क्लार्क ने कुछ गुणों को सूचीबद्ध किया है जिन्हें सत्यापित करना मुश्किल है: "फ्लोटिंग पॉइंट, स्ट्रिंग्स, उपयोगकर्ता-परिभाषित प्रकार, प्रक्रियाएं, संगामिति, सार्वभौमिक टेम्पलेट, भंडारण, पुस्तकालय ...")।

औपचारिक सत्यापनकर्ताओं के पास एक दुविधा है: भाषा जितनी अधिक स्पष्ट है, उतनी ही कठिन बात कुछ साबित करना है। लेकिन भाषा जितनी कम अभिव्यक्त होती है, उस पर लिखना उतना ही मुश्किल होता है। पहले काम करने वाली औपचारिक भाषाएं अधिक अभिव्यंजक भाषाओं के बहुत ही सीमित उपसमुच्चय थे: ACL2 लिस्प का एक उपसमुच्चय था, यूक्लिड पास्कल का एक उपसमुच्चय था, आदि और हमने अब तक जो भी चर्चा की है, उनमें से कोई भी वास्तव में वास्तविक कार्यक्रमों को साबित नहीं करता है, ये सिर्फ दृष्टिकोण का प्रयास है। साक्ष्य लिखना।

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

श्रीमती क्रांति

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

एसएमटी ने एफएम समुदाय को सांस के तहत मारा क्योंकि यह अचानक तुच्छ कई सरल सबूत बना देता है और इसे बहुत जटिल समस्याओं से निपटने की अनुमति देता है। इस प्रकार, लोग अधिक अभिव्यंजक भाषाओं में काम कर सकते थे, क्योंकि अब अभिव्यंजक कथनों की समस्याओं को हल किया जाने लगा। अतुल्य प्रगति IronFleet प्रोजेक्ट में स्पष्ट है: सर्वश्रेष्ठ श्रीमती सॉल्वर और एक उन्नत सत्यापन भाषा का उपयोग करते हुए, Microsoft केवल 3.7 मानव-वर्ष में साबित डैफनी कोड की 5,000 लाइनें लिखने में सक्षम था! यह एक अविश्वसनीय रूप से तेज गति है: प्रति दिन चार पूरी लाइनें (नोट: पिछला रिकॉर्ड seL4 से संबंधित था, जिनमें से डेवलपर्स ने सी में एक दिन में दो लाइनें लिखी थीं।

सबूत मुश्किल है।

इसकी आवश्यकता क्यों है?

यह वापस कदम रखने और पूछने का समय है: "क्या बात है?" हम यह साबित करने की कोशिश कर रहे हैं कि कुछ कार्यक्रम कुछ विनिर्देश पूरा करते हैं। सुधार एक सीमा है। सत्यापन के दो भाग हैं: आपका कार्यक्रम कितना सही "सही" है और आपने कितनी सावधानी से शुद्धता की जाँच की है। जाहिर है, अधिक सत्यापित, बेहतर, लेकिन सत्यापन समय और धन के लायक है। यदि हमारे पास कई प्रतिबंध (प्रदर्शन, बाजार का समय, लागत, आदि) हैं, तो एक पूर्ण सत्यापन आवश्यक रूप से सबसे अच्छा विकल्प नहीं है। फिर सवाल उठता है कि हमें न्यूनतम चेक की क्या आवश्यकता है और इसकी लागत क्या है। ज्यादातर मामलों में, उदाहरण के लिए, 90% या 95% या 99% शुद्धता आपके लिए पर्याप्त है। हो सकता है कि आपको शेष 1% की जाँच करने के बजाय इंटरफ़ेस को सुधारने में समय बिताना चाहिए?

फिर सवाल: "क्या 90/95/99% का चेक 100% से बहुत सस्ता है?" जवाब है हां। यह कहना काफी आरामदायक है कि कोड बेस, जिसे हमने अच्छी तरह से जांचा और टाइप किया है, मूल रूप से उत्पादन में कुछ सुधारों को छोड़कर सही है, और हम प्रति दिन कोड की चार से अधिक लाइनें भी लिखते हैं। वास्तव में, वितरित प्रणालियों में खराबी के विशाल बहुमत को थोड़े अधिक व्यापक परीक्षण के साथ रोका जा सकता था। और यह केवल परीक्षणों का एक विस्तार है, न कि फ़ज़िंग, संपत्ति-आधारित परीक्षण या मॉडल परीक्षण का उल्लेख करना। आप पूर्ण प्रमाण प्राप्त किए बिना इन सरल चालों के साथ वास्तव में उत्कृष्ट परिणाम प्राप्त कर सकते हैं।

यदि टाइपिंग और परीक्षण पर्याप्त सत्यापन प्रदान नहीं करते हैं तो क्या होगा? 99% से 100% की तुलना में 90% से 99% तक स्विच करना अभी भी बहुत आसान है। जैसा कि पहले उल्लेख किया गया है, Cleanroom एक डेवलपर अभ्यास है जिसमें व्यापक प्रलेखन, संपूर्ण प्रवाह विश्लेषण और व्यापक कोड समीक्षाएं शामिल हैं। कोई सबूत नहीं, कोई औपचारिक सत्यापन नहीं, यहां तक ​​कि इकाई परीक्षण भी नहीं। लेकिन एक अच्छी तरह से आयोजित Cleanroom उत्पादन में कोड की प्रति 1000 लाइनों की 1 बग से कम दोषों के घनत्व को कम करता है (ध्यान दें: टॉवर्ड जीरो-डिफेक्ट प्रोग्रामिंग में स्टावले के अध्ययन से आंकड़े> लेकिन हमेशा संदेहपूर्ण रहें और स्रोत की जांच करें )। प्रोग्रामिंग क्लीनरूम विकास की गति को धीमा नहीं करता है, और निश्चित रूप से प्रति दिन 4 लाइनों से अधिक तेज हो जाता है। और Cleanroom ही कई अत्यधिक विश्वसनीय सॉफ्टवेयर विकास विधियों में से एक है जो सामान्य विकास और कोड सत्यापन के बीच में है। अच्छा सॉफ्टवेयर या लगभग सही लिखने के लिए आपको पूर्ण सत्यापन की आवश्यकता नहीं है। ऐसे समय होते हैं जब इसकी आवश्यकता होती है, लेकिन अधिकांश उद्योगों के लिए यह पैसे की बर्बादी है।

हालांकि, इसका मतलब यह नहीं है कि औपचारिक तरीके आमतौर पर अनौपचारिक हैं। पूर्वोक्त अत्यधिक विश्वसनीय तरीकों में से कई कोड विनिर्देशों को लिखने पर आधारित हैं जिन्हें आप औपचारिक रूप से साबित नहीं करते हैं। सत्यापन के संदर्भ में, उद्योग के लाभ के दो सामान्य तरीके हैं। पहले, कोड के बजाय डिजाइन सत्यापन, जिसे हम बाद में चर्चा करेंगे। दूसरे, कोड का आंशिक सत्यापन, जिस पर हम अभी विचार करेंगे।

आंशिक कोड सत्यापन

रोजमर्रा के कामों के लिए, पूरी जाँच करना बहुत महंगा है। आंशिक के बारे में कैसे? आखिरकार, आप व्यक्तिगत कोड के टुकड़े के कुछ गुणों के प्रमाण से लाभ उठा सकते हैं। यह साबित करने के बजाय कि मेरा फ़ंक्शन हमेशा संख्याओं को सही ढंग से क्रमबद्ध करता है, मैं कम से कम यह साबित कर सकता हूं कि यह हमेशा के लिए लूप नहीं करता है और कभी भी सीमा से बाहर नहीं जाता है। यह भी बहुत उपयोगी जानकारी है। इसलिए, यहां तक ​​कि सी कार्यक्रमों के लिए सबसे सरल सबूत अपरिभाषित व्यवहार के एक बड़े हिस्से को खत्म करने का एक शानदार तरीका है ।

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

अधिक बार, कुछ प्रकार के सत्यापन भाषाओं की मूल संरचना में अंतर्निहित होते हैं। उत्पादन में उपयोग किए जाने वाले टंकण प्रणाली एक सामान्य प्रकार है: आप यह नहीं जानते होंगे कि पूंछ हमेशा पूंछ वापस आती है, लेकिन आपको पता है कि इसका प्रकार क्या है [a] -> [a]। अपवाद के साथ सुरक्षा के प्रमाण के साथ रस्ट जैसे साबित स्मृति सुरक्षा और टट्टू जैसे उदाहरण भी हैं। वे स्पार्क और फ्रामा-सी से थोड़ा अलग हैं कि वे केवल आंशिक जांच कर सकते हैं । और वे आमतौर पर प्रोग्रामिंग भाषाओं के विशेषज्ञों द्वारा विकसित किए जाते हैं, न कि औपचारिक तरीकों के विशेषज्ञ: दोनों विषयों के बीच बहुत कुछ समान है, लेकिन वे समान नहीं हैं। शायद यही कारण है कि रस्ट और हास्केल जैसी भाषाएं वास्तव में व्यावहारिक उपयोग के लिए उपयुक्त हैं।

डिजाइन विनिर्देश

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

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

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

• क्या सभी संदेश रिकॉर्ड किए गए हैं या सभी संदेश जो सिस्टम में प्रवेश करते हैं ? संदेशों को एक बार दर्ज किया जाता है या एक बार गारंटी दी जाती है ?
  
• संदेश कैसे भेजे जाते हैं? क्या यह मोड़ है? क्या चैनल उन्हें केवल एक बार डिलीवर करता है? क्या डिलीवरी के साथ सब ठीक है?
  
• ? , ? «» , ?
  
• , ? ?
  
• ? « » ?
  
• GDPR?
  
• .

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

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

संभवतः पहला पूर्ण डीएल 1972 के आसपास वीडीएम था। तब से, हमने विभिन्न विनिर्देशन भाषाओं की एक विशाल विविधता देखी है। कोड सत्यापन भाषाओं (CVL) की तुलना में DL स्थान बहुत अधिक विविध और खंडित है। मोटे तौर पर, लोगों ने डीएल को एक साधन के रूप में और अंत में सीवीएल को एक लक्ष्य के रूप में आविष्कार किया। चूंकि वे विशिष्ट समस्या क्षेत्रों से दृढ़ता से प्रभावित हैं, इसलिए डीएल सभी प्रकार के विचारों और शब्दार्थों को लागू करता है। यहाँ पहले डीएल में से कुछ का बहुत संक्षिप्त विवरण दिया गया है:

भाषा	मॉडलिंग क्षेत्र	माध्यम
जेड	व्यावसायिक आवश्यकताएं	संबंधपरक बीजगणित
Promela		CSP
SDL		-

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

पामेला ज़ेव ने मिश्र धातु के साथ प्रयोग किया और कॉर्ड में एक मूल बग की खोज की , जो मुख्य वितरित हैश तालिकाओं में से एक है। AWS ने 35-चरण वाले महत्वपूर्ण त्रुटियां ढूंढना शुरू कियाटीएलए + विनिर्देशों को लिखकर। मेरे अनुभव में, जब लोग विनिर्देशों को लिखने की कोशिश करते हैं, तो वे बहुत जल्द इस व्यवसाय के बड़े प्रशंसक बन जाते हैं।

लेकिन औपचारिक तरीकों के प्रशंसक और बाहर के लोग पूरी तरह से अलग-अलग लेखन विनिर्देशों के मूल्य का आकलन करते हैं। प्रशंसकों के लिए, सबसे बड़ा फायदा यह है कि डिजाइन प्रक्रिया आपको यह समझने में मदद करती है कि आप क्या लिख ​​रहे हैं। जब आपको औपचारिक रूप से व्यक्त करने की आवश्यकता होती है कि आपका सिस्टम क्या कर रहा है, तो कई अंतर्निहित त्रुटियां अचानक स्पष्ट रूप से स्पष्ट हो जाती हैं। बाहरी लोग इसे बिल्कुल नहीं समझ सकते हैं। यदि आप किसी को एक डीएल देना चाहते हैं, तो एक व्यक्ति के पास यह सत्यापित करने का एक तरीका होना चाहिए कि डिजाइन में वास्तव में वह गुण है जो वह चाहता है।

सौभाग्य से, यह कई बारीकियों के लिए भी बहुत महत्वपूर्ण है, इसलिए डिजाइन सत्यापन अनुसंधान का एक बड़ा क्षेत्र है।

मॉडल की जाँच

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

मॉडल सत्यापन के कई फायदे हैं। सबसे पहले, सबूत लिखने की आवश्यकता नहीं है, जो बहुत समय और प्रयास बचाता है। दूसरी बात, सीखने की कोई जरूरत नहींसबूत लिखें, इसलिए प्रवेश बाधा बहुत कम है। तीसरा, यदि डिज़ाइन टूट गया है, तो मॉडल की जांच करने से एक स्पष्ट प्रतिधारण होगा। यह त्रुटि को ठीक करने के लिए बहुत आसान बनाता है , खासकर अगर यह इसे पुन: पेश करने के लिए 35 कदम लेता है। इसे स्वयं खोजने का प्रयास करें।

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

एक और बड़ा दोष यह है - राज्यों के अंतरिक्ष में विस्फोट (राज्य अंतरिक्ष विस्फोट)। कल्पना करें कि आपके पास तीन प्रक्रियाएं हैं, जिनमें से प्रत्येक में लगातार चार चरण होते हैं, और वे किसी भी तरह से चरणों को वैकल्पिक कर सकते हैं। यदि वे एक-दूसरे के व्यवहार को प्रभावित नहीं करते हैं, तो यह पता चला है(4*3)! / (4!)^3 = 34 650संभव निष्पादन (व्यवहार)। यदि प्रत्येक प्रक्रिया में पांच प्रारंभिक अवस्थाओं में से एक है, तो व्यवहार की कुल संख्या बढ़कर 4,300,000 हो जाती है। और मॉडलों की जाँच करके यह सुनिश्चित करना चाहिए कि वे सभी अच्छा व्यवहार करते हैं। और यह प्रदान किया जाता है कि वे एक-दूसरे के साथ बातचीत नहीं करते हैं! यदि वे ऐसा करना शुरू करते हैं, तो राज्य का स्थान और भी तेजी से बढ़ेगा। एक दहनशील विस्फोट को परीक्षण मॉडल के लिए मुख्य समस्या माना जाता है, और इस समस्या को हल करने के लिए बहुत सारे काम किए जाने बाकी हैं।

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

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

डिजाइन विशिष्टता समस्या

इस प्रकार, डिज़ाइन सत्यापन कोड सत्यापन की तुलना में सरल और तेज़ है, और कई प्रभावशाली सफलताओं का प्रदर्शन किया है। तो लोग इसका इस्तेमाल क्यों नहीं करते? DV के साथ समस्या बहुत अधिक कपटी है। कोड सत्यापन एक तकनीकी समस्या है, और डिज़ाइन सत्यापन एक सामाजिक समस्या है: लोग केवल इस बिंदु को नहीं देखते हैं।

यह काफी हद तक इस तथ्य के कारण है कि डिजाइन कोड नहीं है । अधिकांश डीएल में, कोड बनाने के लिए कोई स्वचालित तरीका नहीं है, न ही मौजूदा कोड को लेने और इसे डिजाइन के खिलाफ जांचने का एक तरीका है (नोट: विनिर्देशों से कोड पीढ़ी को संश्लेषण कहा जाता है ; अभिविन्यास के लिए, नाद्या पोलिकारपोवा का काम देखें ; प्रमाण है कि कोड विनिर्देश से मेल खाता है (या विनिर्देश से मेल खाती है) अन्य विनिर्देशन) कहा जाता हैस्पष्टीकरण : दोनों दिशाओं में सक्रिय अनुसंधान चल रहा है)।

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

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

लेकिन वास्तव में प्रत्येक ऐसी कार्यप्रणाली समुदाय के पास ऐसी शिकायतें हैं जो मुझे पता हैं: TDD समर्थकों की शिकायत है कि प्रोग्रामर TDD की कोशिश नहीं करना चाहते हैं, हास्केल प्रशंसकों की शिकायत है कि प्रोग्रामर स्थिर टाइपिंग के बारे में नहीं सोचते हैं, और इसी तरह।

मैंने तर्क सुना है कि एजाइल पूर्व-तैयार डिज़ाइन को स्वीकार नहीं करता है, इसलिए कोई भी औपचारिक विनिर्देश नहीं बनाना चाहता है। हो सकता है कि।लेकिन जिन लोगों से मैं मिला, उनमें से कई एजाइल और एफएम दोनों को अस्वीकार करते हैं। एक और तर्क यह है कि ऐतिहासिक रूप से औपचारिक तरीकों का लगातार पुनर्मूल्यांकन किया गया था और जो वादा किया गया था उसे पूरा नहीं किया। यह संभव भी है, लेकिन अधिकांश लोगों ने औपचारिक तरीकों के बारे में भी नहीं सुना है , और इससे भी ज्यादा अपने इतिहास के बारे में।

बस लोगों को यह चिंता करना बहुत मुश्किल है कि वे अभी तक क्या नहीं कर रहे हैं, भले ही वे लाभों को पहचानें।

सारांश

कोड को सत्यापित करना एक मुश्किल काम है। अधिक से अधिक लोग शामिल हो रहे हैं, हालांकि प्रमेय साबित करने वाले कार्यक्रम और एसएमटी सॉल्वर अधिक जटिल होते जा रहे हैं। लेकिन अभी भी, निकट भविष्य में, शायद, यह बहुत सारे विशेषज्ञ रहेंगे।

डिजाइन सत्यापन बहुत सरल है, लेकिन इसके उपयोग के लिए सांस्कृतिक बाधा पर काबू पाने की आवश्यकता है। मुझे लगता है कि स्थिति को बदला जा सकता है। बीस साल पहले, स्वचालित परीक्षण और कोड समीक्षा बहुत ही आकर्षक और आला विषय थे, लेकिन अंततः मुख्यधारा बन गए। फिर, अनुबंध प्रोग्रामिंग आला था और ऐसा ही रहता है।

मुझे उम्मीद है कि यह लेख थोड़ा बेहतर बताता है कि औपचारिक तरीकों का उपयोग शायद ही कभी क्यों किया जाता है। कम से कम यह सामान्य तर्क से बेहतर व्याख्या है "वेब एक विमान नहीं है।" यदि आप कोई स्पष्ट गलतियाँ देखते हैं, तो चिल्लाएँ।