अमूर्त व्याख्या

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

इसका मुख्य ठोस अनुप्रयोग औपचारिक स्थिर कोड विश्लेषण है, कंप्यूटर प्रोग्राम के संभावित निष्पादन के बारे में स्वचालित सूचना निष्कर्षण; ऐसे विश्लेषणों के दो मुख्य उपयोग हैं:

• संकलक के अंदर, यह तय करने के लिए प्रोग्राम का विश्लेषण करने के लिए कि कुछ अनुकूलन (कंप्यूटर विज्ञान) या प्रोग्राम परिवर्तन लागू हैं या नहीं;
• डिबगिंग या यहां तक ​​कि बग की कक्षाओं के खिलाफ कार्यक्रमों के प्रमाणन के लिए।

1970 के दशक के अंत में फ्रांसीसी कंप्यूटर वैज्ञानिक कामकाजी युगल पैट्रिक कूसोट और राधिया कुसोट द्वारा अमूर्त व्याख्या को औपचारिक रूप दिया गया था।

अंतर्ज्ञान

यह खंड वास्तविक दुनिया, गैर-कंप्यूटिंग उदाहरणों के माध्यम से अमूर्त व्याख्या को दर्शाता है।

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

हालाँकि यह संभव है कि केवल उपस्थित लोगों के नाम ही पंजीकृत किए गए हों। यदि किसी व्यक्ति का नाम सूची में नहीं मिलता है, तो हम सुरक्षित रूप से यह निष्कर्ष निकाल सकते हैं कि वह व्यक्ति उपस्थित नहीं था; लेकिन अगर ऐसा है, तो हम आगे की पूछताछ के बिना निश्चित रूप से निष्कर्ष नहीं निकाल सकते हैं, समलैंगिकों की संभावना के कारण (उदाहरण के लिए, जॉन स्मिथ नाम के दो लोग)। ध्यान दें कि यह सटीक जानकारी अभी भी अधिकांश उद्देश्यों के लिए पर्याप्त होगी, क्योंकि समानार्थी व्यवहार में दुर्लभ हैं। हालाँकि, सभी कठोरता में, हम निश्चित रूप से यह नहीं कह सकते कि कोई कमरे में मौजूद था; हम केवल इतना कह सकते हैं कि वह संभवतः यहाँ था। हम जिस व्यक्ति की तलाश कर रहे हैं यदि वह अपराधी है, तो हम एक अलार्म जारी करेंगे; लेकिन निश्चित रूप से गलत अलार्म जारी करने की संभावना है। इसी तरह की घटनाएं कार्यक्रमों के विश्लेषण में घटित होंगी।

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

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

कंप्यूटर प्रोग्राम की सार व्याख्या

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

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

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

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

औपचारिकता

उदाहरण: पूर्णांक सेट (लाल) का अमूर्त सेट (हरा) पर हस्ताक्षर करने के लिए

मान लीजिए कि L एक क्रमित समुच्चय है, जिसे मूर्त समुच्चय कहते हैं और L′ एक अन्य क्रमित समुच्चय है, जिसे अमूर्त समुच्चय कहते हैं। तत्वों को एक से दूसरे में मैप करने वाले कुल कार्यों को परिभाषित करके ये दो सेट एक दूसरे से संबंधित हैं।

एक फ़ंक्शन α को अमूर्त फ़ंक्शन कहा जाता है यदि यह कंक्रीट सेट L में एक तत्व x को सार सेट L' में एक तत्व α(x) में मैप करता है। अर्थात्, एल' में तत्व α(x) एल में एक्स का सार है।

एक फ़ंक्शन γ को कंक्रीटेशन फ़ंक्शन कहा जाता है यदि यह कंक्रीट सेट एल में एक तत्व γ(x′) के अमूर्त सेट L′ में एक तत्व x′ को मैप करता है। अर्थात, एल में तत्व γ(x′) का एक ठोसकरण है एक्स' एल' में।

चलो एल₁, एल₂, एल'₁ और मैं'₂ सेट का आदेश दिया जाए। ठोस शब्दार्थ f, L से एक मोनोटोनिक कार्य है₁ एल के लिए₂. L' से फलन f'₁ एल' के लिए₂ f का एक मान्य सार कहा जाता है यदि L' में सभी x' के लिए₁, (च ∘ γ)(x′) ≤ (γ ∘ f′)(x′)।

लूप या पुनरावर्ती प्रक्रियाओं की उपस्थिति में प्रोग्राम सिमेंटिक्स को सामान्यतः निश्चित बिंदु (गणित) का उपयोग करके वर्णित किया जाता है। आइए हम मान लें कि L एक पूर्ण जाली है और f को L से L तक एक मोनोटोनिक फ़ंक्शन होने दें। फिर, कोई भी x′ ऐसा है कि f(x′) ≤ x′, f के कम से कम निश्चित-बिंदु का एक सार है, जो मौजूद है नास्टर-टार्स्की प्रमेय के अनुसार।

कठिनाई अब ऐसा x' प्राप्त करना है। यदि L' परिमित ऊंचाई का है, या कम से कम आरोही श्रृंखला की स्थिति की पुष्टि करता है (सभी आरोही क्रम अंततः स्थिर हैं), तो ऐसे x' को आरोही अनुक्रम x' की स्थिर सीमा के रूप में प्राप्त किया जा सकता है।_n आगमन द्वारा परिभाषित इस प्रकार है: x′₀=⊥ (L′ का सबसे छोटा अवयव) और x′_n+1=च'(एक्स'_n).

अन्य मामलों में, इस तरह के एक एक्स 'को एक विस्तार (कंप्यूटर विज्ञान) के माध्यम से प्राप्त करना अभी भी संभव है ∇: सभी x और y के लिए, x ∇ y, ​​x और y दोनों से बड़ा या बराबर होना चाहिए, और किसी भी अनुक्रम y' के लिए_n, x′ द्वारा परिभाषित अनुक्रम₀=⊥ और एक्स′_n+1= एक्स'_n ∇y'_n अन्ततः स्थिर है। फिर हम y' ले सकते हैं_n=च'(एक्स'_n).

कुछ मामलों में, गाल्वा कनेक्शन (α, γ) का उपयोग करके सार को परिभाषित करना संभव है, जहां α L से L' तक है और γ L' से L तक है। यह सर्वोत्तम सार के अस्तित्व को मानता है, जो जरूरी नहीं कि मामला हो। उदाहरण के लिए, यदि हम उत्तल बहुतल को घेरकर वास्तविक संख्याओं के जोड़े (x, y) का अमूर्त सेट करते हैं, तो x द्वारा परिभाषित डिस्क के लिए कोई इष्टतम अमूर्तता नहीं है।²+y² ≤ 1.

अमूर्त डोमेन के उदाहरण

संख्यात्मक सार डोमेन

कोई दिए गए प्रोग्राम बिंदु पर उपलब्ध प्रत्येक चर x को एक अंतराल [L] निर्दिष्ट कर सकता है_x, एच_x]। चर x को मान v(x) निर्दिष्ट करने वाला राज्य इन अंतरालों का एक ठोसकरण होगा यदि सभी x के लिए, v(x) [L] में है_x, एच_x]। अंतराल से [एल_x, एच_x] और मैं_y, एच_y] चर x और y के लिए, कोई आसानी से x+y के लिए अंतराल प्राप्त कर सकता है ([L_x+एल_y, एच_x+ एच_y]) और x−y के लिए ([L_x-एच_y, एच_x-एल_y]); ध्यान दें कि ये सटीक सार हैं, क्योंकि x+y के लिए संभावित परिणामों का सेट ठीक अंतराल है ([L_x+एल_y, एच_x+ एच_y])। गुणा, भाग आदि के लिए अधिक जटिल सूत्र प्राप्त किए जा सकते हैं, तथाकथित अंतराल अंकगणित उत्पन्न करते हैं। आइए अब निम्नलिखित अत्यंत सरल प्रोग्राम पर विचार करें: <पूर्व> वाई = एक्स; जेड = एक्स - वाई; </पूर्व>

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

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

उचित अंकगणितीय प्रकारों के साथ, के लिए परिणाम z शून्य होना चाहिए। लेकिन अगर हम अंतराल अंकगणित से प्रारम्भ करते हैं x [0, 1] में, एक मिलता है z [−1, +1] में। जबकि व्यक्तिगत रूप से लिए गए प्रत्येक ऑपरेशन बिल्कुल सारगर्भित थे, उनकी संरचना नहीं है।

समस्या स्पष्ट है: हमने बीच समानता संबंध का ट्रैक नहीं रखा x और y; वास्तव में, अंतराल का यह डोमेन चर के बीच किसी भी संबंध को ध्यान में नहीं रखता है, और इस प्रकार यह एक गैर-संबंधपरक डोमेन है। गैर-संबंधपरक डोमेन लागू करने के लिए तेज़ और सरल होते हैं, लेकिन सटीक नहीं होते हैं।

संबंधपरक संख्यात्मक सार डोमेन के कुछ उदाहरण हैं:

• सर्वांगसमता संबंध#पूर्णांकों पर मूल उदाहरण
• उत्तल बहुकोणीय आकृति (cf. बाईं तस्वीर) - कुछ उच्च कम्प्यूटेशनल लागत के साथ
• अंतर-बाध्य मेट्रिसेस
• अष्टकोना
• रैखिक समानताएं

और उसके संयोजन (जैसे कम उत्पाद,सी एफ सही चित्र)।

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

मशीन शब्द सार डोमेन

जबकि उच्च-स्तरीय भाषाएँ जैसे कि पायथन (प्रोग्रामिंग भाषा) या हास्केल (प्रोग्रामिंग भाषा) डिफ़ॉल्ट रूप से असीमित पूर्णांक का उपयोग करती हैं, निचले स्तर की प्रोग्रामिंग भाषाएँ जैसे C (प्रोग्रामिंग भाषा) या असेंबली भाषा सामान्यतः छोटे आकार के वर्ड (कंप्यूटर आर्किटेक्चर) पर काम करती हैं।, जो इंटीजर मॉडुलो n|इंटीजर मोडुलो का उपयोग करके अधिक उपयुक्त रूप से तैयार किए गए हैं ${\textstyle 2^{n}}$(जहाँ n मशीन शब्द की बिट चौड़ाई है)। ऐसे चरों के विभिन्न विश्लेषणों के लिए उपयुक्त कई अमूर्त डोमेन हैं।

बिटफ़ील्ड डोमेन प्रत्येक बिट को मशीन शब्द में अलग से मानता है, अर्थात, चौड़ाई n के एक शब्द को n सार मानों की एक सरणी के रूप में माना जाता है। अमूर्त मान सेट से लिए गए हैं ${\textstyle \{0,1,\bot \}}$, और अमूर्तता और कंक्रीटीकरण कार्य इसके द्वारा दिए गए हैं:

$\gamma (0)=\{0\}$

$\gamma (1)=\{1\}$

$\gamma (\bot )=\{0,1\}$

$\alpha (\{0\})=0$

$\alpha (\{1\})=1$

$\alpha (\{0,1\})=\bot$

$\alpha (\{\})=\bot$

इन सार मूल्यों पर बिटवाइज़ संचालन कुछ तीन-मूल्यवान तर्कों में संबंधित तार्किक संचालन के समान हैं। तीन-मूल्यवान तर्क:

NOT(A) A ¬A 0 1 ⊥ ⊥ 1 0	AND(A, B) A ∧ B B 0 ⊥ 1 A 0 0 0 0 ⊥ 0 ⊥ ⊥ 1 0 ⊥ 1	OR(A, B) A ∨ B B 0 ⊥ 1 A 0 0 ⊥ 1 ⊥ ⊥ ⊥ 1 1 1 1 1

यह भी देखें

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

बाहरी संबंध

• A web-page on Abstract Interpretation maintained by Patrick Cousot
• Roberto Bagnara's paper showing how it is possible to implement an abstract-interpretation based static analyzer for a C-like programming language
• The Static Analysis Symposia, proceedings appearing in the Springer LNCS series
• Conference on Verification, Model-Checking, and Abstract Interpretation (VMCAI), affiliated at the POPL conference, proceedings appearing in the Springer LNCS series

Lecture notes

• Abstract Interpretation. Patrick Cousot. MIT.
• David Schmidt's lecture notes on abstract interpretation
• Møller and Schwarzbach's lecture notes on Static Program Analysis
• Agostino Cortesi's lecture notes on Program Analysis and Verification
• Slides by Grégoire Sutre going through every step of Abstract Interpretation with many examples - also introducing Galois connections