लूप इनवेरिएंट

For कंप्यूटर प्रोग्रामिंग अनुकूलन तकनीक, see लूप-अपरिवर्तनीय कोड गति.

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

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

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

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

अनौपचारिक उदाहरण

निम्नलिखित C (प्रोग्रामिंग भाषा) सबरूटीन max() अपने तर्क सरणी a[] में अधिकतम मान लौटाता है, इसकी लंबाई प्रदान की गई n कम से कम 1 हो। टिप्पणियाँ पंक्तियों 3, 6, 9, 11 और 13 पर प्रदान की जाती हैं। प्रत्येक टिप्पणी फलन के उस चरण में एक या अधिक चर के मूल्यों के बारे में सत्यापन करती है। लूप बॉडी के अन्दर, लूप के प्रारंभ और अंत में हाइलाइट किए गए प्रमाण (पंक्तियाँ 6 और 11), बिल्कुल समान हैं। इस प्रकार वे लूप की एक अपरिवर्तनीय गुण का वर्णन करते हैं। जब पंक्ति 13 पर पहुँच जाता है, तब भी यह अपरिवर्तनीय रहता है, और यह ज्ञात होता है कि पंक्ति 5 से लूप की स्थिति i!=n असत्य हो गयी है। दोनों गुण मिलकर यही दर्शाते हैं कि m में अधिकतम मान a[0...n-1] के बराबर है, अर्थात्, पंक्ति 14 से सही मान लौटाया जाता है।

<सिंटैक्सहाइलाइट लैंग= सी लाइन हाइलाइट= 6,11 >

int max(int ​​n, const int a[]) {

int max(int n, const int a[]) {
    int m = a[0];
    // m equals the maximum value in a[0...0]
    int i = 1;
    while (i != n) {
        // m equals the maximum value in a[0...i-1]
        if (m < a[i])
            m = a[i];
        // m equals the maximum value in a[0...i]
        ++i;
        // m equals the maximum value in a[0...i-1]
    }
    // m equals the maximum value in a[0...i-1], and i==n
    return m;
}

   int m = a[0];
   // m a[0...0] में अधिकतम मान के बराबर है
   पूर्णांक मैं = 1;
   जबकि (i != n) {
       // m a[0...i-1] में अधिकतम मान के बराबर है
       अगर (एम < ए[i])
           एम = ए[आई];
       // m a[0...i] में अधिकतम मान के बराबर है
       ++मैं;
       // m a[0...i-1] में अधिकतम मान के बराबर है
   }
   // m a[0...i-1] में अधिकतम मान के बराबर है, और i==n
   वापसी एम;

} </सिंटैक्सहाइलाइट>

रक्षात्मक प्रोग्रामिंग प्रतिमान का पालन करते हुए, पंक्ति 5 में लूप स्थिति i!=n को बेहतर ढंग से i<n संशोधित किया जाना चाहिए, जिससे n के अवैध नकारात्मक मूल्यों के लिए अंतहीन लूपिंग से बचा जा सके। चूँकि सहज रूप से कोड में इस परिवर्तन से कोई फर्क नहीं पड़ना चाहिए, लेकिन इसके सही होने की ओर ले जाने वाला तर्क कुछ अधिक जटिल हो जाता है, तभी से पंक्ति 13 में केवल i>=n ज्ञात है। इसे प्राप्त करने के लिए i<=n का भी मानना है, स्थिति को लूप इनवेरिएंट में सम्मिलित करना होगा। यह देखना सरल है कि i<=n भी लूप का एक अपरिवर्तनीय है, क्योंकि पंक्ति 6 में i<n पंक्ति 5 में (संशोधित) लूप स्थिति से प्राप्त किया जा सकता है, और इसलिए i<=n पंक्ति में रहता है, 11 के बाद i को पंक्ति 10 में बढ़ा दिया गया है। चूँकि, जब औपचारिक कार्यक्रम सत्यापन के लिए लूप इनवेरिएंट को मैन्युअल रूप से प्रदान करना पड़ता है, तो i<=n जैसे सहज रूप से स्पष्ट गुणों को अधिकांशतः अनदेखा कर दिया जाता है।

फ्लोयड-होरे तर्क

फ्लोयड-होरे तर्क, थोड़ी देर के लूप की आंशिक शुद्धता अनुमान के निम्नलिखित नियम द्वारा नियंत्रित होती है:

${\frac {\{C\land I\}\;\mathrm {body} \;\{I\}}{\{I\}\;{\mathtt {while}}\ (C)\ \mathrm {body} \;\{\lnot C\land I\}}}$

इसका अर्थ यह है:

• यदि कुछ गुण I को कोड $\mathrm {body}$ द्वारा संरक्षित किया जाता है -अधिक स्पष्ट रूप से, यदि I $\mathrm {body}$ के निष्पादन के बाद धारण करता है, जब भी दोनों C और I पहले से होल्ड करते हैं - (ऊपरी पंक्ति) फिर
• C और I पूरे लूप के निष्पादन के बाद क्रमशः असत्य और सत्य होने की गारंटी ${\mathtt {while}}\ (C)\ \mathrm {body}$ है, बशर्ते I लूप (निचली रेखा) से पहले सत्य था।

दूसरे शब्दों में: उपरोक्त नियम एक निगमनात्मक चरण है, जिसका आधार $\{C\land I\}\;\mathrm {body} \;\{I\}$ होरे ट्रिपल है। यह त्रिगुण वास्तव में मशीन अवस्थाओं पर एक संबंध (गणित) है। यह तब भी प्रयुक्त होता है, जब बूलियन अभिव्यक्ति एक ऐसी स्थिति से प्रारंभ होती है, $C\land I$ सत्य है और कुछ कोड $\mathrm {body}$ को सफलतापूर्वक निष्पादित कर रहा है, मशीन ऐसी स्थिति में समाप्त हो जाती है I क्या सच है। यदि यह संबंध सिद्ध किया जा सकता है, तो नियम ${\mathtt {while}}\ (C)\ \mathrm {body}$ हमें कार्यक्रम के सफल निष्पादन का निष्कर्ष निकालने की अनुमति देता है, जिस स्थिति से नेतृत्व करेंगे I उस स्थिति के लिए सत्य है जिसमें $\lnot C\land I$ धारण करता है। बूलियन सूत्र I नियम को लूप इनवेरिएंट कहा जाता है।

प्रयुक्त संकेतन में कुछ भिन्नताओं के साथ, और इस आधार पर कि लूप रुक जाता है, इस नियम को अपरिवर्तनीय संबंध प्रमेय के रूप में भी जाना जाता है। जैसा कि 1970 के दशक की एक पाठ्यपुस्तक इसे छात्र प्रोग्रामरों के लिए सुलभ बनाने की विधियों से प्रस्तुत करती है:

मान लीजिए कि संकेतन P { seq } Q का अर्थ है कि यदि कथनों के क्रम seq चलने से पहले P सत्य है, तो उसके बाद Q सच है। तब अपरिवर्तनीय संबंध प्रमेय यही मानता है

P & c { seq } P

तात्पर्य

P { DO WHILE (c); seq END; } P & ¬c

उदाहरण

निम्नलिखित उदाहरण दिखाता है कि यह नियम कैसे काम करता है। कार्यक्रम पर विचार करें

while (x < 10)
    x := x+1;

फिर कोई निम्नलिखित होरे ट्रिपल को प्रमाणित कर सकता है:

$\{x\leq 10\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{x=10\}$

while लूप की C स्थिति $x<10$ है। I उपयोगी लूप अपरिवर्तनीय का अनुमान लगाना होगा; इससे पता चलेगा कि $x\leq 10$ उपयुक्त है। इन धारणाओं के अनुसार निम्नलिखित होरे ट्रिपल को प्रमाणित करना संभव है:

$\{x<10\land x\leq 10\}\;x:=x+1\;\{x\leq 10\}$

चूँकि इस ट्रिपल को औपचारिक रूप से फ्लोयड-होरे लॉजिक गवर्निंग असाइनमेंट के नियमों से प्राप्त किया जा सकता है, यह सहज रूप से उचित भी है: गणना उस स्थिति में शुरू होती है जहां $x<10\land x\leq 10$ सत्य है, जिसका सीधा सा अर्थ है, $x<10$ क्या सच है। x की गणना में 1 जोड़ा जाता है, जिसका अर्थ है कि $x\leq 10$ अभी भी सत्य है (पूर्णांक x के लिए)।

इस आधार के अंतर्गत, नियम के लिए while लूप्स निम्नलिखित निष्कर्ष की अनुमति देता है:

$\{x\leq 10\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{\lnot (x<10)\land x\leq 10\}$

चूँकि, बाद की स्थिति $\lnot (x<10)\land x\leq 10$ (x 10 से कम या उसके बराबर है, लेकिन यह 10 से कम नहीं है) तार्किक तुल्यता $x=10$ है, जो हम दिखाना चाहते थे।

गुण $0\leq x$ उदाहरण लूप का एक और अपरिवर्तनीय और तुच्छ गुण है $\mathrm {true}$ एक और है।

उपरोक्त अनुमान नियम को पूर्व अपरिवर्तनीय पैदावार पर प्रयुक्त करना $\{0\leq x\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$. इसे अपरिवर्तनीय पर प्रयुक्त करना $\mathrm {true}$ पैदावार $\{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}$, जो थोड़ा अधिक अभिव्यंजक है।

प्रोग्रामिंग भाषा समर्थन

एफिल

एफिल (प्रोग्रामिंग भाषा) प्रोग्रामिंग भाषा लूप इनवेरिएंट के लिए मूल समर्थन प्रदान करती है। एक लूप इनवेरिएंट को वर्ग अपरिवर्तनीय के लिए उपयोग किए गए समान सिंटैक्स के साथ व्यक्त किया जाता है। नीचे दिए गए नमूने में, लूप अपरिवर्तनीय अभिव्यक्ति x <= 10 लूप आरंभीकरण के बाद और लूप बॉडी के प्रत्येक निष्पादन के बाद सत्य होना चाहिए; इसे रनटाइम पर जांचा जाता है।

    from
        x := 0
    invariant
        x <= 10
    until
        x > 10
    loop
        x := x + 1
    end

जबकि

वाइली (प्रोग्रामिंग भाषा) प्रोग्रामिंग भाषा लूप इनवेरिएंट के लिए प्रथम श्रेणी का समर्थन भी प्रदान करती है। लूप इनवेरिएंट को एक या अधिक का उपयोग करके व्यक्त किया जाता है where उपवाक्य, जैसा कि निम्नलिखित में दर्शाया गया है:

function max(int[] items) -> (int r)
// Requires at least one element to compute max
requires |items| > 0
// (1) Result is not smaller than any element
ensures all { i in 0..|items| | items[i] <= r }
// (2) Result matches at least one element
ensures some { i in 0..|items| | items[i] == r }:
    //
    nat i = 1
    int m = items[0]
    //
    while i < |items|
    // (1) No item seen so far is larger than m
    where all { k in 0..i | items[k] <= m }
    // (2) One or more items seen so far matches m
    where some { k in 0..i | items[k] == m }:
        if items[i] > m:
            m = items[i]
        i = i + 1
    //
    return m

max() e> फलन पूर्णांक सरणी में सबसे बड़ा तत्व निर्धारित करता है। इसे परिभाषित करने के लिए, सरणी में कम से कम एक तत्व होना चाहिए। के बाद के नियम max() आवश्यक है कि लौटाया गया मान है: (1) किसी भी तत्व से छोटा नहीं; और, (2) कि यह कम से कम एक तत्व से मेल खाता हो। लूप इनवेरिएंट को दो के माध्यम से आगमनात्मक रूप से परिभाषित किया गया है where खंड, जिनमें से प्रत्येक पोस्टकंडीशन में एक खंड से मेल खाता है। मूलभूत अंतर यह है कि लूप इनवेरिएंट का प्रत्येक खंड परिणाम को वर्तमान तत्व तक सही होने की पहचान करता है i, जबकि पोस्टकंडिशन परिणाम को सभी तत्वों के लिए सही होने की पहचान करता है।

लूप इनवेरिएंट का उपयोग

एक लूप इनवेरिएंट निम्नलिखित उद्देश्यों में से एक को पूरा कर सकता है:

1. विशुद्ध रूप से वृत्तचित्र
2. को कोड के अन्दर जांचा जाना चाहिए, उदा. एक अभिकथन कॉल द्वारा
3. होरे तर्क|फ्लोयड-होरे दृष्टिकोण के आधार पर सत्यापित किया जाना है

1. के लिए, एक प्राकृतिक भाषा टिप्पणी (जैसे // m equals the maximum value in a[0...i-1] #अनौपचारिक उदाहरण उदाहरण में) पर्याप्त है।

2. के लिए, प्रोग्रामिंग भाषा समर्थन की आवश्यकता है, जैसे C (प्रोग्रामिंग भाषा) लाइब्रेरी assert.h, या एफिल-दिखाया गया invariant एफिल में खंड. अधिकांशतः, कंपाइलर या रनटाइम विकल्प द्वारा रन-टाइम चेकिंग को प्रारंभ (डिबगिंग रन के लिए) और बंद (प्रोडक्शन रन के लिए) किया जा सकता है।

3. के लिए, गणितीय प्रमाणों का समर्थन करने के लिए कुछ उपकरण उपस्थित हैं, जो सामान्यतः फ्लोयड-होरे तर्क-दिखाए गए फ़्लॉइड-होरे नियम पर आधारित होते हैं, कि एक दिया गया लूप कोड वास्तव में दिए गए (सेट) लूप इनवेरिएंट को संतुष्ट करता है।

अमूर्त व्याख्या की तकनीक का उपयोग दिए गए कोड के लूप इनवेरिएंट का स्वचालित रूप से पता लगाने के लिए किया जा सकता है। चूँकि, यह दृष्टिकोण बहुत ही सरल अपरिवर्तनीयों तक ही सीमित है (जैसे 0<=i && i<=n && i%2==0)।

लूप-अपरिवर्तनीय कोड से अंतर

Further information: लूप-अपरिवर्तनीय कोड गति

लूप-इनवेरिएंट कोड में ऐसे कथन या अभिव्यक्ति सम्मिलित होते हैं जिन्हें प्रोग्राम शब्दार्थ को प्रभावित किए बिना लूप बॉडी के बाहर ले जाया जा सकता है। ऐसे परिवर्तन, जिन्हें लूप-अपरिवर्तनीय कोड गति कहा जाता है, कुछ कंपाइलरों द्वारा कंपाइलर प्रोग्राम को अनुकूलित करने के लिए किए जाते हैं। एक लूप-इनवेरिएंट कोड उदाहरण (C (प्रोग्रामिंग भाषा) में) है

for (int i=0; i<n; ++i) {
    x = y+z;
    a[i] = 6*i + x*x;
}

जहां गणना x = y+z और x*x लूप से पहले ले जाया जा सकता है, जिसके परिणामस्वरूप एक समतुल्य, लेकिन तेज़ प्रोग्राम बनता है:

x = y+z;
t1 = x*x;
for (int i=0; i<n; ++i) {
    a[i] = 6*i + t1;
}

इसके विपरीत, उदा. गुण 0<=i && i<=n मूल और अनुकूलित प्रोग्राम दोनों के लिए एक लूप अपरिवर्तनीय है, लेकिन यह कोड का हिस्सा नहीं है, इसलिए इसे लूप से बाहर ले जाने की बात करने का कोई अर्थ नहीं है।

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

x1 = y+z;
t1 = x1*x1;
for (int i=0; i<n; ++i) {
    x2 = y+z;
    a[i] = 6*i + t1;
}

इस कोड की एक लूप-अपरिवर्तनीय गुण (x1==x2 && t1==x2*x2) || i==0 है, यह दर्शाता है कि लूप से पहले गणना किए गए मान अन्दर गणना किए गए मानों से सहमत हैं (पहले पुनरावृत्ति से पहले को छोड़कर)।

यह भी देखें

• अपरिवर्तनीय (कंप्यूटर विज्ञान)
• लूप-अपरिवर्तनीय कोड गति
• लूप वैरिएंट
• विधेय ट्रांसफार्मर शब्दार्थ व्हाइल लूप की सबसे कमजोर-पूर्व नियम

अग्रिम पठन

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms, Second Edition. MIT Press and McGraw-Hill, 2001. ISBN 0-262-03293-7. Pages 17–19, section 2.1: Insertion sort.
• David Gries. "A note on a standard strategy for developing loop invariants and loops." Science of Computer Programming, vol 2, pp. 207–214. 1984.
• Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. "Dynamically Discovering Likely Program Invariants to Support Program Evolution." International Conference on Software Engineering, pp. 213–224. 1999.
• Robert Paige. "Programming with Invariants." IEEE Software, 3(1):56–69. January 1986.
• Yanhong A. Liu, Scott D. Stoller, and Tim Teitelbaum. Strengthening Invariants for Efficient Computation. Science of Computer Programming, 41(2):139–172. October 2001.
• Michael Huth, Mark Ryan. "Logic in Computer Science.", Second Edition.