एब्स्ट्रैक्ट इंटरप्रिटेशन (Abstract Interpretation)

एब्स्ट्रैक्ट इंटरप्रिटेशन एक गणितीय सिद्धांत है जो एक सरल एब्स्ट्रैक्ट डोमेन में प्रोग्राम के सिमेंटिक्स (semantics) का व्यवस्थित रूप से अनुमान लगाकर सुदृढ़ स्टैटिक विश्लेषण (static analyses) को डिजाइन करने के लिए है।

Definition

एब्स्ट्रैक्ट इंटरप्रिटेशन प्रोग्राम सिमेंटिक्स के सुदृढ़ अनुमान का एक सिद्धांत है जिसमें एक कंक्रीट सिमेंटिक्स को एक संगणनीय एब्स्ट्रैक्ट सिमेंटिक्स से संबंधित किया जाता है, ताकि एब्स्ट्रैक्ट डोमेन में सिद्ध किए गए गुण वास्तविक प्रोग्राम के लिए मान्य होने की गारंटी हो।

Scope

यह विषय एब्स्ट्रैक्ट इंटरप्रिटेशन के फ्रेमवर्क को कवर करता है: गैलोज़ कनेक्शन (Galois connections) के माध्यम से कंक्रीट और एब्स्ट्रैक्ट सिमेंटिक्स को संबंधित करना, एब्स्ट्रैक्ट डोमेन (अंतराल, पॉलीहेड्रा, ऑक्टागन), समाप्ति सुनिश्चित करने के लिए वाइडनिंग (widening) और नैरोइंग (narrowing) के साथ फिक्सपॉइंट गणना, और विश्लेषण का व्यवस्थित, सही-बाय-कंस्ट्रक्शन (correct-by-construction) डिज़ाइन। यह इस बात पर प्रकाश डालता है कि सुदृढ़ता कैसे सुनिश्चित की जाती है और सटीकता को कैसे समायोजित किया जाता है।

Core questions

• प्रोग्राम सिमेंटिक्स को एक संगणनीय डोमेन में सुदृढ़ तरीके से कैसे अनुमानित किया जा सकता है?
• कंक्रीट और एब्स्ट्रैक्ट दुनिया को संबंधित करने में गैलोज़ कनेक्शन क्या भूमिका निभाते हैं?
• वाइडनिंग और नैरोइंग यह कैसे सुनिश्चित करते हैं कि फिक्सपॉइंट गणना समाप्त हो जाए?
• एब्स्ट्रैक्ट डोमेन के चुनाव के माध्यम से दक्षता के मुकाबले सटीकता को कैसे संतुलित किया जाता है?

Key theories

एब्स्ट्रैक्ट इंटरप्रिटेशन का लैटिस मॉडल

कौसोट और कौसोट का 1977 का फ्रेमवर्क स्टैटिक विश्लेषण को एक लैटिस में प्रोग्राम के सिमेंटिक्स के फिक्सपॉइंट्स के अनुमान के रूप में औपचारिक रूप देता है, जिसमें एब्स्ट्रैक्शन संबंध से सुदृढ़ता प्राप्त होती है।

विश्लेषण फ्रेमवर्क का व्यवस्थित डिज़ाइन

कौसोट्स का 1979 का काम दिखाता है कि गैलोज़ कनेक्शन के माध्यम से सही-बाय-कंस्ट्रक्शन विश्लेषण कैसे प्राप्त किया जाए और वाइडनिंग और नैरोइंग ऑपरेटरों का परिचय देता है जो अनंत-ऊंचाई वाले डोमेन पर समाप्ति की गारंटी देते हैं।

औद्योगिक-पैमाने पर एब्स्ट्रैक्ट इंटरप्रिटेशन

ASTRÉE एनालाइज़र ने बड़े सुरक्षा-महत्वपूर्ण एवियोनिक्स सॉफ्टवेयर में रनटाइम त्रुटियों की अनुपस्थिति को साबित करने के लिए विशेष एब्स्ट्रैक्ट डोमेन के साथ एब्स्ट्रैक्ट इंटरप्रिटेशन लागू किया।

Clinical relevance

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

History

पैट्रिक और राधिया कौसोट ने 1977 में एब्स्ट्रैक्ट इंटरप्रिटेशन की शुरुआत की और 1979 में इसकी व्यवस्थित-डिज़ाइन पद्धति विकसित की, जिसमें वाइडनिंग और नैरोइंग शामिल थे। ऑक्टागन और पॉलीहेड्रा जैसे एब्स्ट्रैक्ट डोमेन इसके बाद आए, और 2000 के दशक की शुरुआत में ASTRÉE एनालाइज़र ने एवियोनिक्स सॉफ्टवेयर पर औद्योगिक पैमाने पर इस सिद्धांत का प्रदर्शन किया।

Debates

एब्स्ट्रैक्ट डोमेन का चुनाव और सटीकता का नुकसान

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

Key figures

• Patrick Cousot
• Radhia Cousot
• Antoine Miné
• Bruno Blanchet

Seminal works

• cousot1977
• cousot1979
• blanchet2003

Frequently asked questions

एब्स्ट्रैक्ट डोमेन क्या है?

एक एब्स्ट्रैक्ट डोमेन कंक्रीट प्रोग्राम अवस्थाओं के सेट का एक सरलीकृत, संगणनीय प्रतिनिधित्व है, जैसे कि अंतराल या चर के बीच संबंध, जिसमें विश्लेषण व्यवहार के सुदृढ़ ओवर-अनुमानों की गणना करता है।

वाइडनिंग ऑपरेटरों की आवश्यकता क्यों है?

अनंत या ऊंचे एब्स्ट्रैक्ट डोमेन पर, भोली फिक्सपॉइंट पुनरावृति समाप्त नहीं हो सकती है; एक वाइडनिंग ऑपरेटर जानबूझकर अभिसरण को मजबूर करने के लिए ओवर-अनुमान लगाता है, जिसके बाद नैरोइंग कुछ सटीकता को पुनः प्राप्त कर सकता है।