प्रोग्रामिंग हे कोडिंगपेक्षा जास्त आहे

हा अनुवाद लेख आहे स्टॅनफोर्ड सेमिनार. पण त्याआधी एक छोटासा परिचय आहे. झोम्बी कसे तयार होतात? प्रत्येकाने स्वतःला अशा परिस्थितीत सापडले आहे जिथे त्यांना मित्र किंवा सहकाऱ्याला त्यांच्या पातळीवर आणायचे आहे, परंतु ते कार्य करत नाही. शिवाय, "हे चालत नाही" आपल्यासाठी इतके नाही, परंतु त्याच्यासाठी: स्केलच्या एका बाजूला सामान्य पगार, कार्ये इत्यादी आहेत आणि दुसरीकडे विचार करण्याची आवश्यकता आहे. विचार करणे अप्रिय आणि वेदनादायक आहे. तो पटकन हार मानतो आणि त्याच्या मेंदूचा अजिबात वापर न करता कोड लिहिणे सुरू ठेवतो. शिकलेल्या असहायतेच्या अडथळ्यावर मात करण्यासाठी किती प्रयत्न करावे लागतात हे तुम्हाला समजते आणि तुम्ही ते करत नाही. अशा प्रकारे झोम्बी तयार होतात, जे बरे करणे शक्य आहे असे दिसते, परंतु असे दिसते की कोणीही हे करणार नाही.

मी ते पाहिले तेव्हा लेस्ली लॅम्पपोर्ट (होय, पाठ्यपुस्तकांतील तोच मित्र) रशियाला येतो आणि अहवाल देत नाही, तर प्रश्नोत्तराच्या सत्रात मी थोडा सावध होतो. फक्त बाबतीत, लेस्ली एक जगप्रसिद्ध शास्त्रज्ञ आहे, वितरीत संगणनात सेमिनल कामांचा लेखक आहे, आणि तुम्ही त्याला LaTeX - “Lamport TeX” मधील La अक्षरांनी देखील ओळखू शकता. दुसरी चिंताजनक बाब म्हणजे त्याची गरज: येणार्‍या प्रत्येकाने (पूर्णपणे विनामूल्य) त्याचे दोन अहवाल आधीच ऐकले पाहिजेत, त्यांच्याबद्दल किमान एक प्रश्न विचारला पाहिजे आणि मगच यावे. मी लॅम्पपोर्ट तिथे काय प्रसारित करत आहे ते पाहण्याचा निर्णय घेतला - आणि ते छान आहे! नेमकी हीच गोष्ट आहे, झोम्बींवर उपचार करण्यासाठी एक जादूची लिंक-गोळी. मी तुम्हाला चेतावणी देतो: ज्यांना अति-चपळ पद्धती आवडतात आणि ज्यांना त्यांनी काय लिहिले आहे ते तपासायला आवडत नाही अशांना मजकूर गंभीरपणे बर्न करू शकतो.

हब्रोकॅटनंतर, परिसंवादाचे भाषांतर प्रत्यक्षात सुरू होते. वाचनाचा आनंद घ्या!

तुम्ही कोणतेही काम कराल, तुम्हाला नेहमी तीन पायऱ्या पार कराव्या लागतात:

• तुम्हाला कोणते ध्येय साध्य करायचे आहे ते ठरवा;
• तुम्ही तुमचे ध्येय नक्की कसे साध्य कराल ते ठरवा;
• आपले ध्येय गाठा.

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

• कार्यक्रम नक्की काय करायचे ते ठरवा;
• त्याचे कार्य कसे करावे ते निश्चित करा;
• योग्य कोड लिहा.

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

कोडचा हा पूर्व-विचार नेमका कसा होतो? यासाठी आपण किती प्रयत्न करावेत? आपण किती जटिल समस्या सोडवत आहोत यावर हे सर्व अवलंबून आहे. समजा आम्हाला दोष-सहिष्णु वितरण प्रणाली लिहायची आहे. या प्रकरणात, कोडवर बसण्यापूर्वी आपण गोष्टींचा काळजीपूर्वक विचार केला पाहिजे. जर आपल्याला पूर्णांक व्हेरिएबल 1 ने वाढवायचे असेल तर? पहिल्या दृष्टीक्षेपात, येथे सर्वकाही क्षुल्लक आहे आणि कोणत्याही विचाराची आवश्यकता नाही, परंतु नंतर आपल्याला आठवते की ओव्हरफ्लो होऊ शकतो. म्हणूनच, एखादी समस्या सोपी आहे की गुंतागुंतीची आहे हे समजून घेण्यासाठी, आपल्याला प्रथम विचार करणे आवश्यक आहे.

एखाद्या समस्येवर संभाव्य उपायांचा आधीच विचार केल्यास, आपण चुका टाळू शकता. पण यासाठी तुमचा विचार स्पष्ट असणे आवश्यक आहे. हे साध्य करण्यासाठी, आपल्याला आपले विचार लिहून ठेवण्याची आवश्यकता आहे. मला डिक गिंडनचा कोट खूप आवडतो: "जेव्हा तुम्ही लिहिता तेव्हा निसर्ग तुम्हाला दाखवतो की तुमची विचारसरणी किती आळशी आहे." जर तुम्ही लिहीत नसाल तर तुम्ही फक्त विचार करत आहात असे तुम्हाला वाटते. आणि तुम्हाला तुमचे विचार स्पेसिफिकेशन्सच्या स्वरूपात लिहावे लागतील.

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

अधिक महत्त्वाचा प्रश्न आहे: आपण स्पष्ट विचार कसे मिळवू शकतो? उत्तर: आपण वैज्ञानिकांप्रमाणे विचार केला पाहिजे. हा विचार करण्याचा एक मार्ग आहे ज्याने गेल्या 500 वर्षांपासून चांगले काम केले आहे. विज्ञानात आपण वास्तवाचे गणिती मॉडेल तयार करतो. खगोलशास्त्र हे कदाचित या शब्दाच्या काटेकोर अर्थाने पहिले विज्ञान होते. खगोलशास्त्रात वापरल्या जाणार्‍या गणितीय मॉडेलमध्ये, खगोलीय पिंड वस्तुमान, स्थिती आणि गती असलेले बिंदू म्हणून दिसतात, जरी प्रत्यक्षात ते पर्वत आणि महासागर, ओहोटी आणि प्रवाह असलेल्या अत्यंत जटिल वस्तू आहेत. हे मॉडेल, इतर कोणत्याही प्रमाणे, काही समस्यांचे निराकरण करण्यासाठी तयार केले गेले होते. जर तुम्हाला एखादा ग्रह शोधायचा असेल तर दुर्बिणी कुठे दाखवायची हे ठरवण्यासाठी हे उत्तम आहे. परंतु जर तुम्हाला या ग्रहावरील हवामानाचा अंदाज घ्यायचा असेल तर हे मॉडेल चालणार नाही.

गणित आपल्याला मॉडेलचे गुणधर्म निर्धारित करण्यास अनुमती देते. आणि हे गुणधर्म वास्तवाशी कसे संबंधित आहेत हे विज्ञान दाखवते. चला आपल्या विज्ञानाबद्दल, संगणक शास्त्राबद्दल बोलूया. आम्ही ज्या वास्तविकतेसह कार्य करतो ती म्हणजे अनेक प्रकारच्या संगणकीय प्रणाली: प्रोसेसर, गेम कन्सोल, प्रोग्राम चालवणारे संगणक आणि असेच. मी संगणकावर प्रोग्राम कार्यान्वित करण्याबद्दल बोलेन, परंतु, मोठ्या प्रमाणात, हे सर्व निष्कर्ष कोणत्याही संगणकीय प्रणालीवर लागू होतात. आमच्या विज्ञानामध्ये आम्ही अनेक भिन्न मॉडेल्स वापरतो: ट्युरिंग मशीन, इव्हेंटचे अंशतः ऑर्डर केलेले संच आणि इतर अनेक.

कार्यक्रम काय आहे? हा कोणताही कोड आहे ज्याचा स्वतःचा विचार केला जाऊ शकतो. समजा आपल्याला ब्राउझर लिहिण्याची गरज आहे. आम्ही तीन कार्ये करतो: वापरकर्त्याच्या प्रोग्रामचे सादरीकरण डिझाइन करा, नंतर प्रोग्रामचा उच्च-स्तरीय आकृती लिहा आणि शेवटी कोड लिहा. जसजसे आपण कोड लिहितो, तसतसे आपल्या लक्षात येते की आपल्याला एक मजकूर फॉरमॅटर लिहिण्याची गरज आहे. येथे पुन्हा आपल्याला तीन समस्यांचे निराकरण करण्याची आवश्यकता आहे: हे साधन कोणता मजकूर परत करेल हे निर्धारित करा; स्वरूपनासाठी अल्गोरिदम निवडा; कोड लिहा. या कार्याचे स्वतःचे उपकार्य आहे: शब्दांमध्ये हायफन योग्यरित्या घालणे. आम्ही हे सबटास्क देखील तीन चरणांमध्ये सोडवतो - जसे आपण पाहतो, ते अनेक स्तरांवर पुनरावृत्ती होते.

चला पहिल्या चरणावर बारकाईने नजर टाकूया: प्रोग्राम कोणत्या समस्येचे निराकरण करतो. येथे आपण बर्‍याचदा प्रोग्रामला फंक्शन म्हणून मॉडेल करतो जे काही इनपुट घेते आणि काही आउटपुट देते. गणितामध्ये, फंक्शनचे वर्णन सहसा जोड्यांचा क्रमबद्ध संच म्हणून केले जाते. उदाहरणार्थ, नैसर्गिक संख्यांसाठी स्क्वेअरिंग फंक्शन {<0,0>, <1,1>, <2,4>, <3,9>, …} संच म्हणून वर्णन केले आहे. अशा फंक्शनच्या व्याख्येचे डोमेन म्हणजे प्रत्येक जोडीच्या पहिल्या घटकांचा संच, म्हणजेच नैसर्गिक संख्या. फंक्शन परिभाषित करण्यासाठी, आपल्याला त्याचे डोमेन आणि सूत्र निर्दिष्ट करणे आवश्यक आहे.

पण गणितातील फंक्शन्स प्रोग्रामिंग लँग्वेजमधील फंक्शन्स सारखी नसतात. गणित जास्त सोपे आहे. माझ्याकडे जटिल उदाहरणांसाठी वेळ नसल्यामुळे, एक साधा विचार करूया: C मधील फंक्शन किंवा Java मधील स्थिर पद्धत जी दोन पूर्णांकांचा सर्वात मोठा सामान्य विभाजक मिळवते. या पद्धतीच्या स्पेसिफिकेशनमध्ये आम्ही लिहू: calculates GCD(M,N) युक्तिवादासाठी M и Nकुठे GCD(M,N) - एक फंक्शन ज्याचे डोमेन पूर्णांकांच्या जोड्यांचा संच आहे आणि परतावा मूल्य सर्वात मोठा पूर्णांक आहे ज्याने भाग घेतला आहे M и N. या मॉडेलशी वास्तवाची तुलना कशी होते? मॉडेल पूर्णांकांसह कार्य करते आणि C किंवा Java मध्ये आमच्याकडे 32-बिट आहे int. हे मॉडेल आम्हाला अल्गोरिदम योग्य आहे की नाही हे ठरवू देते GCD, परंतु ते ओव्हरफ्लो त्रुटींना प्रतिबंध करणार नाही. यासाठी अधिक जटिल मॉडेलची आवश्यकता असेल, ज्यासाठी वेळ नाही.

मॉडेल म्हणून फंक्शनच्या मर्यादांबद्दल बोलूया. काही प्रोग्राम्स (जसे की ऑपरेटिंग सिस्टम) विशिष्ट युक्तिवादांसाठी विशिष्ट मूल्य परत करत नाहीत; ते सतत चालू शकतात. याव्यतिरिक्त, मॉडेल म्हणून कार्य दुस-या टप्प्यासाठी खराबपणे अनुकूल आहे: समस्येचे निराकरण कसे करावे याचे नियोजन. Quicksort आणि बबल सॉर्ट समान फंक्शनची गणना करतात, परंतु ते पूर्णपणे भिन्न अल्गोरिदम आहेत. म्हणून, प्रोग्रामचे ध्येय साध्य करण्याच्या मार्गाचे वर्णन करण्यासाठी, मी दुसरे मॉडेल वापरतो, त्याला मानक वर्तन मॉडेल म्हणूया. प्रोग्राम त्यामध्ये सर्व वैध वर्तनांचा एक संच म्हणून दर्शविला जातो, ज्यापैकी प्रत्येक, यामधून, राज्यांचा एक क्रम आहे आणि राज्य म्हणजे व्हेरिएबल्ससाठी मूल्यांची नियुक्ती.

युक्लिडियन अल्गोरिदमची दुसरी पायरी कशी असेल ते पाहू. आम्हाला गणना करणे आवश्यक आहे 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? शून्याला सर्व संख्यांनी भाग जातो, त्यामुळे या प्रकरणात कोणताही मोठा विभाजक नाही. या परिस्थितीत, आपल्याला पहिल्या चरणावर परत जाणे आवश्यक आहे आणि विचारले पाहिजे: आपल्याला खरोखर गैर-पॉझिटिव्ह संख्यांसाठी GCD ची गणना करण्याची आवश्यकता आहे का? हे आवश्यक नसल्यास, आपल्याला फक्त तपशील बदलण्याची आवश्यकता आहे.

उत्पादनक्षमतेबद्दल एक लहान विषयांतर येथे आहे. हे सहसा दररोज लिहिलेल्या कोडच्या ओळींच्या संख्येत मोजले जाते. परंतु जर तुम्ही ठराविक संख्येच्या ओळींपासून मुक्त झालात तर तुमचे कार्य अधिक उपयुक्त आहे, कारण तुमच्याकडे बगसाठी कमी जागा आहे. आणि कोडपासून मुक्त होण्याचा सर्वात सोपा मार्ग म्हणजे पहिल्या चरणात. हे शक्य आहे की आपण लागू करण्याचा प्रयत्न करत असलेल्या सर्व घंटा आणि शिट्ट्या आवश्यक नाहीत. प्रोग्राम सुलभ करण्याचा आणि वेळ वाचवण्याचा सर्वात जलद मार्ग म्हणजे करू नयेत अशा गोष्टी न करणे. दुसऱ्या पायरीमध्ये दुसऱ्या क्रमांकाची वेळ वाचवण्याची क्षमता आहे. जर तुम्ही लिहीलेल्या ओळींच्या संदर्भात उत्पादकता मोजली, तर एखादे कार्य कसे पूर्ण करायचे याचा विचार कराल कमी उत्पादक, कारण तुम्ही कमी कोडसह समान समस्या सोडवू शकता. मी येथे अचूक आकडेवारी देऊ शकत नाही, कारण माझ्याकडे स्पेसिफिकेशनवर, म्हणजेच पहिल्या आणि दुसर्‍या पायर्‍यांवर घालवलेल्या वेळेमुळे मी न लिहिलेल्या ओळींची संख्या मोजण्याचा कोणताही मार्ग नाही. आणि आम्ही येथे प्रयोग देखील करू शकत नाही, कारण प्रयोगात आम्हाला पहिली पायरी पूर्ण करण्याचा अधिकार नाही; कार्य आधीच निश्चित केले जाते.

अनौपचारिक वैशिष्ट्यांमधील अनेक अडचणींकडे दुर्लक्ष करणे सोपे आहे. फंक्शन्ससाठी कठोर तपशील लिहिण्यात काहीही कठीण नाही; मी याबद्दल चर्चा करणार नाही. त्याऐवजी, आम्ही मानक वर्तनांसाठी मजबूत तपशील लिहिण्याबद्दल बोलू. असे एक प्रमेय आहे जे सांगते की सुरक्षा गुणधर्म वापरून कोणत्याही वर्तनाचे वर्णन केले जाऊ शकते (सुरक्षा) आणि जगण्याची क्षमता (जिवंतपणा). सुरक्षितता म्हणजे काहीही वाईट होणार नाही, कार्यक्रम चुकीचे उत्तर देणार नाही. टिकून राहण्याचा अर्थ असा आहे की लवकरच किंवा नंतर काहीतरी चांगले होईल, म्हणजे कार्यक्रम लवकर किंवा नंतर योग्य उत्तर देईल. नियमानुसार, सुरक्षा हा अधिक महत्त्वाचा सूचक आहे; येथे अनेकदा त्रुटी आढळतात. म्हणून, वेळ वाचवण्यासाठी, मी जगण्याबद्दल बोलणार नाही, जरी ते नक्कीच महत्वाचे आहे.

आम्ही प्रथम संभाव्य प्रारंभिक अवस्थांचा संच निर्दिष्ट करून सुरक्षितता प्राप्त करतो. आणि दुसरे म्हणजे, प्रत्येक राज्यासाठी सर्व संभाव्य पुढील राज्यांशी संबंध. चला शास्त्रज्ञांसारखे वागू आणि गणितीय पद्धतीने राज्यांची व्याख्या करू. प्रारंभिक अवस्थांचा संच सूत्राद्वारे वर्णन केला जातो, उदाहरणार्थ, युक्लिडियन अल्गोरिदमच्या बाबतीत: (x = M) ∧ (y = N). ठराविक मूल्यांसाठी M и N फक्त एक प्रारंभिक अवस्था आहे. पुढील स्थितीशी असलेल्या संबंधाचे वर्णन एका सूत्राद्वारे केले जाते ज्यामध्ये पुढील अवस्थेचे चल अविभाज्य सह लिहिलेले असतात आणि वर्तमान स्थितीचे चल अविभाज्य न लिहिलेले असतात. युक्लिडियन अल्गोरिदमच्या बाबतीत, आपण दोन सूत्रांच्या विघटनाचा सामना करणार आहोत, त्यापैकी एक x सर्वात मोठे मूल्य आहे आणि दुसऱ्यामध्ये - y:

पहिल्या प्रकरणात, y चे नवीन मूल्य y च्या मागील मूल्याच्या बरोबरीचे आहे आणि आपल्याला मोठ्या व्हेरिएबलमधून लहान व्हेरिएबल वजा करून x चे नवीन मूल्य मिळते. दुसऱ्या प्रकरणात, आम्ही उलट करतो.

चला युक्लिडियन अल्गोरिदमकडे परत जाऊया. पुन्हा समजा M = 12, N = 18. हे एकल प्रारंभिक अवस्था परिभाषित करते, (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+. या भाषेतील युक्लिडियन अल्गोरिदमचे तपशील असे दिसेल:

त्रिकोणासह समान चिन्ह चिन्हाचा अर्थ असा आहे की चिन्हाच्या डावीकडील मूल्य चिन्हाच्या उजवीकडील मूल्याच्या समान असल्याचे निर्धारित केले आहे. थोडक्यात, स्पेसिफिकेशन ही एक व्याख्या आहे, आमच्या बाबतीत दोन व्याख्या. TLA+ मधील स्पेसिफिकेशनमध्ये तुम्हाला वरील स्लाइडप्रमाणे घोषणा आणि काही वाक्यरचना जोडणे आवश्यक आहे. ASCII मध्ये हे असे दिसेल:

जसे आपण पाहू शकता, काहीही क्लिष्ट नाही. TLA+ वरील तपशील सत्यापित केले जाऊ शकतात, म्हणजे, लहान मॉडेलमध्ये सर्व संभाव्य वर्तनांना बायपास करणे शक्य आहे. आमच्या बाबतीत, हे मॉडेल विशिष्ट मूल्ये असेल M и N. ही एक अतिशय प्रभावी आणि सोपी पडताळणी पद्धत आहे जी पूर्णपणे स्वयंचलित आहे. याव्यतिरिक्त, सत्याचे औपचारिक पुरावे लिहिणे आणि ते यांत्रिकरित्या तपासणे शक्य आहे, परंतु यास बराच वेळ लागतो, म्हणून जवळजवळ कोणीही असे करत नाही.

TLA+ चा मुख्य तोटा म्हणजे ते गणित आहे आणि प्रोग्रामर आणि संगणक शास्त्रज्ञ गणिताला घाबरतात. पहिल्या दृष्टीक्षेपात हे विनोदासारखे वाटते, परंतु, दुर्दैवाने, मी हे सर्व गांभीर्याने सांगतो. माझा एक सहकारी मला सांगत होता की त्याने अनेक विकासकांना TLA+ कसे समजावून सांगण्याचा प्रयत्न केला. पडद्यावर सूत्रे दिसू लागताच त्यांचे डोळे लगेच काचेच्या बनले. त्यामुळे TLA+ भितीदायक असल्यास, तुम्ही वापरू शकता प्लसकॅल, ही एक प्रकारची खेळण्यांची प्रोग्रामिंग भाषा आहे. PlusCal मधील अभिव्यक्ती कोणतीही TLA+ अभिव्यक्ती असू शकते, म्हणजेच मुळात कोणतीही गणितीय अभिव्यक्ती. याव्यतिरिक्त, PlusCal मध्ये नॉन-डिटरमिनिस्टिक अल्गोरिदमसाठी वाक्यरचना आहे. कारण PlusCal कोणतीही TLA+ अभिव्यक्ती लिहू शकते, ती कोणत्याही वास्तविक प्रोग्रामिंग भाषेपेक्षा लक्षणीयरीत्या अधिक अभिव्यक्त आहे. पुढे, PlusCal वाचण्यास सुलभ TLA+ तपशीलामध्ये संकलित केले आहे. अर्थात, याचा अर्थ असा नाही की जटिल प्लसकॅल तपशील TLA+ वर एक साधे होईल - फक्त त्यांच्यातील पत्रव्यवहार स्पष्ट आहे, कोणतीही अतिरिक्त जटिलता दिसणार नाही. शेवटी, हे तपशील TLA+ टूल्स वापरून सत्यापित केले जाऊ शकतात. सर्वसाधारणपणे, PlusCal गणिताच्या फोबियावर मात करण्यास मदत करू शकते; अगदी प्रोग्रामर आणि संगणक शास्त्रज्ञांनाही समजणे सोपे आहे. भूतकाळात मी त्यावर काही काळ (सुमारे 10 वर्षे) अल्गोरिदम प्रकाशित केले होते.

कदाचित कोणीतरी आक्षेप घेईल की TLA+ आणि PlusCal हे गणित आहेत आणि गणित केवळ तयार केलेल्या उदाहरणांसह कार्य करते. सराव मध्ये, आपल्याला प्रकार, कार्यपद्धती, वस्तू इत्यादींसह वास्तविक भाषेची आवश्यकता आहे. हे चुकीचे आहे. ऍमेझॉनवर काम करणारा ख्रिस न्यूकॉम्ब काय लिहितो ते येथे आहे: “आम्ही दहा मोठ्या प्रकल्पांवर TLA+ चा वापर केला आहे, आणि प्रत्येक बाबतीत त्याच्या वापरामुळे विकासात लक्षणीय फरक पडला कारण आम्ही धोकादायक बग उत्पादनात येण्याआधीच पकडू शकलो आणि त्यामुळे आम्हाला आक्रमक बनवण्यासाठी आवश्यक असलेली अंतर्दृष्टी आणि आत्मविश्वास मिळाला. कार्यक्रमाच्या सत्यावर परिणाम न करता कार्यप्रदर्शन ऑप्टिमायझेशन". आपण अनेकदा ऐकू शकता की औपचारिक पद्धती वापरताना आम्हाला अकार्यक्षम कोड मिळतो - सराव मध्ये, सर्वकाही अगदी उलट आहे. याव्यतिरिक्त, अशी धारणा आहे की व्यवस्थापकांना औपचारिक पद्धतींची आवश्यकता पटवून देऊ शकत नाही, जरी प्रोग्रामरना त्यांच्या उपयुक्ततेबद्दल खात्री असली तरीही. आणि न्यूकॉम्ब लिहितात: "व्यवस्थापक आता TLA+ मध्‍ये तपशील लिहिण्‍यासाठी सर्व संभाव्य मार्गाने दबाव आणत आहेत आणि विशेषत: यासाठी वेळ देत आहेत". म्हणून जेव्हा व्यवस्थापक TLA+ काम करत असल्याचे पाहतात, तेव्हा ते ते स्वीकारतात. ख्रिस न्यूकॉम्बने हे सुमारे सहा महिन्यांपूर्वी (ऑक्टोबर 2014) लिहिले होते, परंतु आता, माझ्या माहितीनुसार, TLA+ चा वापर 14 नव्हे तर 10 प्रकल्पांमध्ये केला जातो. दुसरे उदाहरण XBox 360 च्या डिझाइनशी संबंधित आहे. चार्ल्स ठाकर यांच्याकडे एक इंटर्न आला आणि मेमरी सिस्टमसाठी तपशील लिहिले. या स्पेसिफिकेशनबद्दल धन्यवाद, एक बग आढळला जो अन्यथा शोधला गेला नसता आणि प्रत्येक XBox 360 चार तासांच्या वापरानंतर क्रॅश होईल. IBM च्या अभियंत्यांनी पुष्टी केली की त्यांच्या चाचण्यांमध्ये हा दोष आढळला नसता.

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

परंतु वरील उदाहरणात, वापरकर्त्याला बहुधा संयोग आणि समान चिन्हे संरेखित करायची होती. त्यामुळे योग्य स्वरूपन यासारखे दिसेल:

आणखी एक उदाहरण विचारात घ्या:

येथे, त्याउलट, स्त्रोतामध्ये समान चिन्हे, जोड आणि गुणाकार यांचे संरेखन यादृच्छिक होते, म्हणून सर्वात सोपी प्रक्रिया पुरेसे आहे. सर्वसाधारणपणे, योग्य स्वरूपनाची कोणतीही अचूक गणितीय व्याख्या नाही, कारण या प्रकरणात "योग्य" म्हणजे "वापरकर्त्याला काय हवे आहे" आणि हे गणिताने निर्धारित केले जाऊ शकत नाही.

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

औपचारिक तपशील का वापरला जाऊ शकला नाही? एकीकडे, योग्य अंमलबजावणी येथे फारशी महत्त्वाची नाही. संरचित प्रिंटआउट काहींसाठी असमाधानकारक असेल, म्हणून मला सर्व असामान्य परिस्थितीत ते योग्यरित्या कार्य करण्याची गरज नाही. त्याहूनही महत्त्वाचे म्हणजे माझ्याकडे पुरेशी साधने नव्हती. TLA+ मॉडेल तपासक येथे निरुपयोगी आहे, म्हणून मला उदाहरणे हाताने लिहावी लागतील.

दिलेल्या तपशीलामध्ये सर्व वैशिष्ट्यांसाठी समान वैशिष्ट्ये आहेत. हे कोडपेक्षा उच्च पातळी आहे. ते कोणत्याही भाषेत लागू केले जाऊ शकते. ते लिहिण्यासाठी कोणतीही साधने किंवा पद्धती नाहीत. कोणताही प्रोग्रामिंग कोर्स तुम्हाला हे तपशील लिहिण्यास मदत करणार नाही. आणि अशी कोणतीही साधने नाहीत जी हे तपशील अनावश्यक बनवू शकतील, जोपर्यंत तुम्ही TLA+ मध्ये संरचित प्रिंटआउट प्रोग्राम लिहिण्यासाठी विशेषत: भाषा लिहित नाही. शेवटी, आम्ही कोड नेमका कसा लिहू याविषयी हे तपशील काहीही सांगत नाही, ते फक्त कोड काय करते ते सांगते. आम्‍ही कोडबद्दल विचार करण्‍यापूर्वी समस्‍येचा विचार करण्‍यात मदत करण्‍यासाठी आम्‍ही एक तपशील लिहितो.

परंतु या स्पेसिफिकेशनमध्ये अशी वैशिष्ट्ये देखील आहेत जी ते इतर वैशिष्ट्यांपेक्षा वेगळे करतात. 95% इतर तपशील खूपच लहान आणि सोपे आहेत:

पुढे, हे तपशील नियमांचा एक संच आहे. हे सहसा खराब तपशीलाचे लक्षण असते. नियमांच्या संचाचे परिणाम समजून घेणे खूप कठीण आहे, म्हणूनच मला ते डीबग करण्यात बराच वेळ घालवावा लागला. तथापि, या प्रकरणात मला एक चांगला मार्ग सापडला नाही.

सतत चालणार्‍या प्रोग्रामबद्दल काही शब्द बोलणे योग्य आहे. सामान्यत: ते समांतर कार्य करतात, जसे की ऑपरेटिंग सिस्टम किंवा वितरित प्रणाली. फार कमी लोक त्यांना त्यांच्या मनात किंवा कागदावर समजू शकतात, आणि मी त्यांच्यापैकी नाही, जरी मी एकदा ते करू शकलो होतो. म्हणून, आम्हाला अशा साधनांची आवश्यकता आहे जी आमचे कार्य तपासतील - उदाहरणार्थ, TLA+ किंवा PlusCal.

कोडने काय करावे हे मला आधीच माहित असल्यास मला तपशील लिहिण्याची गरज का होती? खरं तर, मला फक्त ते माहित आहे असे वाटले. या व्यतिरिक्त, एका विशिष्टतेसह, बाहेरच्या व्यक्तीला कोड नक्की काय आहे हे समजून घेण्यासाठी यापुढे पाहण्याची आवश्यकता नाही. माझा एक नियम आहे: कोणतेही सामान्य नियम नसावेत. या नियमाला अर्थातच अपवाद आहे, हा एकमेव सामान्य नियम आहे ज्याचे मी पालन करतो: कोड काय करतो याचे तपशील लोकांना ते कोड वापरताना त्यांना माहित असणे आवश्यक असलेल्या सर्व गोष्टी सांगायला हवे.

तर प्रोग्रामरना विचार करण्याबद्दल नेमके काय माहित असणे आवश्यक आहे? सुरुवातीला, प्रत्येकासाठी सारखेच: जर तुम्ही लिहिले नाही, तर तुम्हाला असे वाटते की तुम्ही विचार करत आहात. तसेच, आपण कोड करण्यापूर्वी आपल्याला विचार करणे आवश्यक आहे, याचा अर्थ आपण कोड करण्यापूर्वी आपल्याला लिहिणे आवश्यक आहे. स्पेसिफिकेशन म्हणजे आम्ही कोडिंग सुरू करण्यापूर्वी जे लिहितो. कोणत्याही कोडसाठी एक तपशील आवश्यक आहे जो कोणीही वापरला जाऊ शकतो किंवा बदलू शकतो. आणि हा "कोणीतरी" कोड लिहिल्यानंतर एक महिन्यानंतर त्याचा लेखक होऊ शकतो. मोठ्या प्रोग्राम्स आणि सिस्टम्ससाठी, वर्गांसाठी, पद्धतींसाठी आणि काहीवेळा एकाच पद्धतीच्या जटिल विभागांसाठी एक तपशील आवश्यक आहे. कोडबद्दल नक्की काय लिहावे? तुम्हाला ते काय करते याचे वर्णन करणे आवश्यक आहे, म्हणजे, हा कोड वापरणार्‍या कोणालाही उपयुक्त ठरू शकेल असे काहीतरी. काहीवेळा कोड त्याचे ध्येय नेमके कसे साध्य करते हे निर्दिष्ट करणे देखील आवश्यक असू शकते. जर आपण अल्गोरिदम कोर्समध्ये या पद्धतीतून गेलो तर आपण त्याला अल्गोरिदम म्हणतो. जर ते अधिक विशिष्ट आणि नवीन असेल तर आम्ही त्याला उच्च-स्तरीय डिझाइन म्हणतो. येथे कोणताही औपचारिक फरक नाही: दोन्ही प्रोग्रामचे अमूर्त मॉडेल आहेत.

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

तपशील आणि कोड कसे जोडायचे? गणिती संकल्पना आणि त्यांची अंमलबजावणी यांना जोडणाऱ्या टिप्पण्या वापरणे. जर तुम्ही आलेखांसह काम केले, तर प्रोग्राम स्तरावर तुमच्याकडे नोड्सचे अॅरे आणि लिंक्सचे अॅरे असतील. त्यामुळे या प्रोग्रामिंग स्ट्रक्चर्सद्वारे आलेख नेमका कसा अंमलात आणला जातो हे तुम्हाला लिहावे लागेल.

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

तपशील लिहिणे ही कोडिंग प्रक्रियेतील एक अतिरिक्त पायरी आहे. त्याबद्दल धन्यवाद, कमी प्रयत्नात बर्‍याच त्रुटी पकडल्या जाऊ शकतात - आम्हाला Amazon वरील प्रोग्रामरच्या अनुभवावरून हे माहित आहे. वैशिष्ट्यांसह, कार्यक्रमांची गुणवत्ता उच्च होते. मग आपण अनेकदा त्यांच्याशिवाय का जातो? कारण लिहिणे अवघड आहे. पण लिहिणे अवघड आहे, कारण त्यासाठी विचार करणे आवश्यक आहे, आणि विचार करणे देखील कठीण आहे. आपण विचार करत असल्याची बतावणी करणे नेहमीच सोपे असते. येथे तुम्ही धावण्याशी साधर्म्य काढू शकता - तुम्ही जितके कमी धावाल तितके हळू. तुम्हाला तुमच्या स्नायूंना प्रशिक्षित करणे आणि लेखनाचा सराव करणे आवश्यक आहे. त्यासाठी सराव लागतो.

स्पेसिफिकेशन चुकीचे असू शकते. तुमची कुठेतरी चूक झाली असेल, किंवा आवश्यकता बदलल्या असतील, किंवा सुधारणा करण्याची आवश्यकता असू शकते. कोणीही वापरत असलेला कोणताही कोड बदलला पाहिजे, त्यामुळे लवकरच किंवा नंतर तपशील यापुढे प्रोग्रामशी जुळणार नाहीत. आदर्शपणे, या प्रकरणात, आपल्याला एक नवीन तपशील लिहिण्याची आणि कोड पूर्णपणे पुन्हा लिहिण्याची आवश्यकता आहे. हे कोणी करत नाही हे आम्हाला चांगलंच माहीत आहे. सराव मध्ये, आम्ही कोड पॅच करतो आणि कदाचित तपशील अद्यतनित करतो. जर हे लवकर किंवा नंतर घडणे बंधनकारक असेल, तर मग तपशील का लिहावे? प्रथम, तुमचा कोड संपादित करणार्‍या व्यक्तीसाठी, तपशीलातील प्रत्येक अतिरिक्त शब्दाचे वजन सोन्यामध्ये असेल आणि ही व्यक्ती तुम्हीच असू शकता. जेव्हा मी माझा कोड संपादित करतो तेव्हा पुरेसा विशिष्ट नसल्यामुळे मी अनेकदा स्वतःला लाथ मारतो. आणि मी कोडपेक्षा अधिक तपशील लिहितो. म्हणून, जेव्हा तुम्ही कोड संपादित करता, तेव्हा तपशील नेहमी अपडेट करणे आवश्यक असते. दुसरे म्हणजे, प्रत्येक संपादनासह कोड खराब होतो, वाचणे आणि राखणे अधिक कठीण होते. ही एन्ट्रॉपीमध्ये वाढ आहे. परंतु तुम्ही स्पेसिफिकेशनने सुरुवात केली नाही, तर तुम्ही लिहीलेली प्रत्येक ओळ संपादन असेल आणि कोड सुरुवातीपासूनच मोठा आणि वाचण्यास कठीण असेल.

म्हटल्याप्रमाणे आयझेनहॉवर, योजनेनुसार कोणतीही लढाई जिंकली गेली नाही आणि योजनेशिवाय कोणतीही लढाई जिंकली गेली नाही. आणि त्याला युद्धांबद्दल काहीतरी माहित होते. तपशील लिहिणे म्हणजे वेळेचा अपव्यय आहे असे मत आहे. कधीकधी हे खरे असते आणि कार्य इतके सोपे असते की त्यावर विचार करण्यात काही अर्थ नाही. परंतु तुम्ही नेहमी लक्षात ठेवा की जेव्हा तुम्हाला तपशील लिहू नका असा सल्ला दिला जातो तेव्हा याचा अर्थ असा होतो की तुम्हाला विचार न करण्याचा सल्ला दिला जातो. आणि आपण प्रत्येक वेळी याचा विचार केला पाहिजे. एखाद्या कार्याचा विचार केल्याने आपण चुका करणार नाही याची हमी देत ​​नाही. आपल्याला माहित आहे की, कोणीही जादूच्या कांडीचा शोध लावला नाही आणि प्रोग्रामिंग हे एक कठीण काम आहे. परंतु आपण कार्याचा विचार न केल्यास, आपल्याकडून चुका होण्याची हमी आहे.

तुम्ही TLA+ आणि PlusCal बद्दल विशेष वेबसाइटवर अधिक वाचू शकता, तुम्ही माझ्या होम पेजवरून तिथे जाऊ शकता दुवा. हे सर्व माझ्यासाठी आहे, तुमचे लक्ष दिल्याबद्दल धन्यवाद.

कृपया लक्षात ठेवा की हे भाषांतर आहे. तुम्ही टिप्पण्या लिहिता तेव्हा लक्षात ठेवा की लेखक त्या वाचणार नाहीत. जर तुम्हाला लेखकाशी खरोखरच गप्पा मारायच्या असतील, तर तो सेंट पीटर्सबर्ग येथे 2019-11 जुलै 12 रोजी होणाऱ्या Hydra 2019 परिषदेत असेल. तिकिटे खरेदी करता येतील अधिकृत वेबसाइटवर.

स्त्रोत: www.habr.com