Niezmienniczość pętli — Loop invariant

W informatyce , o niezmienne pętla jest właściwością programu pętli , która jest prawdą przed (i po) każdej iteracji. Jest to asercja logiczna , czasami sprawdzana w kodzie przez wywołanie asercji . Znajomość jego niezmienników jest niezbędna do zrozumienia efektu pętli.

W formalnej weryfikacji programu , szczególnie w podejściu Floyda-Hoare'a , niezmienniki pętli są wyrażane przez formalną logikę predykatów i używane do dowodzenia własności pętli oraz przez algorytmy rozszerzające wykorzystujące pętle (zwykle własności poprawności ). Niezmienniki pętli będą prawdziwe przy wejściu do pętli i po każdej iteracji, dzięki czemu przy wyjściu z pętli można zagwarantować zarówno niezmienniki pętli, jak i warunek zakończenia pętli.

Z punktu widzenia metodologii programowania, niezmiennik pętli może być postrzegany jako bardziej abstrakcyjna specyfikacja pętli, która charakteryzuje głębszy cel pętli poza szczegółami tej implementacji. Artykuł ankietowy obejmuje podstawowe algorytmy z wielu dziedzin informatyki (przeszukiwanie, sortowanie, optymalizacja, arytmetyka itp.), charakteryzując każdy z nich z punktu widzenia jego niezmiennika.

Ze względu na podobieństwo pętli i programów rekurencyjnych dowodzenie częściowej poprawności pętli z niezmiennikami jest bardzo podobne do dowodzenia poprawności programów rekurencyjnych poprzez indukcję . W rzeczywistości niezmiennik pętli jest często taki sam, jak hipoteza indukcyjna, którą należy udowodnić dla programu rekurencyjnego równoważnego danej pętli.

Nieformalny przykład

Poniższy podprogram C zwraca maksymalną wartość w swojej tablicy argumentów , pod warunkiem, że jej długość wynosi co najmniej 1. Komentarze znajdują się w wierszach 3, 6, 9, 11 i 13. Każdy komentarz stanowi potwierdzenie wartości jednej lub więcej zmiennych na tym etapie funkcji. Podświetlone asercje w ciele pętli, na początku i na końcu pętli (linie 6 i 11), są dokładnie takie same. W ten sposób opisują niezmienną właściwość pętli. Po osiągnięciu linii 13 ten niezmiennik nadal obowiązuje i wiadomo, że warunek pętli z linii 5 stał się fałszywy. Obie właściwości razem oznaczają, że równa się wartości maksymalnej w , to znaczy, że poprawna wartość jest zwracana z wiersza 14. max()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;
}

Zgodnie z defensywnym paradygmatem programowania , warunek pętli i!=nw wierszu 5 powinien być lepiej zmodyfikowany do i<n, aby uniknąć niekończących się pętli dla niedozwolonych ujemnych wartości n. O ile ta zmiana w kodzie intuicyjnie nie powinna robić różnicy, to rozumowanie prowadzące do jego poprawności staje się nieco bardziej skomplikowane, ponieważ tylko wtedy i>=njest znane w wierszu 13. Aby to również było i<=nspełnione, warunek ten musi zostać włączony do pętli niezmienny. Łatwo zauważyć, że i<=n, również jest niezmiennikiem pętli, ponieważ i<nw linii 6 można uzyskać z (zmodyfikowanego) warunku pętli z linii 5, a zatem i<=nutrzymuje się w linii 11 po izwiększeniu w linii 10. Jednak, kiedy niezmienniki pętli muszą być wprowadzone ręcznie w celu formalnej weryfikacji programu, takie intuicyjnie zbyt oczywiste właściwości i<=nsą często pomijane.

Logika Floyda-Hoare'a

W logice Floyd- Hoare The częściowy poprawności z pętli reguluje następującej reguły wnioskowania:

${\displaystyle {\frac {\{C\land I\}\;\mathrm {ciało} \;\{ja\}}{\{ja\}\;{\mathtt {podczas}}\ (C)\ \mathrm {ciało} \;\{\lnie C\land I\}}}}$

To znaczy:

• Jeśli jakaś właściwość I jest zachowana przez kod — dokładniej, jeśli trzymam po wykonaniu, gdy zarówno C, jak i ja trzymaliśmy wcześniej — (górny wiersz), to${\displaystyle \mathrm {ciało}}$${\displaystyle \mathrm {ciało}}$
• C i I są gwarantowane odpowiednio jako fałsz i prawda po wykonaniu całej pętli , pod warunkiem, że przed pętlą (dolna linia) byłam prawdziwa .${\ Displaystyle {\ mathtt {podczas}} \ (C) \ \ operatorname {ciało}}$

Innymi słowy: powyższa reguła jest krokiem dedukcyjnym, którego założeniem jest trójka Hoare'a . Ta trójka jest właściwie relacją dotyczącą stanów maszyn. Przechowuje się, gdy zaczyna się od stanu, w którym wyrażenie logiczne jest prawdziwe i pomyślnie wykonuje kod o nazwie , maszyna kończy się w stanie, w którym I jest prawdziwe. Jeśli ta relacja może być udowodnione, reguła następnie pozwala nam stwierdzić, że pomyślne wykonanie programu będzie prowadzić od stanu, w którym ja jest prawdą do stanu, w którym przechowuje. Formuła logiczna I w tej regule nazywa się niezmiennikiem pętli. ${\displaystyle \{C\land I\}\;\mathrm {ciało} \;\{ja\}}$${\displaystyle C\land I}$${\displaystyle \mathrm {ciało}}$${\ Displaystyle {\ mathtt {podczas}} \ (C) \ \ operatorname {ciało}}$${\ Displaystyle \ nie C \ ziemia I}$

Przykład

Poniższy przykład ilustruje działanie tej reguły. Rozważ program

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

Można wtedy udowodnić następującą trójkę Hoare'a:

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

Warunek C w whilepętli . Przydatny niezmiennik pętli, muszę się domyślić; okaże się, że jest to właściwe. Przy tych założeniach możliwe jest udowodnienie następującej trójki Hoare'a: ${\displaystyle x<10}$${\displaystyle x\leq 10}$

${\displaystyle \{x<10\land x\równ 10\}\;x:=x+1\;\{x\równ 10\}}$

Chociaż tę trójkę można formalnie wyprowadzić z reguł logiki Floyd-Hoare rządzących przypisaniem, jest to również intuicyjnie uzasadnione: obliczenia rozpoczynają się w stanie, w którym jest prawdziwe, co oznacza po prostu, że jest prawdziwe. Obliczenie dodaje 1 do x , co oznacza, że nadal jest prawdziwe (dla liczby całkowitej x). ${\displaystyle x<10\ziemia x\leq 10}$${\displaystyle x<10}$${\displaystyle x\leq 10}$

Zgodnie z tym założeniem reguła whilepętli pozwala na następujący wniosek:

${\ Displaystyle \ {x \ leq 10 \} \; {\ mathtt {gdy}} \ (x <10) \ x: = x + 1 \; \ {\ nie (x < 10) \ ziemia x \ równoważnik 10 \}}$

Jednak warunek końcowy ( x jest mniejsze lub równe 10, ale nie jest mniejsze niż 10) jest logicznie równoważny z , co chcieliśmy pokazać. ${\ Displaystyle \ lnot (x <10) \ ziemia x \ równoważnik 10}$${\displaystyle x=10}$

Właściwość to kolejny niezmiennik pętli przykładowej, a właściwość trywialna to kolejna. Zastosowanie powyższej reguły wnioskowania do poprzednich niezmiennych plonów . Stosując go do niezmiennych plonów , co jest nieco bardziej wyraziste. ${\displaystyle 0\leq x}$${\displaystyle \mathrm {prawda}}$${\ Displaystyle \ {0 \ leq x \} \; {\ mathtt {gdy}} \ (x <10) \ x: = x + 1 \; \ {10 \ leq x \}}$${\displaystyle \mathrm {prawda}}$${\ Displaystyle \ {\ operatorname {prawda} \} \; {\ mathtt {gdy}} \ (x <10) \ x: = x + 1 \; \ {10 \ leq x \}}$

Obsługa języka programowania

Eiffla

Język programowania Eiffel zapewnia natywną obsługę niezmienników pętli. Niezmiennik pętli jest wyrażany przy użyciu tej samej składni, co niezmiennik klasy . W poniższym przykładzie wyrażenie niezmienne pętli x <= 10musi być prawdziwe po zainicjowaniu pętli i po każdym wykonaniu treści pętli; jest to sprawdzane w czasie wykonywania.

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

Chociaż

Język programowania Whiley zapewnia również pierwszorzędną obsługę niezmienników pętli. Niezmienniki pętli są wyrażane za pomocą co najmniej jednej whereklauzuli, jak pokazano poniżej:

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()Funkcji określa maksymalny element tablicy całkowitej. Aby to zostało zdefiniowane, tablica musi zawierać co najmniej jeden element. W postconditions z max()wymaga, by zwrócone wartość jest: (1) nie mniejsze niż elementu; oraz (2) że pasuje do co najmniej jednego elementu. Niezmiennik pętli jest definiowany indukcyjnie przez dwie whereklauzule, z których każda odpowiada klauzuli w warunku końcowym. Podstawowa różnica polega na tym, że każda klauzula niezmiennika pętli identyfikuje wynik jako poprawny aż do bieżącego elementu i, podczas gdy warunki końcowe identyfikują wynik jako poprawny dla wszystkich elementów.

Użycie niezmienników pętli

Niezmiennik pętli może służyć do jednego z następujących celów:

1. czysto dokumentalny
2. do sprawdzenia w kodzie przez wywołanie asercji
3. do weryfikacji w oparciu o podejście Floyd-Hoare

Dla 1. wystarczy komentarz w języku naturalnym (jak // m equals the maximum value in a[0...i-1]w powyższym przykładzie).

2. Informacje, programowanie obsługę języka jest wymagana, takich jak C biblioteki assert.h , lub powyżej -shown invariantklauzuli Eiffel. Często sprawdzanie w czasie wykonywania można włączać (w przypadku uruchomień debugowania) i wyłączać (w przypadku uruchomień produkcyjnych) za pomocą kompilatora lub opcji środowiska uruchomieniowego.

W przypadku 3. istnieją narzędzia do obsługi dowodów matematycznych, zwykle opartych na powyższej regule Floyda-Hoare'a, że ​​dany kod pętli faktycznie spełnia dany (zestaw) niezmienników pętli.

Technikę abstrakcyjnej interpretacji można wykorzystać do automatycznego wykrywania niezmienników pętli danego kodu. Jednak to podejście jest ograniczone do bardzo prostych niezmienników (takich jak 0<=i && i<=n && i%2==0).

Odróżnienie od kodu niezmiennego pętli

Niezmienniczość pętli ( właściwość niezmienna pętli ) należy odróżnić od kodu niezmiennego pętli ; zwróć uwagę na „niezmienny pętli” (rzeczownik) kontra „niezmienny pętli” (przymiotnik). Kod niezmienny w pętli składa się z instrukcji lub wyrażeń, które można przenieść poza treść pętli bez wpływu na semantykę programu. Takie przekształcenia, zwane ruchem kodu niezmiennego w pętli , są wykonywane przez niektóre kompilatory w celu optymalizacji programów. Przykładowy kod niezmienny w pętli (w języku programowania C ) to

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

gdzie obliczenia x = y+zi x*xmogą być przesunięte przed pętlą, co daje równoważny, ale szybszy program:

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

W przeciwieństwie do tego np. właściwość 0<=i && i<=njest niezmiennikiem pętli zarówno dla oryginalnego, jak i zoptymalizowanego programu, ale nie jest częścią kodu, stąd nie ma sensu mówić o „wyjściu z pętli”.

Kod niezmienny w pętli może indukować odpowiednią właściwość niezmienną pętli. W powyższym przykładzie najprostszym sposobem, aby to zobaczyć, jest rozważenie programu, w którym kod niezmiennika pętli jest obliczany zarówno przed, jak i wewnątrz pętli:

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

Właściwość niezmienna pętli tego kodu to (x1==x2 && t1==x2*x2) || i==0, wskazująca, że ​​wartości obliczone przed pętlą zgadzają się z wartościami obliczonymi w obrębie (z wyjątkiem przed pierwszą iteracją).

Zobacz też

• Niezmienny (informatyka)
• Niezmienny ruch w pętli
• Wariant pętli
• Najsłabsze warunki wstępne pętli While

Bibliografia

Dalsza lektura

• Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest i Clifford Stein . Wprowadzenie do algorytmów , wydanie drugie. MIT Press i McGraw-Hill, 2001. ISBN  0-262-03293-7 . Strony 17–19, sekcja 2.1: Sortowanie przez wstawianie.
• David Gries . „ Uwaga dotycząca standardowej strategii tworzenia niezmienników pętli i pętli ”. Science of Computer Programming , tom 2, s. 207-214. 1984.
• Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. „ Dynamiczne odkrywanie prawdopodobnych niezmienników programu w celu wspierania rozwoju programu ”. Międzynarodowa Konferencja Inżynierii Oprogramowania , s. 213–224. 1999.
• Roberta Paige. „ Programowanie ze niezmiennikami ”. Oprogramowanie IEEE , 3(1):56-69. Styczeń 1986.
• Yanhong A. Liu, Scott D. Stoller i Tim Teitelbaum . Wzmocnienie niezmienników dla wydajnych obliczeń . Nauka o programowaniu komputerowym , 41(2): 139–172. Październik 2001.
• Michael Huth, Mark Ryan. „ Logika w informatyce ”, wydanie drugie.