प्रोग्रामिंग कोडिंग से अधिक है

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

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

हब्रोकट के बाद, वास्तव में, संगोष्ठी का अनुवाद शुरू होता है। अच्छा पढ़ लो!

आप जो भी कार्य करते हैं, आपको हमेशा तीन चरणों से गुजरना पड़ता है:

• तय करें कि आप किस लक्ष्य को प्राप्त करना चाहते हैं;
• तय करें कि आप अपने लक्ष्य को कैसे प्राप्त करेंगे;
• अपने लक्ष्य पर आओ।

यह प्रोग्रामिंग पर भी लागू होता है। जब हम कोड लिखते हैं, तो हमें आवश्यकता होती है:

• तय करें कि कार्यक्रम क्या करना चाहिए;
• यह निर्धारित करें कि यह अपने कार्य को कैसे पूरा करे;
• उपयुक्त कोड लिखें।

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

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

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

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

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

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

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

आइए हम पहले चरण में अधिक विस्तार से विचार करें: कार्यक्रम क्या समस्या हल करता है। यहां हम अक्सर एक प्रोग्राम को एक फ़ंक्शन के रूप में मॉडल करते हैं जो कुछ इनपुट प्राप्त करता है और कुछ आउटपुट देता है। गणित में, एक फ़ंक्शन को आमतौर पर जोड़े के एक निर्धारित सेट के रूप में वर्णित किया जाता है। उदाहरण के लिए, प्राकृतिक संख्याओं के लिए स्क्वेरिंग फ़ंक्शन को सेट {<0,0>, <1,1>, <2,4>, <3,9>, ...} के रूप में वर्णित किया गया है। इस तरह के फ़ंक्शन का दायरा प्रत्येक जोड़ी के पहले तत्वों का सेट है, अर्थात, प्राकृतिक संख्याएं। किसी फ़ंक्शन को परिभाषित करने के लिए, हमें इसके दायरे और सूत्र को निर्दिष्ट करने की आवश्यकता है।

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

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

आइए देखें कि यूक्लिडियन एल्गोरिथ्म के लिए दूसरा कदम क्या दिखेगा। हमें GCD(M, N) गणना करने की आवश्यकता है। हम M को x , और N को y रूप में आरंभीकृत करते हैं, फिर इन चरों के छोटे को बड़े से फिर से घटाते हैं जब तक कि वे समान न हों। उदाहरण के लिए, यदि M = 12 , और N = 18 , हम निम्नलिखित व्यवहार का वर्णन कर सकते हैं:

[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]

और अगर M = 0 और N = 0 ? शून्य सभी संख्याओं से विभाज्य है, इसलिए इस मामले में कोई सबसे बड़ा विभाजक नहीं है। इस स्थिति में, हमें पहले चरण पर लौटने और पूछने की आवश्यकता है: क्या हमें वास्तव में गैर-सकारात्मक संख्याओं के लिए जीसीडी की गणना करने की आवश्यकता है? यदि यह आवश्यक नहीं है, तो आपको केवल विनिर्देश बदलने की आवश्यकता है।

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

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

हम पहले से ही, कई संभावित प्रारंभिक राज्यों को निर्धारित करके सुरक्षा प्राप्त करते हैं। और दूसरी बात, प्रत्येक राज्य के लिए सभी संभव अगले राज्यों के साथ संबंध। हम वैज्ञानिकों के रूप में व्यवहार करेंगे और राज्यों को गणितीय रूप से परिभाषित करेंगे। प्रारंभिक अवस्थाओं के सेट को सूत्र द्वारा वर्णित किया गया है, उदाहरण के लिए, यूक्लिडियन एल्गोरिथ्म के मामले में: (x = M) ∧ (y = N) । M और N के कुछ मूल्यों के लिए N केवल एक प्रारंभिक अवस्था है। अगले राज्य के साथ संबंध एक सूत्र द्वारा वर्णित है जिसमें अगले राज्य के चर को डैश के साथ लिखा गया है, और वर्तमान स्थिति को बिना डैश के। यूक्लिडियन एल्गोरिथ्म के मामले में, हम दो फ़ार्मुलों के निपटान से निपटेंगे, जिनमें से एक में x सबसे बड़ा मूल्य है, और दूसरे में - y :

पहले मामले में, y का नया मान, y के पिछले मान के बराबर है, और हमें x का नया मान मिलता है, जो बड़े चर से छोटे को घटाता है। दूसरे मामले में, हम इसके विपरीत करते हैं।

आइए यूक्लिडियन एल्गोरिथ्म पर वापस जाएं। फिर से मान लीजिए कि M = 12 , N = 18 । यह एकमात्र प्रारंभिक स्थिति निर्धारित करता है, (x = 12) ∧ (y = 18) initial (x = 12) ∧ (y = 18) । फिर हम ऊपर दिए गए सूत्र में इन मूल्यों को प्रतिस्थापित करते हैं और प्राप्त करते हैं:

यहां एकमात्र संभव समाधान है: x' = 18 - 12 ∧ y' = 12 , और हमें व्यवहार मिलता है: [x = 12, y = 18] । उसी तरह, हम अपने व्यवहार में सभी राज्यों का वर्णन कर सकते हैं: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6] ।

अंतिम अवस्था [x = 6, y = 6] अभिव्यक्ति के दोनों भाग झूठे होंगे, इसलिए, इसकी कोई अगली अवस्था नहीं है। इसलिए, हमारे पास दूसरे चरण का पूरा विनिर्देश है - जैसा कि हम देखते हैं, यह काफी सामान्य गणित है, जैसे इंजीनियरों और वैज्ञानिकों का, और अजीब नहीं, कंप्यूटर विज्ञान की तरह।

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

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

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

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

जैसा कि आप देख सकते हैं, कुछ भी जटिल नहीं है। TLA + के लिए विनिर्देशन की जाँच की जा सकती है, अर्थात्, एक छोटे मॉडल में सभी संभावित व्यवहारों को बायपास करें। हमारे मामले में, यह मॉडल M और N कुछ मूल्य होंगे N यह एक बहुत ही कुशल और आसान सत्यापन विधि है जो पूरी तरह से स्वचालित रूप से चलती है। इसके अलावा, आप सत्य के औपचारिक प्रमाण लिख सकते हैं और उन्हें यंत्रवत् सत्यापित कर सकते हैं, लेकिन इसमें बहुत समय लगता है, इसलिए लगभग कोई भी ऐसा नहीं करता है।

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

शायद किसी को आपत्ति होगी कि TLA + और PlusCal गणित हैं, और गणित केवल आविष्कृत उदाहरणों पर काम करता है। व्यवहार में, आपको एक वास्तविक भाषा की आवश्यकता होती है जिसमें प्रकार, प्रक्रियाएं, वस्तुएं, और इसी तरह की अन्य चीजें होती हैं। ऐसा नहीं है। यहाँ अमेज़न पर काम करने वाले क्रिस न्यूकॉम्ब ने लिखा है: "हमने दस बड़ी परियोजनाओं में टीएलए + का उपयोग किया, और प्रत्येक मामले में, इसके उपयोग ने विकास में महत्वपूर्ण योगदान दिया, क्योंकि हम उत्पादन में आने से पहले खतरनाक कीड़े पकड़ने में सक्षम थे, और क्योंकि हमने हमें दिया था।" आक्रामक प्रदर्शन अनुकूलन के लिए समझ और विश्वास आवश्यक है जो कार्यक्रम की सच्चाई को प्रभावित नहीं करते हैं । ” आप अक्सर सुन सकते हैं कि औपचारिक तरीकों का उपयोग करते समय, हमें एक अक्षम कोड मिलता है - व्यवहार में, सब कुछ बिल्कुल विपरीत है। इसके अलावा, यह माना जाता है कि प्रबंधकों को औपचारिक तरीकों की आवश्यकता के बारे में आश्वस्त नहीं किया जा सकता है, भले ही प्रोग्रामर उनकी उपयोगिता के बारे में आश्वस्त हों। और न्यूकॉम्ब लिखते हैं: "प्रबंधक अब हर तरह से टीएलए + के लिए विनिर्देशों को लिखने के लिए जोर दे रहे हैं, और वे विशेष रूप से इस समय के लिए समर्पित हैं । " इसलिए जब प्रबंधक देखते हैं कि टीएलए + काम कर रहा है, तो वे इसे स्वीकार करके खुश हैं। क्रिस न्यूकॉम्ब ने इसे लगभग छह महीने पहले (अक्टूबर 2014 में) लिखा था, लेकिन अब, जहां तक ​​मुझे पता है, टीएलए + का इस्तेमाल 14 परियोजनाओं में किया जाता है, न कि 10. एक्सबॉक्स 360 के डिजाइन से संबंधित एक और उदाहरण। चार्ल्स थैकर के लिए एक इंटर्न आया था और लिखा था एक मेमोरी सिस्टम के लिए विनिर्देश। इस विनिर्देश के लिए धन्यवाद, एक बग पाया गया जो अन्यथा नहीं देखा गया होगा, और जिसके कारण प्रत्येक XBox 360 चार घंटे के उपयोग के बाद गिर जाएगा। आईबीएम इंजीनियरों ने पुष्टि की है कि उनके परीक्षणों ने इस बग का पता नहीं लगाया होगा।

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

लेकिन उपर्युक्त उदाहरण में, उपयोगकर्ता सबसे अधिक संयोजन और समान संकेतों को संरेखित करना चाहता था। तो सही स्वरूपण इस तरह दिखाई देगा:

एक अन्य उदाहरण पर विचार करें:

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

ऐसा लगता है कि अगर हमारे पास सत्य की परिभाषा नहीं है, तो विनिर्देश बेकार है। लेकिन ऐसा है नहीं। अगर हमें ठीक से पता नहीं है कि कार्यक्रम क्या करना चाहिए, इसका मतलब यह नहीं है कि हमें इसके काम के माध्यम से सोचने की आवश्यकता नहीं है - इसके विपरीत, हमें इस पर और भी अधिक प्रयास करना चाहिए। यहां विनिर्देश विशेष रूप से महत्वपूर्ण है। संरचनात्मक लिस्टिंग के लिए इष्टतम कार्यक्रम निर्धारित करना असंभव है, लेकिन इसका मतलब यह नहीं है कि हमें इसे बिल्कुल भी नहीं शुरू करना चाहिए, और चेतना की एक धारा के रूप में कोड लिखना कोई बात नहीं है। अंत में, मैंने जावा फ़ाइल में टिप्पणियों के रूप में परिभाषाओं के साथ छह नियमों का एक विनिर्देश लिखा। यहां नियमों में से एक का उदाहरण a left-comment token is LeftComment aligned with its covering token गया है: a left-comment token is LeftComment aligned with its covering token । यह नियम, गणितीय अंग्रेजी में लिखा गया है: LeftComment aligned , left-comment और covering token परिभाषाओं के साथ हैं। इस तरह से गणितज्ञ गणित का वर्णन करते हैं: वे शर्तों की परिभाषा लिखते हैं और उनके आधार पर - नियम। इस विनिर्देश का लाभ यह है कि छह नियमों की समझ और डिबगिंग कोड की 850 लाइनों की तुलना में बहुत सरल है। मुझे कहना होगा कि इन नियमों को लिखना आसान नहीं था, उन्हें डिबग करने में काफी समय खर्च किया गया था। विशेष रूप से इस उद्देश्य के लिए, मैंने कोड लिखा था जिसमें बताया गया था कि किस नियम का उपयोग किया गया था। इस तथ्य के कारण कि मैंने इन छह नियमों को कुछ उदाहरणों के साथ जांचा, मुझे कोड की 850 लाइनों को डीबग करने की आवश्यकता नहीं थी, और बग को पता लगाने में काफी आसान हो गया। जावा के पास इसके लिए कुछ बेहतरीन उपकरण हैं। अगर मैं सिर्फ कोड लिखता हूं, तो मुझे अधिक समय लगेगा और स्वरूपण बदतर गुणवत्ता का होगा।

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

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

लेकिन इस विनिर्देशन में ऐसी विशेषताएं भी हैं जो इसे अन्य विशिष्टताओं से अलग करती हैं। 95% अन्य विनिर्देश बहुत छोटे और सरल हैं:

इसके अलावा, यह विनिर्देश नियमों का एक समूह है। यह आमतौर पर खराब विनिर्देशन का संकेत है। नियमों के एक सेट के परिणामों को समझना काफी कठिन है, और इसीलिए मुझे उन्हें डिबग करने में काफी समय देना पड़ा। हालाँकि, इस मामले में मुझे इससे बेहतर तरीका नहीं मिला।

यह उन कार्यक्रमों के बारे में कुछ शब्द कहने के लायक है जो लगातार काम करते हैं। एक नियम के रूप में, वे समानांतर में काम करते हैं, उदाहरण के लिए, ऑपरेटिंग सिस्टम या वितरित सिस्टम। बहुत कम लोग उन्हें अपने दिमाग में या कागज पर समझ सकते हैं, और मैं उनमें से नहीं हूं, हालांकि मैं एक बार इसे खरीद सकता था। इसलिए, ऐसे उपकरणों की आवश्यकता होती है जो हमारे काम का परीक्षण करेंगे - उदाहरण के लिए, टीएलए + या प्लसकाल।

यदि आपको पहले से ही पता था कि कोड क्या करना चाहिए तो आपको एक विनिर्देश लिखने की आवश्यकता क्यों है? वास्तव में, यह केवल मुझे लग रहा था कि मैं इसे जानता था। इसके अलावा, यदि कोई विनिर्देश है, तो एक बाहरी व्यक्ति को अब यह समझने के लिए कोड में आने की आवश्यकता नहीं है कि वह क्या कर रहा है। मेरा एक नियम है: कोई सामान्य नियम नहीं होना चाहिए। यह नियम, निश्चित रूप से, एक अपवाद है, यह एकमात्र सामान्य नियम है जिसका मैं पालन करता हूं: इस कोड का उपयोग करते समय लोगों को वे सब कुछ बताने के लिए जो उन्हें जानना आवश्यक है, उसका विनिर्देश।

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

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

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

, . , , . , . . , , . , . , .

— . — Amazon. . ? . , , . , . — , . . .

. - , , . , - , , . . , . , , . , ? -, , , , . , . , . , , . -, , . . , , .

, , . - . , — . , , . , , , , . . , . , , — . , .

TLA+ PlusCal , . , .

, . — , . , Hydra 2019, 11-12 2019 -. .