निश्चित असाइनमेंट विश्लेषण

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

प्रेरणा

सी प्रोग्रामिंग भाषा और C++ प्रोग्राम्स में, विशेष रूप से कठिन-से-निदान त्रुटियों का एक स्रोत गैर-नियतात्मक व्यवहार है, जो गैर-प्रारंभिक चर पढ़ने के परिणामस्वरूप होता है; यह व्यवहार प्लेटफ़ॉर्म, बिल्ड और यहां तक ​​कि रन से रन के बीच भिन्न हो सकता है।

इस समस्या को हल करने के दो सामान्य तरीके हैं। एक यह सुनिश्चित करना है कि पढ़ने से पहले सभी स्थानों को लिखा जाए। राइस की प्रमेय स्थापित करती है कि इस समस्या को सामान्य रूप से सभी कार्यक्रमों के लिए हल नहीं किया जा सकता है; हालाँकि, एक रूढ़िवादी (अशुद्ध) विश्लेषण बनाना संभव है जो केवल उन कार्यक्रमों को स्वीकार करेगा जो इस बाधा को संतुष्ट करते हैं, जबकि कुछ सही कार्यक्रमों को अस्वीकार करते हैं, और निश्चित असाइनमेंट विश्लेषण ऐसा विश्लेषण है। जावा प्रोग्रामिंग भाषा और सी शार्प (प्रोग्रामिंग भाषा)|सी# प्रोग्रामिंग भाषा विशिष्टताओं के लिए आवश्यक है कि विश्लेषण विफल होने पर संकलक एक संकलन-समय त्रुटि की रिपोर्ट करे। दोनों भाषाओं को विश्लेषण के एक विशिष्ट रूप की आवश्यकता होती है जिसे सावधानीपूर्वक विस्तार से लिखा गया है। जावा में, इस विश्लेषण को स्टार्क एट अल द्वारा औपचारिक रूप दिया गया था। और कुछ सही कार्यक्रमों को अस्वीकार कर दिया जाता है और स्पष्ट अनावश्यक कार्य शुरू करने के लिए उन्हें बदलना चाहिए। सी # में, इस विश्लेषण को फ्रुजा द्वारा औपचारिक रूप दिया गया था, और यह सटीक होने के साथ-साथ ध्वनि भी है, इस अर्थ में कि सभी नियंत्रण प्रवाह पथों के साथ निर्दिष्ट सभी चर निश्चित रूप से निर्दिष्ट माने जाएंगे। चक्रवात (प्रोग्रामिंग भाषा) लैंग्वेज को भी प्रोग्राम्स को एक निश्चित असाइनमेंट एनालिसिस पास करने की आवश्यकता होती है, लेकिन केवल पॉइंटर टाइप वाले वेरिएबल्स पर, C प्रोग्राम्स की पोर्टिंग को आसान बनाने के लिए। समस्या को हल करने का दूसरा तरीका सभी स्थानों को स्वचालित रूप से कुछ निश्चित, पूर्वानुमेय मूल्य पर उस बिंदु पर प्रारंभ करना है जिस पर उन्हें परिभाषित किया गया है, लेकिन यह नए असाइनमेंट पेश करता है जो प्रदर्शन को बाधित कर सकते हैं। इस मामले में, निश्चित असाइनमेंट विश्लेषण एक संकलक अनुकूलन को सक्षम करता है जहां अनावश्यक असाइनमेंट - असाइनमेंट केवल अन्य असाइनमेंट के बाद बिना किसी संभावित हस्तक्षेप के पढ़ता है - समाप्त किया जा सकता है। इस मामले में, कोई कार्यक्रम अस्वीकार नहीं किया जाता है, लेकिन जिन कार्यक्रमों के लिए विश्लेषण निश्चित असाइनमेंट को पहचानने में विफल रहता है, उनमें अनावश्यक आरंभीकरण हो सकता है। सामान्य भाषा अवसंरचना इस दृष्टिकोण पर निर्भर करता है।

शब्दावली

कार्यक्रम में किसी दिए गए बिंदु पर एक चर या स्थान को तीन राज्यों में से एक में कहा जा सकता है:

• निश्चित रूप से असाइन किया गया: वेरिएबल निश्चित रूप से असाइन किए जाने के लिए जाना जाता है।
• निश्चित रूप से असाइन नहीं किया गया: वेरिएबल निश्चित रूप से असाइन किए जाने के लिए जाना जाता है।
• अज्ञात: चर असाइन या असाइन नहीं किया जा सकता है; विश्लेषण यह निर्धारित करने के लिए पर्याप्त सटीक नहीं है कि कौन सा।

विश्लेषण

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

Name	Domain	Description
before	All statements and expressions	Variables definitely assigned before the evaluation of the given statement or expression.
after	All statements and expressions	Variables definitely assigned after the evaluation of the given statement or expression, assuming it completes normally.
vars	All statements and expressions	All variables available in the scope of the given statement or expression.
true	All boolean expressions	Variables definitely assigned after the evaluation of the given expression, assuming the expression evaluates to true.
false	All boolean expressions	Variables definitely assigned after the evaluation of the given expression, assuming the expression evaluates to false.

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

• कोई भी अभिव्यक्ति या बयान ई जो निश्चित रूप से असाइन किए गए चर के सेट को प्रभावित नहीं करता है: के बाद (ई) = पहले (ई)
• ई को असाइनमेंट एक्सप्रेशन loc = v होने दें। फिर पहले (v) = पहले (ई), और बाद में (ई) = के बाद (v) यू {लोक}।
• आइए अभिव्यक्ति 'सत्य' बनें। फिर सच (ई) = पहले (ई) और झूठा (ई) = संस्करण (ई)। दूसरे शब्दों में, यदि ई 'गलत' का मूल्यांकन करता है, तो सभी चर (रिक्त सत्य) निश्चित रूप से निर्दिष्ट होते हैं, क्योंकि ई गलत का मूल्यांकन नहीं करता है।
• चूँकि विधि तर्कों का मूल्यांकन बाएँ से दाएँ किया जाता है, इससे पहले (arg_i + 1) = के बाद (तर्क_i). एक विधि पूर्ण होने के बाद, आउट पैरामीटर निश्चित रूप से असाइन किए जाते हैं।
• चलो सशर्त बयान 'अगर' (ई) एस हो₁ और स₂. फिर पहले (ई) = पहले (एस), पहले (एस₁) = सच (ई), पहले (एस₂) = झूठा (ई), और उसके बाद (एस) = के बाद (एस₁) के बाद प्रतिच्छेद करें (एस₂).
• चलो जबकि लूप स्टेटमेंट 'जबकि' (ई) एस₁. फिर पहले (ई) = पहले (एस), पहले (एस₁) = सच (ई), और बाद में (एस) = गलत (ई)।
• और इसी तरह।

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

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

इंट आई = 1;
एल:
गोटो एल;

</वाक्यविन्यास हाइलाइट> चूँकि लेबल L को दो स्थानों से पहुँचा जा सकता है, गोटो के लिए नियंत्रण-प्रवाह समीकरण तय करता है कि पहले (2) = बाद (1) पहले (3) को काटता है। लेकिन पहले (3) = पहले (2), इसलिए पहले (2) = के बाद (1) पहले (2) प्रतिच्छेद करें। इसमें पहले (2), {i} और खाली सेट के लिए दो निश्चित बिंदु हैं। हालांकि, यह दिखाया जा सकता है कि डेटा-प्रवाह समीकरणों के मोनोटोनिक रूप के कारण, एक अद्वितीय अधिकतम निश्चित बिंदु (सबसे बड़े आकार का निश्चित बिंदु) है जो निश्चित रूप से निर्दिष्ट चर के बारे में सबसे अधिक संभव जानकारी प्रदान करता है। इस तरह के अधिकतम (या अधिकतम) निश्चित बिंदु की गणना मानक तकनीकों द्वारा की जा सकती है; डेटा प्रवाह विश्लेषण देखें।

एक अतिरिक्त मुद्दा यह है कि एक नियंत्रण-प्रवाह कूद कुछ नियंत्रण प्रवाहों को अव्यवहार्य बना सकता है; उदाहरण के लिए, इस कोड खंड में चर i निश्चित रूप से उपयोग किए जाने से पहले असाइन किया गया है: <वाक्यविन्यास लैंग = सी लाइन>

int मैं;
अगर (जे <0) वापसी; और मैं = जे;
प्रिंट (मैं);

</वाक्यविन्यास हाइलाइट> if के लिए डेटा-फ्लो समीकरण कहता है कि after(2) = after('return') after(i = j) प्रतिच्छेद करता है। इस कार्य को सही ढंग से करने के लिए, हम सभी नियंत्रण-प्रवाह कूदों के लिए after(e) = var(e) परिभाषित करते हैं; यह उसी अर्थ में रिक्त रूप से मान्य है कि समीकरण false('true') = vars(e) मान्य है, क्योंकि नियंत्रण-प्रवाह कूद के तुरंत बाद नियंत्रण के लिए एक बिंदु तक पहुंचना संभव नहीं है।