Formal specification
कंप्यूटर विज्ञान में, औपचारिक विनिर्देश गणितीय रूप से आधारित तकनीकें हैं जिनका उद्देश्य सिस्टम और सॉफ्टवेयर के कार्यान्वयन में मदद करना है। इनका उपयोग किसी प्रणाली का वर्णन करने, उसके व्यवहार का विश्लेषण करने और कठोर और प्रभावी तर्क उपकरणों के माध्यम से रुचि के प्रमुख गुणों को सत्यापित करके उसके डिजाइन में सहायता करने के लिए किया जाता है। ये विनिर्देश इस अर्थ में औपचारिक हैं कि उनके पास एक वाक्यविन्यास है, उनके शब्दार्थ एक डोमेन के भीतर आते हैं, और उनका उपयोग उपयोगी जानकारी का अनुमान लगाने के लिए किया जा सकता है। प्रेरणा प्रत्येक बीतते दशक में, कंप्यूटर प्रणालियाँ तेजी से अधिक शक्तिशाली हो गई हैं और परिणामस्वरूप, वे समाज के लिए अधिक प्रभावशाली हो गई हैं। इस वजह से, विश्वसनीय सॉफ्टवेयर के डिजाइन और कार्यान्वयन में सहायता के लिए बेहतर तकनीकों की आवश्यकता है। स्थापित इंजीनियरिंग विषय गणितीय विश्लेषण का उपयोग उत्पाद डिजाइन बनाने और मान्य करने की नींव के रूप में करते हैं। सॉफ्टवेयर इंजीनियरिंग विश्वसनीयता में इसे प्राप्त करने के लिए औपचारिक विनिर्देश एक ऐसा तरीका है जैसा कि एक बार भविष्यवाणी की गई थी। परीक्षण जैसी अन्य विधियों का उपयोग आमतौर पर कोड की गुणवत्ता बढ़ाने के लिए किया जाता है। उपयोग इस तरह के विनिर्देशन को देखते हुए, यह प्रदर्शित करने के लिए औपचारिक सत्यापन तकनीकों का उपयोग करना संभव है कि एक प्रणाली डिजाइन अपने विनिर्देशन के संबंध में सही है। यह किसी भी बड़े निवेश को वास्तविक कार्यान्वयन में लाने से पहले गलत प्रणाली डिजाइनों को संशोधित करने की अनुमति देता है। एक अन्य दृष्टिकोण एक विनिर्देश को एक डिजाइन में बदलने के लिए शायद सही परिष्करण चरणों का उपयोग करना है, जो अंततः एक कार्यान्वयन में बदल जाता है जो निर्माण द्वारा सही है। यह ध्यान रखना महत्वपूर्ण है कि एक औपचारिक विनिर्देश एक कार्यान्वयन नहीं है, बल्कि इसका उपयोग एक कार्यान्वयन विकसित करने के लिए किया जा सकता है। औपचारिक विनिर्देश वर्णन करते हैं कि एक प्रणाली को क्या करना चाहिए, न कि प्रणाली को इसे कैसे करना चाहिए। एक अच्छे विनिर्देशन में निम्नलिखित विशेषताओं में से कुछ होनी चाहिएः पर्याप्त, आंतरिक रूप से सुसंगत, असंदिग्ध, पूर्ण, संतुष्ट, न्यूनतम एक अच्छा विनिर्देशन होगाः निर्माण क्षमता, प्रबंधनीयता और विकासशीलता उपयोगिता संचार क्षमता शक्तिशाली और कुशल विश्लेषण औपचारिक विनिर्देशों में रुचि रखने के मुख्य कारणों में से एक यह है कि वे सॉफ्टवेयर कार्यान्वयन पर प्रमाण करने की क्षमता प्रदान करेंगे। इन प्रमाणों का उपयोग किसी विनिर्देश को मान्य करने, डिजाइन की शुद्धता को सत्यापित करने या यह साबित करने के लिए किया जा सकता है कि कोई प्रोग्राम किसी विनिर्देश को संतुष्ट करता है। सीमाएं एक डिजाइन (या कार्यान्वयन) को कभी भी अपने दम पर "सही" घोषित नहीं किया जा सकता है। यह केवल "किसी दिए गए विनिर्देश के संबंध में सही" हो सकता है। क्या औपचारिक विनिर्देशन हल की जाने वाली समस्या का सही वर्णन करता है, यह एक अलग मुद्दा है। इसे संबोधित करना भी एक कठिन मुद्दा है क्योंकि यह अंततः एक अनौपचारिक ठोस समस्या क्षेत्र के अमूर्त औपचारिक प्रतिनिधित्व के निर्माण की समस्या से संबंधित है, और इस तरह का एक अमूर्त कदम औपचारिक प्रमाण के लिए उत्तरदायी नहीं है। हालाँकि, उन गुणों से संबंधित "चुनौती" प्रमेयों को साबित करके एक विनिर्देशन को मान्य करना संभव है जो विनिर्देशन से प्रदर्शित होने की उम्मीद है। यदि सही है, तो ये प्रमेय विनिर्देशन की विनिर्देशक की समझ और अंतर्निहित समस्या क्षेत्र के साथ इसके संबंध को सुदृढ़ करते हैं। यदि नहीं, तो विनिर्देशन के उत्पादन (और कार्यान्वयन) से जुड़े लोगों की डोमेन समझ को बेहतर ढंग से प्रतिबिंबित करने के लिए विनिर्देशन को शायद बदलने की आवश्यकता है। सॉफ्टवेयर विकास के औपचारिक तरीकों का उद्योग में व्यापक रूप से उपयोग नहीं किया जाता है। अधिकांश कंपनियाँ अपनी सॉफ्टवेयर विकास प्रक्रियाओं में उन्हें लागू करना लागत प्रभावी नहीं मानती हैं। यह कई कारणों से हो सकता है, जिनमें से कुछ हैंः कम मापने योग्य रिटर्न के साथ समय उच्च प्रारंभिक स्टार्ट अप लागत लचीलापन बहुत सारी सॉफ्टवेयर कंपनियां फुर्तीली पद्धतियों का उपयोग करती हैं जो लचीलेपन पर ध्यान केंद्रित करती हैं। सामने की ओर पूरी प्रणाली का एक औपचारिक विनिर्देश करना अक्सर लचीले के विपरीत के रूप में माना जाता है। हालांकि, "फुर्तीले" विकास जटिलता के साथ औपचारिक विनिर्देशों का उपयोग करने के लाभों में कुछ शोध है उन्हें समझने और उन्हें प्रभावी ढंग से लागू करने के लिए उच्च स्तर की गणितीय विशेषज्ञता और विश्लेषणात्मक कौशल की आवश्यकता होती है इसका एक समाधान ऐसे उपकरण और मॉडल विकसित करना होगा जो इन तकनीकों को लागू करने की अनुमति देते हैं लेकिन अंतर्निहित गणित के सीमित दायरे को छिपाते हैं वे परियोजना में सभी हितधारकों के लिए रुचि के गुणों को नहीं पकड़ते हैं वे उपयोगकर्ता इंटरफेस और उपयोगकर्ता बातचीत को निर्दिष्ट करने का अच्छा काम नहीं करते हैं लागत प्रभावी नहीं यह पूरी तरह से सच नहीं है, उनके उपयोग को केवल महत्वपूर्ण प्रणालियों के मुख्य भागों तक सीमित करके उन्होंने लागत प्रभावी दिखाया है अन्य सीमाएंः अलगाव निम्न-स्तरीय ऑन्टोलॉजी खराब मार्गदर्शन चिंताओं का खराब पृथक्करण खराब प्रतिक्रिया उपकरण प्रतिमान औपचारिक विनिर्देश तकनीकें विभिन्न क्षेत्रों में मौजूद हैं। औपचारिक विनिर्देशों का कार्यान्वयन इस बात पर निर्भर करता है कि वे किस प्रकार की प्रणाली को मॉडल करने का प्रयास कर रहे हैं, उन्हें कैसे लागू किया जाता है और सॉफ्टवेयर जीवन चक्र में उन्हें किस बिंदु पर पेश किया गया है। इस प्रकार के मॉडलों को निम्नलिखित विनिर्देशन प्रतिमानों में वर्गीकृत किया जा सकता हैः प्रणाली इतिहास के आधार पर इतिहास-आधारित विनिर्देशन व्यवहार की व्याख्या समय के साथ की जाती है-प्रणाली अवस्थाओं की क्रमिक चरणों की श्रृंखला के आधार पर राज्य-आधारित विनिर्देशन व्यवहार, (जैसे। एक वित्तीय लेन-देन) जेड, वी. डी. एम. या बी. जैसी भाषाएँ इस प्रतिमान संक्रमण-आधारित विनिर्देशन व्यवहार पर निर्भर करती हैं जो स्टेटचार्ट, प्रोमेला, एस. टी. ई. पी.-एस. पी. एल., आर. एस. एम. एल. या एस. सी. आर. जैसी प्रतिक्रियाशील प्रणाली भाषाओं के साथ सबसे अच्छी तरह से उपयोग की जाने वाली प्रणाली के राज्य-से-राज्य संक्रमणों पर आधारित होती हैं। कार्यात्मक विनिर्देशन इस प्रतिमान पर निर्भर करता है। एक प्रणाली को गणितीय कार्यों की संरचना के रूप में निर्दिष्ट करता है ओ. बी. जे., ए. एस. एल., पी. एल. यू. एस. एस., एल. ए. आर. सी. एच., एच. ओ. एल. या पी. वी. एस. इस प्रतिमान पर निर्भर करते हैं। यहाँ संदर्भित पेपर एक विनिर्देश को डिजाइन करते समय उपयोग करने के लिए ह्यूरिस्टिक्स पर सबसे अच्छी चर्चा करता है। वे एक विभाजन और विजय दृष्टिकोण लागू करके ऐसा करते हैं। सॉफ्टवेयर उपकरण जेड संकेतन एक प्रमुख औपचारिक विनिर्देशन भाषा का एक उदाहरण है। अन्य में वियना विकास पद्धति की विनिर्देशन भाषा (वी. डी. एम.-एस. एल.) और बी-विधि की अमूर्त मशीन संकेतन (ए. एम. एन.) शामिल हैं। वेब सेवा क्षेत्र में, औपचारिक विनिर्देशन का उपयोग अक्सर गैर-कार्यात्मक गुणों (वेब सेवाओं की सेवा की गुणवत्ता) का वर्णन करने के लिए किया जाता है। कुछ उपकरण हैंः बीजगणितीय लार्च ओ. बी. जे. लोटोस मॉडल-आधारित जेड. बी. वी. डी. एम. सी. एस. पी. पेट्री नेट्स टी. एल. ए. + यह भी देखें बीजगणितीय विनिर्देशन औपचारिक तरीके मॉडल-आधारित विनिर्देशन सॉफ्टवेयर इंजीनियरिंग विनिर्देशन भाषा विनिर्देशन (तकनीकी मानक) संदर्भ बाहरी लिंक कोर्योथ 2005-07-30 औपचारिक विधियों द्वारा औपचारिक विनिर्देशन के लिए एक मामला