टाइपस्टेट विश्लेषण

From Vigyanwiki
Revision as of 10:31, 16 June 2023 by alpha>Indicwiki (Created page with "{{Short description|Validates computer program operations}} टाइपस्टेट विश्लेषण, जिसे कभी-कभी प्रोटोकॉल...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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

टाइपस्टेट व्यवहार प्रकार के परिशोधन का प्रतिनिधित्व करने में सक्षम हैं जैसे कि विधि ए को विधि बी से पहले लागू किया जाना चाहिए, और विधि सी को बीच में लागू नहीं किया जा सकता है। टाइपस्टेट्स उन संसाधनों का प्रतिनिधित्व करने के लिए उपयुक्त हैं जो ओपन/क्लोज़ सेमेन्टिक्स का उपयोग शब्दार्थिक रूप से मान्य अनुक्रमों को लागू करके करते हैं जैसे कि ओपन फिर क्लोज अमान्य अनुक्रमों के विपरीत जैसे कि एक खुली स्थिति में फ़ाइल छोड़ना। ऐसे संसाधनों में फ़ाइल सिस्टम तत्व, लेन-देन, कनेक्शन और प्रोटोकॉल शामिल हैं। उदाहरण के लिए, डेवलपर्स यह निर्दिष्ट करना चाह सकते हैं कि फ़ाइलों या सॉकेट्स को पढ़ने या लिखे जाने से पहले खोला जाना चाहिए, और अगर उन्हें बंद कर दिया गया है तो उन्हें अब पढ़ा या लिखा नहीं जा सकता है। टाइपस्टेट नाम इस तथ्य से उपजा है कि इस प्रकार का विश्लेषण अक्सर प्रत्येक प्रकार की वस्तु को परिमित राज्य मशीन के रूप में मॉडल करता है। इस राज्य मशीन में, प्रत्येक राज्य में अनुमत विधियों/संदेशों का एक अच्छी तरह से परिभाषित सेट होता है, और विधि आमंत्रण राज्य संक्रमण का कारण बन सकता है। रिफाइनमेंट_टाइप के साथ उपयोग के लिए पेट्री डिश को संभावित व्यवहार मॉडल के रूप में भी प्रस्तावित किया गया है।[1] 1983 में रोब स्ट्रोम द्वारा टाइपस्टेट विश्लेषण पेश किया गया था[2] थॉमस जे. वॉटसन रिसर्च सेंटर | आईबीएम की वॉटसन लैब में विकसित नेटवर्क कार्यान्वयन भाषा (NIL) में। इसे 1986 के एक लेख में स्ट्रोम और येमिनी द्वारा औपचारिक रूप दिया गया था[3] यह वर्णन करता है कि टाइपस्टेट का उपयोग चर के आरंभीकरण की डिग्री को ट्रैक करने के लिए कैसे किया जाता है, यह गारंटी देता है कि अनुचित तरीके से आरंभिक डेटा पर संचालन कभी भी लागू नहीं किया जाएगा, और आगे हर्मीस (प्रोग्रामिंग भाषा) प्रोग्रामिंग भाषा में सामान्यीकृत किया जाएगा।

हाल के वर्षों में, विभिन्न अध्ययनों ने ऑब्जेक्ट-ओरिएंटेड भाषाओं में टाइपस्टेट अवधारणा को लागू करने के तरीके विकसित किए हैं।[4][5]


दृष्टिकोण

प्रकार के एक चर के आरंभीकरण से उत्पन्न होने वाली नॉनलाइनियर टाइपस्टेट जाली struct{int x;int y;int z;}.
न्यूनतम तत्व ⊥ राज्य के साथ मेल खाता है ∅ कोई संरचना घटक प्रारंभ नहीं हुआ है।

स्ट्रोम और येमिनी (1986) को किसी दिए गए प्रकार के आंशिक रूप से आदेशित होने के लिए टाइपस्टेट्स के सेट की आवश्यकता होती है, ताकि कुछ जानकारी को हटाकर एक निम्न टाइपस्टेट को उच्चतर से प्राप्त किया जा सके। उदाहरण के लिए, ए int C (प्रोग्रामिंग लैंग्वेज) में वेरिएबल में आमतौर पर टाइपस्टेट्स अनइनिशियलाइज़्ड <इनिशियलाइज़्ड होते हैं, और a FILE* पॉइंटर में टाइपस्टेट्स को आवंटित नहीं किया जा सकता है <आवंटित, लेकिन अप्रारंभीकृत <प्रारंभिक, लेकिन फ़ाइल नहीं खोली गई <फ़ाइल खोली गई। इसके अलावा, स्ट्रोम और येमिनी के लिए आवश्यक है कि प्रत्येक दो टाइपस्टेट्स की सबसे बड़ी निचली सीमा हो, यानी आंशिक क्रम एक मिलना-अर्ध-जाली भी हो; और यह कि प्रत्येक क्रम में एक न्यूनतम अवयव होता है, जिसे हमेशा ⊥ कहा जाता है।

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

int n;                // here, n has typestate "uninitialized"
if (...) {
    n = 5;            // here, n has typestate   "initialized"
} else {
    /*do nothing*/    // here, n has typestate "uninitialized"
}                     // here, n has typestate "uninitialized" = greatest_lower_bound("initialized","uninitialized")

हर बुनियादी ऑपरेशन[note 1] एक टाइपस्टेट ट्रांज़िशन से लैस होना चाहिए, यानी प्रत्येक पैरामीटर के लिए क्रमशः ऑपरेशन से पहले और बाद में आवश्यक और सुनिश्चित टाइपस्टेट। उदाहरण के लिए, एक ऑपरेशन fwrite(...,fd) आवश्यक है fd टाइपस्टेट फ़ाइल खोलने के लिए। अधिक सटीक रूप से, एक ऑपरेशन के कई 'परिणाम' हो सकते हैं, जिनमें से प्रत्येक को अपने स्वयं के टाइपस्टेट संक्रमण की आवश्यकता होती है। उदाहरण के लिए, सी कोड FILE *fd=fopen("foo","r") सेट fdफ़ाइल खोलने के लिए टाइपस्टेट खोला गया और आवंटित नहीं किया गया यदि उद्घाटन क्रमशः सफल होता है और विफल रहता है।

प्रत्येक दो टाइपस्टेट्स के लिए टी1 कवरिंग रिलेशन|<· टी2, एक अद्वितीय टाइपस्टेट जबरदस्ती ऑपरेशन प्रदान करने की आवश्यकता है, जो टाइपस्टेट टी की वस्तु पर लागू होने पर2, इसके टाइपस्टेट को t तक कम कर देता है1, संभवतः कुछ संसाधन जारी करके। उदाहरण के लिए, fclose(fd) चेकों fdफ़ाइल से टाइपस्टेट प्रारंभ करने के लिए खोला गया, लेकिन फ़ाइल नहीं खोली गई।

एक प्रोग्राम निष्पादन को 'टाइपस्टेट-करेक्ट' कहा जाता है यदि

  • प्रत्येक मूल ऑपरेशन से पहले, सभी मापदंडों में ऑपरेशन के टाइपस्टेट ट्रांज़िशन के लिए आवश्यक टाइपस्टेट होता है, और
  • कार्यक्रम समाप्ति पर, सभी चर टाइपस्टेट ⊥ में हैं।[note 2]

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

चुनौतियां

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

एक अन्य मुद्दे के रूप में, कुछ कार्यक्रमों के लिए, निष्पादन पथों को अभिसरण करने और संबंधित डाउन-कॉर्सियन संचालन को जोड़ने के लिए सबसे बड़ी निचली सीमा लेने की विधि अपर्याप्त प्रतीत होती है। उदाहरण के लिए, इससे पहले वापसी 1 निम्नलिखित कार्यक्रम में,[note 3] सभी घटक एक्स </ कोड>, वाई, और z का coord आरंभीकृत हैं, लेकिन स्ट्रोम और येमिनी का दृष्टिकोण इसे पहचानने में विफल रहता है, क्योंकि लूप बॉडी में एक स्ट्रक्चर कंपोनेंट के प्रत्येक इनिशियलाइज़ेशन को पहले लूप एंट्री के टाइपस्टेट को पूरा करने के लिए लूप री-एंट्री पर डाउन-कॉर्स्ड करना पड़ता है। , अर्थात। ⊥। एक संबंधित समस्या यह है कि इस उदाहरण में टाइपस्टेट ट्रांज़िशन के ओवरलोडिंग की आवश्यकता होगी; उदाहरण के लिए, parse_int_attr( x ,&coord->x) एक टाइपस्टेट को बदलता है कोई घटक x घटक के लिए आरंभीकृत नहीं होता है, बल्कि y घटक को x और y घटक के लिए आरंभीकृत किया जाता है। 

int parse_coord(struct { int x; int y; int z; } *coord) {
    int seen = 0;     /* remember which attributes have been parsed */

    while (1)
        if      (parse_int_attr("x", &coord->x)) seen |= 1;
        else if (parse_int_attr("y", &coord->y)) seen |= 2;
        else if (parse_int_attr("z", &coord->z)) seen |= 4;
        else break;

    if (seen != 7)    /* some attribute missing, fail */
        return 0;
    ...               /* all attributes present, do some computations and succeed */
    return 1;
}


टाइपस्टेट अनुमान

कार्यक्रमों (या अनुबंधों जैसे अन्य कलाकृतियों) से टाइपस्टेट्स का अनुमान लगाने के लिए कई दृष्टिकोण हैं। उनमें से कई संकलन समय पर टाइपस्टेट्स का अनुमान लगा सकते हैं [6][7][8][9] और अन्य मॉडल को गतिशील रूप से माइन करते हैं।[10][11][12][13][14][15]


टाइपस्टेट का समर्थन करने वाली भाषाएं

टाइपस्टेट एक प्रायोगिक अवधारणा है जो अभी तक मुख्यधारा की प्रोग्रामिंग भाषाओं में पार नहीं हुई है। हालांकि, कई अकादमिक परियोजनाएं सक्रिय रूप से जांच करती हैं कि इसे दैनिक प्रोग्रामिंग तकनीक के रूप में और अधिक उपयोगी कैसे बनाया जाए। दो उदाहरण प्लेड और ओब्सीडियन भाषाएं हैं, जिन्हें कार्नेगी मेलन विश्वविद्यालय में जोनाथन एल्ड्रिच के समूह द्वारा विकसित किया जा रहा है।[16] [17] अन्य उदाहरणों में क्लारा शामिल हैं[18] भाषा अनुसंधान ढांचा, रस्ट (प्रोग्रामिंग भाषा) भाषा के पुराने संस्करण, और >> एटीएस (प्रोग्रामिंग भाषा) में कीवर्ड।[19]


यह भी देखें

टिप्पणियाँ

  1. ↑ these include language constructs, e.g. += in C, and standard library routines, e.g.fopen()
  2. ↑ This aims at ensuring that e.g. all files have been closed, and all malloced memory has been freed. In most programming languages, a variable's lifetime may end before program termination; the notion of typestate-correctness has then to be sharpened accordingly.
  3. ↑ assuming that int parse_int_attr(const char *name,int *val) initializes *val whenever it succeeds


संदर्भ

  1. ↑ Jorge Luis Guevara D´ıaz (2010). "टाइपस्टेट उन्मुख डिजाइन - एक रंगीन पेट्री नेट दृष्टिकोण" (PDF).
  2. ↑ Strom, Robert E. (1983). "Mechanisms for compile-time enforcement of security". Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '83. pp. 276–284. doi:10.1145/567067.567093. ISBN 0897910907.
  3. ↑ Strom, Robert E.; Yemini, Shaula (1986). "Typestate: A programming language concept for enhancing software reliability" (PDF). IEEE Transactions on Software Engineering. IEEE. 12: 157–171. doi:10.1109/tse.1986.6312929.
  4. ↑ DeLine, Robert; Fähndrich, Manuel (2004). "वस्तुओं के लिए टाइपस्टेट्स". ECOOP 2004: Proceedings of the 18th European Conference on Object-Oriented Programming. Lecture Notes in Computer Science. Springer. 3086: 465–490. doi:10.1007/978-3-540-24851-4_21. ISBN 978-3-540-22159-3.
  5. ↑ Bierhoff, Kevin; Aldrich, Jonathan (2007). "अलियास्ड ऑब्जेक्ट्स की मॉड्यूलर टाइपस्टेट जाँच". OOPSLA '07: Proceedings of the 22nd ACM SIGPLAN Conference on Object-Oriented Programming: Systems, Languages and Applications. 42 (10): 301–320. doi:10.1145/1297027.1297050. ISBN 9781595937865.
  6. ↑ Guido de Caso, Victor Braberman, Diego Garbervetsky, and Sebastian Uchitel. 2013. Enabledness-based program abstractions for behavior validation. ACM Trans. Softw. Eng. Methodol. 22, 3, Article 25 (July 2013), 46 pages.
  7. ↑ R. Alur, P. Cerny, P. Madhusudan, and W. Nam. Synthesis of interface specifications for Java classes, 32nd ACM Symposium on Principles of Programming Languages, 2005
  8. ↑ Giannakopoulou, D., and Pasareanu, C.S., "Interface Generation and Compositional Verification in JavaPathfinder", FASE 2009.
  9. ↑ Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Permissive interfaces. Proceedings of the 13th Annual Symposium on Foundations of Software Engineering (FSE), ACM Press, 2005, pp. 31-40.
  10. ↑ Valentin Dallmeier, Christian Lindig, Andrzej Wasylkowski, and Andreas Zeller. 2006. Mining object behavior with ADABU. In Proceedings of the 2006 international workshop on Dynamic systems analysis (WODA '06). ACM, New York, NY, USA, 17-24
  11. ↑ Carlo Ghezzi, Andrea Mocci, and Mattia Monga. 2009. Synthesizing intensional behavior models by graph transformation. In Proceedings of the 31st International Conference on Software Engineering (ICSE '09). IEEE Computer Society, Washington, DC, USA, 430-440
  12. ↑ Mark Gabel and Zhendong Su. 2008. Symbolic mining of temporal specifications. In Proceedings of the 30th international conference on Software engineering (ICSE '08). ACM, New York, NY, USA, 51-60.
  13. ↑ Davide Lorenzoli, Leonardo Mariani, and Mauro Pezzè. 2008. Automatic generation of software behavioral models. In Proceedings of the 30th international conference on Software engineering (ICSE '08). ACM, New York, NY, USA, 501-510
  14. ↑ Ivan Beschastnikh, Yuriy Brun, Sigurd Schneider, Michael Sloan, and Michael D. Ernst. 2011. Leveraging existing instrumentation to automatically infer invariant-constrained models. In Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering (ESEC/FSE '11). ACM, New York, NY, USA, 267-277
  15. ↑ Pradel, M.; Gross, T.R., "Automatic Generation of Object Usage Specifications from Large Method Traces," Automated Software Engineering, 2009. ASE '09. 24th IEEE/ACM International Conference on , vol., no., pp.371,382, 16-20 Nov. 2009
  16. ↑ Aldrich, Jonathan. "प्लेड प्रोग्रामिंग भाषा". Retrieved 22 July 2012.
  17. ↑ Coblenz, Michael. "ओब्सीडियन प्रोग्रामिंग भाषा". Retrieved 16 February 2018.
  18. ↑ Bodden, Eric. "क्लारा". Retrieved 23 July 2012.
  19. ↑ Xi, Hongwei. "एटीएस में प्रोग्रामिंग का परिचय". Retrieved 20 April 2018.
Retrieved from ‘https://www.vigyanwiki.in/index.php?title=टाइपस्टेट_विश्लेषण&oldid=200541’