loop invariant چیست؟

اثبات درستی الگوریتم ها یک موضوع مهم در علوم کامپیوتر است.

loop invariant به معنای مستقل از حلقه و به عبارتی هر شرطی است که در ابتدای هر چرخش(iteration) مقدارش ثابت باشد.

به قطعه کد زیر دقت کنید:

for(int i=0;i<10;i++)
{
   //any statement(s)
}

حالا عبارت زیر را در نظر بگیرید:

i<100

همان طور که مشاهده می کنید این شرط در ابتدای هر بار چرخش مقدارش TRUE است. همین که این عبارت همواره مقدارش ثابت است برای loop invariant بودن کافی است. اما loop invariant ها کاربردی اساسی در اثبات(proof) درستی عملکرد حلقه ها دارند.
اگر شما به صحت کارکرد یک حلقه شک دارید کافی است به دنبال یک loop invariant  بگردید که ضامن درستی الگوریتم باشد.
به عنوان مثال الگوریتم insertion sort را در نظر بگیرید:

void InsertionSort( int* num)
{
     int i, j, key, n = num.length( );
     for(j = 1; j < n; j++)    // Start with 1 (not 0)
    {
           key = num[j];
           for(i = j - 1; (i >= 0) && (num[i] < key); i--) 
          {
                 num[i+1] = num[i];
          }
         num[i+1] = key;    //Put key into its proper location
     }
     return;
}

عملکرد این الگوریتم به این گونه است:

1. ده کارت شماره گذاری شده از یک تا ده به صورت نامرتب داریم.کارت ها را به دست بگیرید. فرض کنید می خواهیم کارت ها را به صورت صعودی مرتب کنیم.
2. فرض کنید کارت اول که در پیش روی شما قرار دارد در جای درست خود قرار گرفته است. البته این فرض چند ثانیه بیشتر دوام نمی آورد. این گونه انتزاع کنید که ما الان یک آرایه ی تک عضوی مرتب و یک آرایه ی نه عضوی نا مرتب داریم.
3. کارت دوم(نه الزاما کارت شماره ی دو- منظور دومین کارتی است که در دست شما قرار دارد به ترتیب از کارت رویی به کارت پشتی) را با کارت اول مقایسه کنید. اگر از کارت اول کوچک تر بود آن را به جای مناسب خود(که در این جا روی کارت اول است) منتقل کنید. و اگر کوچکتر نبود جای آن را عوض نکنید. حالا ما یک آرایه ی دوعضوی مرتب و یک آرایه ی هشت عضوی نامرتب داریم.
4. کارت سوم را بردارید و آن را در جای خود بگذارید. ممکن است روی کارت اول، بین کارت اول و دوم یا زیر کارت دوم(سر جای خودش) قرار گیرد. حال ما یک آرایه ی سه عضوی مرتب و یک آرایه ی هفت عضوی نامرتب داریم.
5. ...

در این جا loop variant به کار می آید. همان طور که شاهده می کنید در هر بار چرخش، ما یک آرایه ی مرتب j عضوی و یک آرایه ی نامرتب n-j عضوی(در این مثال n=10) داریم. اگر این رویه ادامه پیدا کند با افزایش j  ،قسمت مرتب شده به تمام آرایه سرایت پیدا می کند و تمام آرایه مرتب می شود. بنا براین ما یک loop variant کارا پیدا کرده ایم. کارایی آن در این است که اگر شرط زیر همواره برقرار باشد ما مطمئن می شویم که حلقه درست کار میکند و آرایه ی ما حتما مرتب می شود.

loopInvariant = mySubarrayIsSorted(j,num);//return false or true

اهمیت loop invariant به حدی است که در بعضی از زبان های برنامه نویسی دستور مشخصی برای آن وجود دارد مثل زبان برنامه نویسی Eiffel

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

-برگرفته از کتاب CLRS ویرایش 2 صفحه 17