Poprawność (informatyka) - Correctness (computer science)

W teoretycznej An algorytm jest prawidłowe w odniesieniu do specyfikacji , jeśli zachowuje się w określony sposób. Najlepiej zbadana jest poprawność funkcjonalna , która odnosi się do zachowania wejścia-wyjścia algorytmu (tj. dla każdego wejścia generuje wyjście spełniające specyfikację).

W drugim pojęciem, częściowego poprawności i oznacza, że jeśli odpowiedź jest zwrócony będzie prawidłowa, różni się od całkowitego poprawności , dodatkowo wymaga, że odpowiedź jest powrócił, tj zakończone jest algorytmem. Odpowiednio, aby udowodnić całkowitą poprawność programu, wystarczy udowodnić jego częściową poprawność i jego zakończenie. Ten ostatni rodzaj dowodu (dowód zakończenia ) nigdy nie może być w pełni zautomatyzowany, ponieważ problem zatrzymania jest nierozstrzygnięty .

Częściowo poprawny program C do znalezienia
najmniej nieparzystej liczby doskonałej,
jego całkowita poprawność jest nieznana od 2021 r. 
// return the sum of proper divisors of n
static int divisorSum(int n) {
   int i, sum = 0;
   for (i=1; i<n; ++i)
      if (n % i == 0)
         sum += i;
   return sum;
}
// return the least odd perfect number
int leastPerfectNumber(void) {
   int n;
   for (n=1; ; n+=2)
      if (n == divisorSum(n))
         return n;
}

Na przykład, przeszukując kolejno liczby całkowite 1, 2, 3, …, aby zobaczyć, czy możemy znaleźć przykład jakiegoś zjawiska — powiedzmy nieparzystą liczbę doskonałą — całkiem łatwo jest napisać częściowo poprawny program (patrz ramka). Ale stwierdzenie, że ten program jest całkowicie poprawny, byłoby stwierdzeniem czegoś, co obecnie nie jest znane w teorii liczb .

Dowód musiałby być dowodem matematycznym, przy założeniu, że zarówno algorytm, jak i specyfikacja są podane formalnie. W szczególności nie oczekuje się, że będzie to stwierdzenie poprawności dla danego programu implementującego algorytm na danej maszynie. Wiązałoby się to z takimi rozważaniami jak ograniczenia pamięci komputera .

Głęboko wynik w teoria dowodu The korespondencja Curry-Howard , stwierdza, że dowód poprawności funkcjonalnej w konstruktywnych logicznych odpowiada pewnej programu w rachunku lambda . Konwersja dowodu w ten sposób nazywana jest wyodrębnianiem programu .

Logika Hoare'a to specyficzny formalny system rygorystycznego wnioskowania o poprawności programów komputerowych. Wykorzystuje techniki aksjomatyczne do definiowania semantyki języka programowania i argumentowania na temat poprawności programów poprzez twierdzenia znane jako trójki Hoare'a.

Testowanie oprogramowania to każda czynność mająca na celu ocenę atrybutu lub możliwości programu lub systemu i ustalenie, czy spełnia on wymagane wyniki. Chociaż kluczowe dla jakości oprogramowania i szeroko stosowane przez programistów i testerów, testowanie oprogramowania nadal pozostaje sztuką ze względu na ograniczone zrozumienie zasad oprogramowania. Trudność w testowaniu oprogramowania wynika ze złożoności oprogramowania: nie możemy całkowicie przetestować programu o umiarkowanej złożoności. Testowanie to coś więcej niż debugowanie. Celem testowania może być zapewnienie jakości, weryfikacja i walidacja lub szacowanie niezawodności. Testowanie może być również używane jako ogólna metryka. Testowanie poprawności i testowanie niezawodności to dwa główne obszary testowania. Testowanie oprogramowania to kompromis między budżetem, czasem i jakością.

Zobacz też

Uwagi

Bibliografia