टेस्ट या प्रकार

हाय, हैब्र। दूसरे दिन मैं इदरीस में कुछ करने के तरीके की तलाश कर रहा था, और एक अच्छे पद पर आया, जिसका एक मुफ्त अनुवाद काफी उपयुक्त लगता है। लिबर्टीज़ और गैग जहाँ आवश्यक हो, मैं "यहाँ इस तरह के स्किगलों द्वारा शुरुआत में और अंत में" निरूपित करूँगा।

परीक्षणों का उपयोग कब करें, और कब - प्रकार? उन्हें लिखने के हमारे प्रयासों के बदले में हमें क्या जानकारी और क्या गारंटी मिलती है?

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

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

विनिर्देश

एक सूची और कुछ अर्थ दिया जाए। सूची में इस मूल्य के सूचकांक को वापस करना आवश्यक है या संकेत मिलता है कि यह मूल्य सूची में नहीं है।

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

अजगर

 def x(y, z): # 10000    

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

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

के विश्लेषण

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

• प्रलेखन
  
  • Expected हम अपेक्षित व्यवहार को जानते हैं
    हमें इस फ़ंक्शन के व्यवहार के बारे में बताने के लिए कुछ भी नहीं है। आप अपनी दादी से नफरत करते हैं। आप एक राक्षस हैं।
• सुरक्षा उपायों
  
  • ✓ मेमोरी सुरक्षा
    पायथन एक कचरा संग्रहण भाषा है जो इस चिंता को हमसे दूर करती है। Preventsअभी तक, जहां तक ​​मुझे पता है, कुछ भी आपको इस फ़ंक्शन के अंदर असुरक्षित पुस्तकालयों या सी एफएफआई को खींचने से नहीं रोकता है ।ever

परीक्षण के साथ अजगर

 def test_happy_path(): assert x([1, 2, 3], 2) == 1 def test_missing(): assert x([1, 2, 3], 4) is None 

अब हम जानते हैं कि हमारा फ़ंक्शन काम करता है, और यदि तत्व गायब है, तो परिणाम None ?

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

संभावना है कि यह फ़ंक्शन None 4 लिए None लौटेगा, लेकिन 5 लिए नहीं, बल्कि पागल लगता है, और इस विशेष मामले में यह सबसे अधिक संभावना बकवास है। हम अपने विश्वास के स्तर से संतुष्ट हो सकते हैं और एक निश्चित संख्या में उदाहरणों पर बस सकते हैं। लेकिन फिर, फिर पोस्ट छोटा होगा, तो आइए कल्पना करें कि कार्यान्वयन इतना स्पष्ट नहीं है।

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

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

के विश्लेषण

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

• प्रलेखन
  
  • ✓ हमारे पास उपयोग का एक उदाहरण है
  • Classes हम कुछ वर्गों के मूल्यों को जानते हैं जिन्हें सही ढंग से संसाधित किया जाएगा
  • Types हम सभी प्रकार के मूल्यों को जानते हैं जिन्हें सही ढंग से संसाधित किया जाएगा
    हमारे पास तर्कों के प्रकारों पर कोई प्रतिबंध नहीं है, इसलिए इस बात के उदाहरणों के अस्तित्व के बावजूद कि फ़ंक्शन क्या संभाल सकता है, हम नहीं जानते कि किस प्रकार का परीक्षण नहीं किया गया है।
  • Expected हम अपेक्षित व्यवहार को जानते हैं
    Tick ​​मूल लेख के लेखक ने यहाँ पर टिक किया है, मैं अपने आप को एक क्रॉस लगाने की अनुमति दूंगा, ऊपर टिप्पणी दी गई
• विनिर्देश
  
  • Least कम से कम एक मामले में काम करता है
  • Is लौटा हुआ सूचकांक हमेशा एक वैध सूचकांक होता है
  • ✗ लौटा हुआ सूचकांक हमेशा एक उपयुक्त मूल्य इंगित करता है
  • Ing मिसिंग आइटम हमेशा None Nothing None / Nothing None लौटाता है
• सामान्य गलतियाँ
  
  • ✗ कोई टाइपो या गलत नाम नहीं
    स्थैतिक विश्लेषण मदद कर सकता है, लेकिन चूंकि पायथन एक गतिशील भाषा है, जो रनटाइम पर विभिन्न चीजों को ओवरराइड करने की क्षमता के साथ है, हम कभी भी यह साबित नहीं कर सकते हैं कि कोई त्रुटि नहीं है।
    विशेष रूप से, यह निर्धारित करना बहुत कठिन या असंभव हो सकता है कि विधि का नाम सही है, क्योंकि विधि कॉल की वैधता उस रनटाइम प्रकार के ऑब्जेक्ट पर निर्भर करती है जिस पर कॉल किया जाता है।
  • Ull कोई अप्रत्याशित null नहीं
  • ✗ त्रुटि का मामला हमेशा संभाला जाता है
    मेरे अनुभव में, यह त्रुटियों के सबसे सामान्य स्रोतों में से एक है: हमारे उदाहरण में, फ़ंक्शन एक लापता तत्व के मामले में None लौटाता है, लेकिन इस फ़ंक्शन का उपयोग करने वाला कोड मान सकता है, उदाहरण के लिए, कि यह हमेशा एक नंबर लौटाएगा। इसके अलावा, यह एक अखंड अपवाद भी हो सकता है।
• सुरक्षा उपायों
  
  • ✓ मेमोरी सुरक्षा
  • Be फ़ंक्शन को गलत प्रकार के साथ नहीं बुलाया जा सकता है
  • Effects कोई दुष्प्रभाव नहीं
  • Ions कोई अपवाद नहीं
  • ✗ कोई त्रुटि नहीं
  • ✗ कोई स्थायी चक्र नहीं

हास्केल

 xyz = -- 10000   

यदि आप वाक्यविन्यास से अपरिचित हैं: यह एक फ़ंक्शन x की परिभाषा है जिसमें पैरामीटर y और z । हास्केल में, आप प्रकारों को छोड़ सकते हैं, क्योंकि वे कार्यान्वयन से कट जाएंगे ellunless, बेशक, आप प्रकार के आधुनिक एक्सटेंशन से विभिन्न उन्नत सुविधाओं का उपयोग करते हैं system⟧।

ऐसा लग सकता है कि यह पायथन संस्करण से बहुत अलग नहीं है, लेकिन केवल इस तथ्य के लिए धन्यवाद कि हमने हास्केल में अपना फ़ंक्शन लिखा था और इसे टाइल किया गया है, हम पहले से ही कुछ दिलचस्प गुणों के बारे में बात कर सकते हैं।

के विश्लेषण

जाहिर है, हम यहां इतने निष्कर्ष नहीं निकाल सकते, लेकिन यहां कुछ बिंदुओं पर ध्यान दिया गया है:

• प्रलेखन
  
  • Expected हम अपेक्षित व्यवहार को जानते हैं
• सामान्य गलतियाँ
  
  • ✓ कोई टाइपो या गलत नाम नहीं
    चूंकि हास्केल एक संकलित भाषा है, सभी नामों को संकलन समय पर हल किया जाना चाहिए। यदि यह त्रुटि है तो प्रोग्राम केवल संकलित नहीं करेगा।
  • Ull कोई अप्रत्याशित null नहीं
    हास्केल में बस null नहीं है। समस्या हल हो गई!
• सुरक्षा उपायों
  
  • ✓ मेमोरी सुरक्षा
  • Be फ़ंक्शन को गलत प्रकार के साथ नहीं बुलाया जा सकता है
  • ✓ कोई अप्रत्याशित दुष्प्रभाव नहीं
    Did मूल लेख के लेखक ने इस आइटम को निर्दिष्ट नहीं किया है, लेकिन मैं अपने आप को यह नोट करने की अनुमति दूंगा कि यदि साइड इफेक्ट्स हैं, तो इस फ़ंक्शन का घटा हुआ प्रकार उनकी उपस्थिति का संकेत देगा, जिससे कॉलिंग कोड को उनकी क्षमताओं के बारे में पता चल जाएगा।

हास्केल प्रकार निर्दिष्ट करना

 x :: Eq a => [a] -> a -> Maybe Int xyz = -- ... 

इससे पहले, हमने दादी-नानी की सुरक्षा के बारे में अधिक स्पष्ट दृष्टिकोण के बारे में बात की: परीक्षणों से यह स्पष्ट था कि फ़ंक्शन किसी को नुकसान नहीं पहुंचाने वाला था , लेकिन क्या दादी वास्तव में सुरक्षित थीं? क्या यह फ़ंक्शन सही रूप से कोई शपथ पत्र नहीं भेजता है?

हास्केल एक शुद्ध कार्यात्मक भाषा होने के लिए जाना जाता है। इसका मतलब यह नहीं है कि कोड के दुष्प्रभाव नहीं हो सकते हैं, लेकिन सभी दुष्प्रभाव प्रकार में मौजूद होने चाहिए। हम इस फ़ंक्शन के प्रकार को जानते हैं, हम देखते हैं कि यह साफ है, इसलिए हमें यकीन है कि यह फ़ंक्शन किसी भी बाहरी स्थिति को संशोधित नहीं करता है।

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

के विश्लेषण

• प्रलेखन
  
  • ✓ हम अपेक्षित व्यवहार जानते हैं
  • ✗ हमारे पास उपयोग का एक उदाहरण है
  • Classes हम कुछ वर्गों के मूल्यों को जानते हैं जिन्हें सही ढंग से संसाधित किया जाएगा
  • Types हम सभी प्रकार के मूल्यों को जानते हैं जिन्हें सही ढंग से संसाधित किया जाएगा
• विनिर्देश
  
  • Least कम से कम एक मामले में काम करता है।
    लापता परीक्षणों या सबूतों के साथ, हम यह नहीं जानते कि क्या हमारा कार्य हमारी अपेक्षा के अनुरूप काम करता है!
  • Is लौटा हुआ सूचकांक हमेशा एक वैध सूचकांक होता है।
  • ✗ लौटा हुआ सूचकांक हमेशा एक उपयुक्त मूल्य इंगित करता है।
  • Missing एक लापता वस्तु हमेशा None / Nothing None लौटाती है।
• सामान्य गलतियाँ
  
  • ✓ कोई टाइपो या गलत नाम नहीं
  • Ull कोई अप्रत्याशित null नहीं
  • ✓ त्रुटि का मामला हमेशा संभाला जाता है
    यदि हमारा फ़ंक्शन Nothing लौटाता है, तो टाइप सिस्टम यह सुनिश्चित करता है कि यह मामला कॉलिंग कोड द्वारा सही ढंग से संभाला गया है। बेशक, इस मामले को नजरअंदाज किया जा सकता है, लेकिन यह स्पष्ट रूप से किया जाना चाहिए।
• सुरक्षा उपायों
  
  • ✓ मेमोरी सुरक्षा
  • Be फ़ंक्शन को गलत प्रकार के साथ नहीं बुलाया जा सकता है
  • Effects कोई दुष्प्रभाव नहीं
  • Ions कोई अपवाद नहीं
    मैं अपवादों और त्रुटियों को साझा करता हूं, यह मानते हुए कि अपवादों के बाद इसे पुनर्प्राप्त करना संभव है, और त्रुटियों के बाद (उदाहरण के लिए, आंशिक रूप से परिभाषित कार्य - नहीं।
    अधिकांश भाग के लिए, अपवाद प्रकारों में वर्णित हैं (उदाहरण के लिए, आईओ मोनड में)। एक अच्छे तरीके से, हमें पता होना चाहिए कि एक फ़ंक्शन केवल इसके प्रकार के आधार पर, एक अपवाद नहीं फेंकेगा। हालांकि, हास्केल इस उम्मीद को तोड़ता है कि अपवादों को शुद्ध कोड से फेंक दिया जाए ।
    H इसके अलावा, यह ध्यान देने योग्य है कि हास्केल में, गलत तरीके से आंशिक रूप से परिभाषित कार्यों को कॉल करने जैसी त्रुटियां भी अपवाद के रूप में प्रस्तुत की जाती हैं, जिन्हें पकड़ा और संसाधित किया जा सकता है, इसलिए दोनों श्रेणियों के बीच का अंतर थोड़ा कम स्पष्ट है।
  • ✗ कोई त्रुटि नहीं
    हम अभी भी आंशिक रूप से परिभाषित कार्यों का उपयोग कर सकते हैं, उदाहरण के लिए, शून्य से विभाजन।
  • ✗ कोई स्थायी चक्र नहीं

परीक्षणों के साथ हास्केल

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

उदाहरण के लिए:

 not :: Bool -> Bool not x = ... 

इनपुट True या False हो सकता है। इन दो विकल्पों का परीक्षण करना पर्याप्त है, और यहाँ यह है, पवित्र कंघी बनानेवाले की रेती! कोई अपवाद नहीं, सदा चक्र, गलत परिणाम, कोई त्रुटि नहीं। It हालांकि, थोड़े अधिक जटिल कार्य के लिए, यह स्पष्ट नहीं हो सकता है कि परीक्षणों पर कितना समय व्यतीत होता है: यदि उन्हें पूरा करने में लंबा समय लगता है, तो क्या हम एक अनन्त चक्र में समाप्त हो गए, या यह सिर्फ भारी है? उसे रोकने की समस्या।

वास्तव में, यह हास्केल के मामले में भी पूरी तरह से सच नहीं है: प्रत्येक हास्केल प्रकार में एक मान also भी होता है (जिसे undefined , error या कुछ अर्थों में अनंत पुनरावृत्ति के रूप में प्राप्त किया जा सकता है), लेकिन हास्केलिस्ट परंपरागत रूप से अपनी आँखें बंद करते हैं और मानते हैं कि यह मौजूद नहीं है।

Extracurricular पढ़ना: केवल चार बिलियन फ़्लोट्स हैं - इसलिए उन्हें सभी का परीक्षण करें!

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

के विश्लेषण
इस मामले में, परीक्षण प्रकारों के पूरक हैं और हास्केल प्रकार प्रणाली में कुछ छेदों को प्लग करते हैं। केवल परीक्षण या प्रकारों का उपयोग करने की तुलना में हमें अपने कोड पर अधिक विश्वास है।

सी

 /* C    ,    int */ int x(int *y, size_t n, int z) { /* 10000    */ } 

हम पुराने प्रकार के सिस्टम में सी आउट ऑफ इंटरेस्ट मानते हैं। सी में, विशेष रूप से, प्रोग्रामर द्वारा प्रकारों की सबसे अधिक आवश्यकता होती है, लेकिन कंपाइलर द्वारा उसे तेज कोड उत्पन्न करने में मदद करने के लिए।

हमारे उदाहरण में, हम नहीं जानते कि तत्व नहीं मिलने पर फ़ंक्शन क्या लौटेगा। हमें परंपरा या प्रलेखन पर निर्भर रहना होगा (उदाहरण के लिए, इस मामले में यह -1 हो सकता है)।

हम तर्कों का भी उपयोग कर सकते हैं: इस तरह हम एक त्रुटि लौटा सकते हैं और वापसी मूल्य को इस तर्क में संग्रहीत कर सकते हैं। यह थोड़ा अधिक अभिव्यंजक विकल्प है, लेकिन हमें अभी भी यह समझने के लिए प्रलेखन पर निर्भर रहना होगा कि कौन से पैरामीटर पढ़े गए हैं और कौन से लिखे गए हैं। दोनों मामलों में, प्रकारों को देखकर व्यवहार को समझना कठिन है।

 /*   ,   out- */ error_t x(int *y, size_t n, int z, size_t *w) { /* 10000    */ } 

के विश्लेषण
टाइप सिस्टम ही हमें इतनी सारी गारंटी नहीं देता है। बेशक, हमें इन प्रकारों से कुछ जानकारी मिलती है, लेकिन बस हास्केल मामले से इसकी तुलना करें।

इदरिस

 x : Eq x => List x -> x -> Maybe Int xyz = ... 

यह फ़ंक्शन उसी प्रकार का है जैसे हास्केल के मामले में। हालांकि, अधिक अभिव्यंजक प्रकार की प्रणाली के साथ, हम अधिक प्राप्त कर सकते हैं। प्रकारों का चुनाव कार्यान्वयन के बारे में बात कर सकता है।

 %default total x : Eq x => Vect nx -> x -> Maybe (Fin n) xyz = ... 

इस प्रकार के रूप में पढ़ा जा सकता है "मुझे आकार n की सूची और कुछ मूल्य दें, और मैं आपको n या n से कम संख्या में वापस कर दूंगा।" यह सुनिश्चित करता है कि फ़ंक्शन एक इंडेक्स लौटाता है जो स्पष्ट रूप से सीमा से परे नहीं जाता है।

इसके अलावा, यह फ़ंक्शन कुल है, अर्थात, टाइमर ने जांच की है कि यह हमेशा समाप्त होता है। यह स्थायी चक्र और त्रुटियों को समाप्त करता है।

के विश्लेषण

• विनिर्देश
  
  • Least कम से कम एक मामले में काम करता है।
  • Returned लौटा हुआ इंडेक्स हमेशा सही इंडेक्स होता है
  • ✗ लौटा हुआ सूचकांक हमेशा एक उपयुक्त मूल्य इंगित करता है
  • Ing मिसिंग आइटम हमेशा None Nothing None / Nothing None लौटाता है
• सुरक्षा उपायों
  
  • ✓ मेमोरी सुरक्षा
  • Be फ़ंक्शन को गलत प्रकार के साथ नहीं बुलाया जा सकता है
  • Effects कोई दुष्प्रभाव नहीं
  • Ions कोई अपवाद नहीं
  • ✓ कोई त्रुटि नहीं
  • ✓ कोई स्थायी चक्र नहीं

परीक्षण के साथ इदरीस

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

 ex : x [1, 2, 3] 2 = Just 1 ex = Refl 

इस फ़ंक्शन में एक अजीब प्रकार का x [1, 2, 3] 2 = Just 1 । इस प्रकार का मतलब है कि एक सफल प्रकार की जाँच के लिए, टाइपर को यह साबित करना होगा कि x [1, 2, 3] 2 संरचनात्मक रूप से Just 1 बराबर है। Sinceइस मामले में, सबूत तुच्छ है, क्योंकि यह टिपर के लिए समान चिह्न के दोनों किनारों पर शर्तों को सामान्य करने के लिए पर्याप्त है, जो कि उपयोग किए गए सभी कार्यों की समग्रता के कारण परिमित समय में किया जाएगा, और जो चर्च-रोसेर के कारण एक अद्वितीय परिणाम का नेतृत्व करेगा। उसके बाद, कोई समानता की Refl का उपयोग कर सकता है, जो कि Refl '

वास्तव में, हमने एक प्रकार का स्तर परीक्षण लिखा था।

सबूत के साथ इदरीस

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

विशेष रूप से, हम उन गुणों को सिद्ध कर सकते हैं जो पहले हमारे लिए अप्राप्य थे:

 --      Eq  DecEq x : DecEq a => Vect na -> (y : a) -> Maybe (Fin n) xyz = ... --    ,       `x` findIndexOk : DecEq a => (y : Vect na) -> (z : a) -> case xyz of Just i => index iy = z Nothing => Not (Elem zy) findIndexOk yz = ... 

Type findIndexOk को "किसी भी प्रकार के लिए" के रूप में पढ़ा जा सकता है, जिसमें इसके लिए एक एल्गोरिदमिक रूप से निर्णायक तुलना ( DecEq ) है, किसी भी प्रकार y तत्वों के किसी भी वेक्टर y और किसी भी प्रकार के z प्रकार z : यदि xyz रिटर्न सूचकांक i , तो यह सूचकांक z झूठ है, लेकिन अगर xyz Nothing देता है, तो वेक्टर में ऐसा कोई तत्व नहीं है। "

⟦यह दिलचस्प है कि मूल लेख का लेखक ऊपर दिए गए की तुलना में थोड़ा कमजोर है।

अब हम सब कुछ पर कब्जा कर लिया है! नुकसान क्या हैं? खैर, यह सब सबूत लिखना काफी मुश्किल हो सकता है।

तुलना

राय

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

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