Asercja (rozwój oprogramowania) - Assertion (software development)

Ten artykuł dotyczy koncepcji programowania komputerowego. Aby uzyskać potwierdzenia w kontekście otwartego standardu SAML ( Security Assertion Markup Language ), zobacz Security Assertion Markup Language § Assertions .

W programowaniu komputerowym , w szczególności przy użyciu paradygmatu programowania imperatywnego , asercja jest predykatem ( funkcją o wartości logicznej nad przestrzenią stanów , zwykle wyrażoną jako logiczne zdanie przy użyciu zmiennych programu) połączonym z punktem w programie, który zawsze należy ewaluować jako true w tym momencie wykonywania kodu. Asercje mogą pomóc programiście odczytać kod, pomóc kompilatorowi go skompilować lub pomóc programowi wykryć jego własne defekty.

W przypadku tych ostatnich niektóre programy sprawdzają asercje, faktycznie oceniając predykat podczas ich uruchamiania. Następnie, jeśli nie jest to w rzeczywistości prawdą – niepowodzenie asercji – program uważa się za uszkodzony i zazwyczaj celowo zawiesza się lub zgłasza wyjątek niepowodzenia asercji .

Detale

Poniższy kod zawiera dwie asercje x > 0i x > 1, i rzeczywiście są one prawdziwe we wskazanych punktach podczas wykonywania: 

x = 1;
assert x > 0;
x++;
assert x > 1;

Programiści mogą używać asercji, aby pomóc określić programy i uzasadnić poprawność programu. Na przykład warunek wstępny — asercja umieszczona na początku sekcji kodu — określa zestaw stanów, w których programista oczekuje wykonania kodu. Postcondition -placed w końcowych przedstawia przewidywaną stan po zakończeniu realizacji. Na przykład: x > 0 { x++ } x > 1.

Powyższy przykład używa notacji do włączenia twierdzeń użytych przez CAR Hoare w jego artykule z 1969 roku. Ta notacja nie może być używana w istniejących językach programowania głównego nurtu. Jednak programiści mogą dołączać niesprawdzone asercje, korzystając z funkcji komentarzy ich języka programowania. Na przykład w C : 

x = 5;
x = x + 1;
// {x > 1}

Nawiasy klamrowe zawarte w komentarzu pomagają odróżnić to użycie komentarza od innych zastosowań.

Biblioteki mogą również udostępniać funkcje asercji. Na przykład w C używając glibc z obsługą C99: 

#include <assert.h>

int f(void)
{
    int x = 5;
    x = x + 1;
    assert(x > 1);
}

Kilka nowoczesnych języków programowania zawiera sprawdzone asercje — instrukcje, które są sprawdzane w czasie wykonywania lub czasami statycznie. Jeśli asercja zostanie oceniona jako fałsz w czasie wykonywania, wyniknie niepowodzenie asercji, co zwykle powoduje przerwanie wykonywania. Zwraca to uwagę na lokalizację, w której wykryto logiczną niespójność i może być lepsze niż zachowanie, które w innym przypadku by się pojawiło.

Użycie asercji pomaga programiście zaprojektować, rozwinąć i uzasadnić program.

Stosowanie

W językach takich jak Eiffel twierdzenia stanowią część procesu projektowania; inne języki, takie jak C i Java , używają ich tylko do sprawdzania założeń w czasie wykonywania. W obu przypadkach można je sprawdzić pod kątem poprawności w czasie wykonywania, ale zwykle można je również pominąć.

Twierdzenia w projekcie według umowy

Twierdzenia może funkcjonować jako forma dokumentacji: mogą opisać stan kod spodziewa się znaleźć przed uruchomieniem (jego warunki wstępne ), a państwo to oczekuje kod spowoduje, kiedy jest gotowy do jazdy ( postconditions ); mogą również określić niezmienników o klasie . Eiffel integruje takie twierdzenia z językiem i automatycznie wyodrębnia je w celu udokumentowania klasy. Stanowi to ważną część metody projektowania na podstawie umowy .

Podejście to jest również przydatne w językach, które nie wspierają go wyraźnie: zaletą używania instrukcji asercji zamiast asercji w komentarzach jest to, że program może sprawdzać asercje przy każdym uruchomieniu; jeśli asercja nie jest już aktualna, może zostać zgłoszony błąd. Zapobiega to utracie synchronizacji kodu z potwierdzeniami.

Asercje do sprawdzania czasu wykonywania

Asercja może być użyta do sprawdzenia, czy założenie poczynione przez programistę podczas implementacji programu pozostaje ważne, gdy program jest wykonywany. Rozważmy na przykład następujący kod Java : 

 int total = countNumberOfUsers();
 if (total % 2 == 0) {
     // total is even
 } else {
     // total is odd and non-negative
     assert total % 2 == 1;
 }

W Java , %to pozostała uruchamiający ( modulo ), i Java, jeśli jego pierwszy argument operacji jest negatywny, wynik może być ujemny (w przeciwieństwie do stosowanych w matematyce modulo). W tym przypadku programista założył, że totaljest nieujemna, więc reszta z dzielenia przez 2 zawsze będzie równa 0 lub 1. Asercja uściśla to założenie: jeśli countNumberOfUserszwróci wartość ujemną, program może mieć błąd.

Główną zaletą tej techniki jest to, że gdy wystąpi błąd, jest on wykrywany natychmiast i bezpośrednio, a nie później poprzez często niejasne efekty. Ponieważ niepowodzenie asercji zwykle zgłasza lokalizację kodu, często można wskazać błąd bez dalszego debugowania.

Asercje są również czasami umieszczane w punktach, do których egzekucja nie powinna dotrzeć. Na przykład asercje mogą być umieszczane w defaultklauzuli switchinstrukcji w językach takich jak C , C++ i Java . Każdy przypadek, którego programista nie rozpatrzy celowo, zgłosi błąd i program zostanie przerwany, a nie po cichu kontynuowany w błędnym stanie. W D takie stwierdzenie jest dodawane automatycznie, gdy switchinstrukcja nie zawiera defaultklauzuli.

W Javie asercje są częścią języka od wersji 1.4. Błędy asercji skutkują podniesieniem an, AssertionErrorgdy program jest uruchamiany z odpowiednimi flagami, bez których instrukcje attach są ignorowane. W C są dodawane przez standardowy nagłówek assert.hdefiniujący jako makro, które sygnalizuje błąd w przypadku niepowodzenia, zwykle kończącego program. W C++ zarówno nagłówki , jak i nagłówki udostępniają makro. assert (assertion) assert.hcassertassert

Niebezpieczeństwo asercji polega na tym, że mogą one powodować skutki uboczne poprzez zmianę danych w pamięci lub zmianę taktowania wątków. Asercje powinny być implementowane ostrożnie, aby nie powodowały skutków ubocznych w kodzie programu.

Konstrukcje asercji w języku pozwalają na łatwe tworzenie oparte na testach (TDD) bez użycia biblioteki innej firmy.

Asercje w trakcie cyklu rozwojowego

Podczas cyklu rozwojowego programista zazwyczaj uruchamia program z włączonymi asercjami. Gdy wystąpi błąd asercji, programista jest natychmiast powiadamiany o problemie. Wiele implementacji asercji również zatrzymuje wykonywanie programu: jest to przydatne, ponieważ kontynuowanie działania programu po wystąpieniu naruszenia asercji może spowodować uszkodzenie jego stanu i utrudnić zlokalizowanie przyczyny problemu. Korzystając z informacji dostarczonych przez niepowodzenie asercji (takich jak lokalizacja błędu i być może ślad stosu lub nawet pełny stan programu, jeśli środowisko obsługuje zrzuty pamięci lub jeśli program działa w debugerze ), programista może zwykle naprawić problem. W ten sposób asercje stanowią bardzo potężne narzędzie w debugowaniu.

Asercje w środowisku produkcyjnym

Gdy program jest wdrażany w środowisku produkcyjnym , asercje są zazwyczaj wyłączane, aby uniknąć jakichkolwiek dodatkowych kosztów lub skutków ubocznych, jakie mogą mieć. W niektórych przypadkach asercje są całkowicie nieobecne we wdrożonym kodzie, na przykład w asercjach C/C++ za pośrednictwem makr. W innych przypadkach, takich jak Java, asercje są obecne we wdrożonym kodzie i można je włączyć w polu w celu debugowania.

Asercje mogą być również używane do obiecania kompilatorowi, że dany warunek brzegowy nie jest faktycznie osiągalny, umożliwiając w ten sposób pewne optymalizacje , które w innym przypadku nie byłyby możliwe. W takim przypadku wyłączenie asercji może w rzeczywistości zmniejszyć wydajność.

Asercje statyczne

Asercje sprawdzane w czasie kompilacji są nazywane asercjami statycznymi.

Asercje statyczne są szczególnie przydatne w metaprogramowaniu szablonów w czasie kompilacji , ale mogą być również używane w językach niskiego poziomu, takich jak C, wprowadzając niedozwolony kod, jeśli (i tylko wtedy) asercja się nie powiedzie. C11 i C++11 obsługują asercje statyczne bezpośrednio przez static_assert. We wcześniejszych wersjach C można zaimplementować asercję statyczną, na przykład tak: 

#define SASSERT(pred) switch(0){case 0:case pred:;}

SASSERT( BOOLEAN CONDITION );

Jeśli (BOOLEAN CONDITION)część ma wartość false, powyższy kod nie zostanie skompilowany, ponieważ kompilator nie zezwoli na dwie etykiety wielkości liter z tą samą stałą. Wyrażenie logiczne musi być wartością stałą czasu kompilacji, na przykład byłoby prawidłowym wyrażeniem w tym kontekście. Ta konstrukcja nie działa w zakresie pliku (tzn. nie wewnątrz funkcji), dlatego musi być opakowana wewnątrz funkcji. (sizeof(int)==4)

Innym popularnym sposobem implementacji asercji w C jest: 

static char const static_assertion[ (BOOLEAN CONDITION)
                                    ? 1 : -1
                                  ] = {'!'};

Jeśli (BOOLEAN CONDITION)część ma wartość false, powyższy kod nie zostanie skompilowany, ponieważ tablice mogą nie mieć ujemnej długości. Jeśli w rzeczywistości kompilator zezwala na ujemną długość, to bajt inicjujący ( '!'część) powinien spowodować skargę nawet tak pobłażliwym kompilatorom. Wyrażenie logiczne musi być wartością stałą czasu kompilacji, na przykład (sizeof(int) == 4)byłoby prawidłowym wyrażeniem w tym kontekście.

Obie te metody wymagają metody konstruowania unikalnych nazw. Nowoczesne kompilatory obsługują __COUNTER__definicję preprocesora, która ułatwia konstruowanie unikalnych nazw, zwracając monotonicznie rosnące liczby dla każdej jednostki kompilacji.

D zapewnia statyczne asercje poprzez użycie static assert.

Wyłączanie asercji

Większość języków umożliwia włączanie lub wyłączanie asercji globalnie, a czasem niezależnie. Asercje są często włączane podczas opracowywania i wyłączane podczas końcowych testów oraz po wydaniu dla klienta. Niesprawdzanie stwierdzeń pozwala uniknąć kosztów oceny stwierdzeń, podczas gdy (zakładając, że stwierdzenia są wolne od skutków ubocznych ) nadal dają ten sam wynik w normalnych warunkach. W nietypowych warunkach wyłączenie sprawdzania asercji może oznaczać, że program, który zostałby przerwany, będzie nadal działał. Czasami jest to lepsze.

Niektóre języki, w tym C i C++ , mogą całkowicie usunąć asercje w czasie kompilacji przy użyciu preprocesora . Java wymaga przekazania opcji do silnika wykonawczego w celu włączenia asercji. W przypadku braku tej opcji asercje są pomijane, ale zawsze pozostają w kodzie, chyba że zostaną zoptymalizowane przez kompilator JIT w czasie wykonywania lub wykluczone przez if (false)warunek w czasie kompilacji, dlatego nie muszą mieć miejsca ani kosztu czasu w czasie wykonywania w Javie albo.

Programiści mogą wbudować w swój kod kontrole, które są zawsze aktywne, omijając lub manipulując normalnymi mechanizmami sprawdzania asercji języka.

Porównanie z obsługą błędów

Asercje różnią się od rutynowej obsługi błędów. Asercje dokumentują logicznie niemożliwe sytuacje i odkrywają błędy programistyczne: jeśli niemożliwe się wydarzy, oznacza to, że coś fundamentalnego jest wyraźnie nie tak z programem. Różni się to od obsługi błędów: większość warunków błędu jest możliwa, chociaż niektóre mogą być bardzo mało prawdopodobne w praktyce. Używanie asercji jako mechanizmu obsługi błędów ogólnego przeznaczenia jest nierozsądne: asercje nie pozwalają na naprawienie błędów; niepowodzenie asercji zwykle powoduje nagłe zatrzymanie wykonywania programu; a asercje są często wyłączone w kodzie produkcyjnym. Asercje również nie wyświetlają przyjaznego dla użytkownika komunikatu o błędzie.

Rozważmy następujący przykład użycia asercji do obsługi błędu: 

  int *ptr = malloc(sizeof(int) * 10);
  assert(ptr);
  // use ptr
  ...

Tutaj programista jest świadomy, że malloczwróci NULLwskaźnik, jeśli pamięć nie zostanie przydzielona. Jest to możliwe: system operacyjny nie gwarantuje, że każde wywołanie się mallocpowiedzie. Jeśli wystąpi błąd braku pamięci, program zostanie natychmiast przerwany. Bez potwierdzenia program działałby dalej, dopóki nie ptrzostanie wyłuskany, a być może dłużej, w zależności od używanego sprzętu. Dopóki asercje nie są wyłączone, zapewnione jest natychmiastowe wyjście. Ale jeśli pożądana jest pełna wdzięku awaria, program musi sobie z nią poradzić. Na przykład serwer może mieć wielu klientów lub może przechowywać zasoby, które nie zostaną zwolnione w sposób czysty, lub może zawierać niezatwierdzone zmiany do zapisu w magazynie danych. W takich przypadkach lepiej jest nie powieść jednej transakcji niż nagle przerwać.

Innym błędem jest poleganie na efektach ubocznych wyrażeń użytych jako argumenty asercji. Należy zawsze pamiętać, że twierdzenia mogą w ogóle nie zostać wykonane, ponieważ ich jedynym celem jest sprawdzenie, czy warunek, który zawsze powinien być prawdziwy, faktycznie jest prawdziwy. W konsekwencji, jeśli program zostanie uznany za wolny od błędów i zwolniony, asercje mogą zostać wyłączone i nie będą już oceniane.

Rozważ inną wersję poprzedniego przykładu: 

  int *ptr;
  // Statement below fails if malloc() returns NULL,
  // but is not executed at all when compiling with -NDEBUG!
  assert(ptr = malloc(sizeof(int) * 10));
  // use ptr: ptr isn't initialised when compiling with -NDEBUG!
  ...

Może to wyglądać na sprytny sposób przypisania wartości zwracanej mallocdo ptri sprawdzenia, czy jest to NULLw jednym kroku, ale mallocwywołanie i przypisanie do ptrjest efektem ubocznym oceny wyrażenia, które tworzy assertwarunek. Gdy NDEBUGparametr jest przekazywany do kompilatora, na przykład gdy program jest uważany za wolny od błędów i wydany, assert()instrukcja jest usuwana, więc malloc()nie jest wywoływana, renderując ptrniezainicjowaną. Może to potencjalnie skutkować błędem segmentacji lub podobnym błędem wskaźnika zerowego znacznie dalej w trakcie wykonywania programu, powodując błędy, które mogą być sporadyczne i/lub trudne do wyśledzenia. Programiści czasami używają podobnej definicji VERIFY(X), aby złagodzić ten problem.

Współczesne kompilatory mogą generować ostrzeżenie podczas napotkania powyższego kodu.

Historia

W raportach von Neumanna i Goldstine'a z 1947 roku na temat ich projektu maszyny IAS opisali algorytmy za pomocą wczesnej wersji schematów blokowych , w których zawarli twierdzenia: „Może być prawdą, że za każdym razem, gdy C faktycznie osiąga określony punkt w przepływie diagramu, co najmniej jedna zmienna związana będzie z konieczności posiadać pewne określone wartości lub pewne właściwości lub spełniać pewne właściwości ze sobą. Ponadto możemy w takim momencie wskazać ważność tych ograniczeń. Z tego powodu oznaczymy każdy obszar, w którym ważność takich ograniczeń jest potwierdzana, przez specjalne pudełko, które nazywamy skrzynką asercji”.

Asercyjną metodę udowadniania poprawności programów opowiadał Alan Turing . W przemówieniu „Sprawdzanie dużej procedury” w Cambridge, 24 czerwca 1949 r. Turing zasugerował: „Jak można sprawdzić dużą rutynę w sensie upewnienia się, że jest ona poprawna? programista powinien poczynić szereg określonych asercji, które można indywidualnie sprawdzić i z których łatwo wynika poprawność całego programu”.

Zobacz też

Bibliografia

Zewnętrzne linki