Доказателство за коректността на алгоритъма чрез инварианти

Здравейте!Можете ли да обясните как да докажете коректността на алгоритъма с помощта на инварианти на цикъл.Да приемем линейно търсене: in:A[], u //масив, желан елемент out:i //индекс на елемент u в масив A begin i=0; for j:=1 to length(a) do if A[j]=u then i:=j end;

Инвариантът е логически израз, който е верен след всяко преминаване на тялото на цикъла (след изпълнението на фиксиран израз) и преди началото на цикъла, в зависимост от променливите, които се променят в тялото на цикъла.[3]

Инвариантите се използват в теорията на верификацията на програмата, за да се докаже коректността на изпълнението на цикъла. Процедурата за доказване на работоспособността на цикъла с помощта на инвариант е следната:

1. Доказано е, че изразът на инварианта е верен преди началото на цикъла. 2. Доказано е, че изразът на инварианта остава верен след изпълнението на тялото на цикъла; по този начин чрез индукция се доказва, че в края на цикъла инвариантът ще бъде изпълнен. 3. Доказано е, че ако инвариантът е верен, след края на цикъла променливите ще приемат точно стойностите, които трябва да бъдат получени (това е елементарно определено от израза на инварианта и известните крайни стойности на променливите, на които се основава условието за прекратяване на цикъла). , доказано на предишните етапи, недвусмислено показва, че цикълът ще бъде завършен за крайно време и ще даде желания резултат. Инвариантите се използват и при проектирането и оптимизирането на циклични алгоритми. Например, за да се уверите, че оптимизираният цикъл остава правилен, е достатъчно да докажете, че инвариантът на цикъла не е нарушен и условиетозавършването на цикъла е постижимо.

Концепцията за инвариант също се използва в обектно-ориентираното програмиране за обозначаване на последователно състояние на обект. Разбираемо е, че извикването на всеки метод оставя обекта в инвариантно състояние.

---