Döngü değişmezi - Loop invariant

Gelen bilgisayar bilimleri , bir döngü değişkeni bir özelliğidir programı döngü her tekrarında önce (ve sonrası) doğrudur. Bu , bazen kod içinde bir onaylama çağrısıyla kontrol edilen mantıksal bir iddiadır . Bir döngünün etkisini anlamak için değişmezlerini bilmek esastır.

Olarak resmi program doğrulama , özellikle Floyd-Hoare yaklaşım , döngü değişmezleri resmi ile ifade edilir yüklem mantığı ve ilmeklerin özellikleri ve uzantı ile kanıtlamak için kullanılan algoritmalar istihdam döngüler (genellikle bu doğruluk özellikleri). Döngü değişmezleri, bir döngüye girişte ve her yinelemeden sonra doğru olacaktır, böylece döngüden çıkışta hem döngü değişmezleri hem de döngü sonlandırma koşulu garanti edilebilir.

Bir programlama metodolojisi bakış açısından, döngü değişmezi, bu uygulamanın ayrıntılarının ötesinde döngünün daha derindeki amacını karakterize eden, döngünün daha soyut bir özelliği olarak görülebilir. Bir anket makalesi, bilgisayar biliminin birçok alanından (arama, sıralama, optimizasyon, aritmetik vb.) temel algoritmaları kapsar ve her birini değişmezi açısından karakterize eder.

Döngüler ve özyinelemeli programların benzerliği nedeniyle, döngülerin kısmi doğruluğunu değişmezlerle kanıtlamak, özyinelemeli programların doğruluğunu tümevarım yoluyla kanıtlamaya çok benzer . Aslında, döngü değişmezi, belirli bir döngüye eşdeğer özyinelemeli bir program için kanıtlanacak endüktif hipotezle genellikle aynıdır.

resmi olmayan örnek

Aşağıdaki C alt yordamı , uzunluğunun en az 1 olması koşuluyla max(), bağımsız değişken dizisindeki maksimum değeri döndürür . Açıklamalar 3, 6, 9, 11 ve 13. satırlarda sağlanır. Her yorum, bir veya daha fazla değişkenin değerleri hakkında bir iddiada bulunur. fonksiyonun bu aşamasında. Döngünün başında ve sonunda (6. ve 11. satırlar) döngü gövdesi içinde vurgulanan iddialar tamamen aynıdır. Böylece döngünün değişmez bir özelliğini tanımlarlar. 13. satıra ulaşıldığında, bu değişmez hala geçerlidir ve 5. satırdaki döngü koşulunun yanlış olduğu bilinmektedir . Her iki özellik birlikte bunun içindeki maksimum değere eşit olduğunu, yani 14. satırdan doğru değerin döndürüldüğünü ima eder . a[]ni!=nma[0...n-1]

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;
}

Savunmacı bir programlama paradigmasının ardından , gayri meşru negatif değerler için sonsuz döngüden kaçınmak i!=niçin 5. satırdaki döngü koşulu olarak değiştirilmelidir . Koddaki bu değişiklik sezgisel olarak bir fark yaratmasa da, doğruluğuna götüren mantık biraz daha karmaşık hale gelir, çünkü o zaman sadece 13. satırda bilinir. Bunu da elde etmek için , bu koşulun döngüye dahil edilmesi gerekir. değişmez. 6. satırdaki (değiştirilmiş) döngü koşulundan 5. satırdaki (değiştirilmiş) döngü koşulundan elde edilebildiğinden ve dolayısıyla satır 10'da artırıldıktan sonra 11. satırda tutulduğundan , 'nin de döngünün bir değişmezi olduğunu görmek kolaydır . döngü değişmezlerinin resmi program doğrulaması için manuel olarak sağlanması gerektiğinde, bu tür sezgisel olarak çok açık özellikler genellikle göz ardı edilir. i<nni>=ni<=ni<=ni<ni<=nii<=n

Floyd-Hoare mantığı

In Floyd-Hoare mantığı , kısmi doğruluğu a while döngüsünün çıkarsama aşağıdaki kural tarafından yönetilir:

${\displaystyle {\frac {\{C\land I\}\;\mathrm {body} \;\{I\}}{\{I\}\;{\mathtt {while}}\ (C)\ \mathrm {body} \;\{\C\land I değil\}}}}$

Bu şu anlama gelir:

• Bazı özellik ise bir kod tarafından korunur tam -daha, eğer bir yürütülmesinden sonra tutar hem zaman Cı ve ı beforehand- tutulan (üst çizgi) , sonra${\displaystyle \mathrm {vücut} }$${\displaystyle \mathrm {vücut} }$
• Döngüden (alt satır) önce doğru olmam koşuluyla , tüm döngünün yürütülmesinden sonra C ve I'in sırasıyla false ve true olması garanti edilir .${\displaystyle {\mathtt {while}}\ (C)\ \mathrm {vücut} }$

Başka bir deyişle: Yukarıdaki kural, Hoare üçlüsünün öncülü olan tümdengelimli bir adımdır . Bu üçlü aslında makine durumlarıyla ilgili bir ilişkidir . Boole ifadesinin doğru olduğu bir durumdan başlayarak ve adlı bir kodu başarıyla yürüttüğünde , makine I'in doğru olduğu bir durumda biter . Bu ilişki kanıtlanabilirse, kural, programın başarılı bir şekilde yürütülmesinin, I'in doğru olduğu bir durumdan, geçerli olduğu bir duruma yol açacağı sonucuna varmamızı sağlar. Bu kuraldaki boole formülü I'e döngü değişmezi denir. ${\displaystyle \{C\land I\}\;\mathrm {body} \;\{I\}}$${\ Displaystyle C\land I}$${\displaystyle \mathrm {vücut} }$${\displaystyle {\mathtt {while}}\ (C)\ \mathrm {vücut} }$${\displaystyle \l değil C\land I}$

Örnek

Aşağıdaki örnek, bu kuralın nasıl çalıştığını gösterir. Programı düşünün

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

Daha sonra aşağıdaki Hoare üçlüsü kanıtlanabilir:

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

Durum Cı arasında whiledöngü olup . Kullanışlı bir döngü değişmezi I tahmin edilmelidir; uygun olduğu ortaya çıkacaktır . Bu varsayımlar altında aşağıdaki Hoare üçlüsünü kanıtlamak mümkündür: ${\görüntüleme stili x<10}$${\displaystyle x\leq 10}$

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

Bu üçlü, atamayı yöneten Floyd-Hoare mantığının kurallarından resmi olarak türetilebilse de, aynı zamanda sezgisel olarak da doğrulanır: Hesaplama , doğru olan bir durumda başlar , bu da basitçe bunun doğru olduğu anlamına gelir . Hesaplama 1'e x ekler , bu da bunun hala doğru olduğu anlamına gelir (x tamsayı için). ${\displaystyle x<10\land x\leq 10}$${\görüntüleme stili x<10}$${\displaystyle x\leq 10}$

Bu öncül altında, whiledöngü kuralı aşağıdaki sonuca izin verir:

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

Ancak sonrası durum ( x veya 10'a eşit azdır, ancak en az 10 olan) 'dir mantıksal olarak eşdeğer için biz göstermek istediğim şey olan. ${\displaystyle \lnot (x<10)\land x\leq 10}$${\görüntüleme stili x=10}$

Özellik , örnek döngünün başka bir değişmezidir ve önemsiz özellik başka bir özelliktir . Yukarıdaki çıkarım kuralının önceki değişmez verimlere uygulanması . Bunu , biraz daha anlamlı olan değişmez verimlere uygulamak . ${\displaystyle 0\leq x}$${\displaystyle \mathrm {doğru} }$${\displaystyle \{0\leq x\}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}}$${\displaystyle \mathrm {doğru} }$${\displaystyle \{\mathrm {true} \}\;{\mathtt {while}}\ (x<10)\ x:=x+1\;\{10\leq x\}}$

Programlama dili desteği

Eyfel

Eyfel programlama dili döngü değişmezleri için doğal destek sağlar. Bir döngü değişmezi, bir sınıf değişmezi için kullanılanla aynı sözdizimiyle ifade edilir . Aşağıdaki örnekte x <= 10, döngü başlatmanın ardından ve döngü gövdesinin her yürütülmesinden sonra döngü değişmez ifadesi doğru olmalıdır; bu çalışma zamanında kontrol edilir.

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

süre

Whiley programlama dili de döngü değişmezleri için birinci sınıf destek sağlar. Döngü değişmezleri where, aşağıdaki şekilde gösterildiği gibi bir veya daha fazla yan tümce kullanılarak ifade edilir :

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()Fonksiyon, bir Integer dizideki büyük elemanı belirler. Bunun tanımlanabilmesi için dizinin en az bir eleman içermesi gerekir. Hedefşartlar arasında max()dönen bir değerdir gerektirir: (1) herhangi bir element daha küçük olmayan; ve (2) en az bir elemanla eşleşmesi. Döngü değişmezi where, her biri son koşuldaki bir tümceye karşılık gelen iki tümce aracılığıyla tümevarımsal olarak tanımlanır . Temel fark, döngü değişmezinin her bir yan tümcesinin sonucu geçerli öğeye ikadar doğru olarak tanımlaması, son koşulların ise sonucu tüm öğeler için doğru olarak tanımlamasıdır.

Döngü değişmezlerinin kullanımı

Bir döngü değişmezi aşağıdaki amaçlardan birine hizmet edebilir:

1. tamamen belgesel
2. bir onaylama çağrısı ile kod içinde kontrol edilecek
3. Floyd-Hoare yaklaşımına göre doğrulanacak

1. için, (örneğin bir doğal dil açıklama // m equals the maximum value in a[0...i-1]olarak yukarıda örnek yeterlidir).

2. için, C kitaplığı assert.h veya Eiffel'de yukarıda gösterilen invariantyan tümce gibi programlama dili desteği gereklidir . Çoğu zaman, çalışma zamanı denetimi bir derleyici veya çalışma zamanı seçeneği tarafından açılabilir (hata ayıklama çalıştırmaları için) ve kapatılabilir (üretim çalıştırmaları için).

3. için, genellikle yukarıda gösterilen Floyd-Hoare kuralına dayanan, belirli bir döngü kodunun aslında belirli bir döngü değişmezini/değişimlerini karşıladığını gösteren matematiksel kanıtları desteklemek için bazı araçlar mevcuttur .

Soyut yorumlama tekniği, verilen kodun döngü değişmezini otomatik olarak tespit etmek için kullanılabilir. Ancak, bu yaklaşım çok basit değişmezlerle sınırlıdır (örneğin, 0<=i && i<=n && i%2==0).

Döngü değişmez koddan farkı

Döngü değişmezi (döngü değişmez özelliği ), döngü değişmez kodundan ayırt edilmelidir ; "döngü değişmez" (isim) ile "döngü değişmez" (sıfat) arasında not alın. Döngü değişmez kodu, program semantiğini etkilemeden bir döngü gövdesinin dışına taşınabilen ifadelerden veya ifadelerden oluşur. Döngüsel değişmez kod hareketi adı verilen bu tür dönüşümler, programları optimize etmek için bazı derleyiciler tarafından gerçekleştirilir . Döngü ile değişmez bir kod örneği ( C programlama dilinde )

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

burada hesaplamalar x = y+zve x*xdöngüden önce hareket ettirilebilir, bu da eşdeğer, ancak daha hızlı bir programla sonuçlanır:

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

Buna karşılık, örneğin özellik 0<=i && i<=n, hem orijinal hem de optimize edilmiş program için bir döngü değişmezidir, ancak kodun bir parçası değildir, bu nedenle "onu döngüden çıkarmaktan" bahsetmek mantıklı değildir.

Döngüyle değişmez kod, karşılık gelen bir döngüyle değişmez özelliği indükleyebilir. Yukarıdaki örnek için, bunu görmenin en kolay yolu, döngü değişmez kodunun hem döngüden önce hem de döngü içinde hesaplandığı bir programı düşünmektir:

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

Bu kodun döngüden değişmez özelliği (x1==x2 && t1==x2*x2) || i==0, döngüden önce hesaplanan değerlerin, içinde hesaplananlarla aynı olduğunu gösterir (ilk yinelemeden önce hariç).

Ayrıca bakınız

• Değişmez (bilgisayar bilimi)
• Döngü değişmez kod hareketi
• Döngü varyantı
• while döngüsünün en zayıf önkoşulları

Referanslar

daha fazla okuma

• Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest ve Clifford Stein . Algoritmalara Giriş , İkinci Baskı. MIT Press ve McGraw-Hill, 2001. ISBN  0-262-03293-7 . Sayfa 17–19, bölüm 2.1: Ekleme sıralaması.
• David Gries'in fotoğrafı . " Döngü değişmezleri ve döngüler geliştirmek için standart bir strateji üzerine bir not . Bilgisayar Programlama Bilimi , cilt 2, s. 207–214. 1984.
• Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. " Program Evrimini Desteklemek için Muhtemel Program Değişmezlerini Dinamik Olarak Keşfetmek ." Uluslararası Yazılım Mühendisliği Konferansı , s. 213–224. 1999.
• Robert Paige. " Değişmeyenlerle Programlama ." IEEE Yazılımı , 3(1):56–69. Ocak 1986.
• Yanhong A. Liu, Scott D. Stoller ve Tim Teitelbaum . Verimli Hesaplama için Değişmezlerin Güçlendirilmesi . Bilgisayar Programlama Bilimi , 41(2):139-172. Ekim 2001.
• Michael Huth, Mark Ryan. " Bilgisayar Biliminde Mantık .", İkinci Baskı.