Realizacja zamówienia (w języku angielskim, projektu umowy lub DBC ) to paradygmat programowania, w którym przebieg leczenia jest regulowane przepisami. Reguły te, zwane asercjami , tworzą umowę określającą obowiązki między klientem a dostawcą fragmentu kodu oprogramowania . Jest to pół- formalny programowanie metoda , której głównym celem jest ograniczenie liczby błędów w programach.
Historycznie rzecz biorąc, programowanie kontraktowe zostało wprowadzone przez Bertranda Meyera w jego języku Eiffla z 1985 roku, który był inspirowany notacją Z stworzoną przez Jeana-Raymonda Abriala .
Zasadą jest sprecyzowanie, co w danym momencie musi być prawdą w wykonaniu programu. Nie myśl, że ten paradygmat zobowiązuje do efektywnego testowania reguł podczas ich wykonywania: testy te są tylko jednym ze sposobów upewnienia się, że reguły są przestrzegane. Istnieją cztery typy twierdzeń :
Język, w którym zapisano warunki, jest ważny. Musi mieć wartość prawdy; Innymi słowy jest to logika i na ogół używać wyrażeń logicznych o tym gospodarza języku . Aby móc wyrazić więcej rzeczy, często dodajemy środki, tak aby warunki końcowe mogły odnosić się do starej wartości zmiennych zmodyfikowanych przez przetwarzanie. Na koniec możemy dodać kwantyfikatory logiki pierwszego rzędu .
Te stwierdzenia są zapisywane bezpośrednio w kodzie źródłowym programu i stanowią dodatkową dokumentację dotyczącą znaczenia kodu. Dzięki temu można opisać semantykę programu.
Kilka języków programowania implementuje ten paradygmat, np. Eiffel , D , Lisaac , Oxygene (en) , SPARK , Vala oraz Ada od wersji Ada 2012. Istnieją moduły dla innych języków, takich jak OCL dla UML , JML dla Java , ACSL dla C , Praspel dla PHP lub PSL dla VHDL .
Technika ta ma bardzo silny związek z formalnymi metodami stosowanymi do certyfikacji programu jako poprawnego. Trzy powyższe zasady są w rzeczywistości klasyczną formą specyfikacji programu.
Ale w przeciwieństwie do metod sprawdzania programów, nie będziemy dążyć do jednoznacznego wykazania, że specyfikacja jest rzeczywiście wykonywana przez program. Ta część pozostaje w gestii klienta i dostawcy.
Narzędzia do statycznej weryfikacji kodu mogą polegać na asercjach, aby zapewnić znaczącą diagnostykę.
Jednak często konfigurujemy mechanizmy testujące reguły podczas wykonywania, aby sprawdzić ich ważność. Potwierdzenia podczas testów możemy zweryfikować w elegancki sposób. Ale to w żaden sposób nie gwarantuje, że zasady będą obowiązywać przez cały czas. W rzeczywistości przez większość czasu konieczne byłoby przeprowadzenie nieskończonej liczby różnych egzekucji, aby zweryfikować wszystkie możliwe przypadki.
Programowanie kontraktowe, gdy jest ogólne, umożliwia znajdowanie błędów tak samo wydajnych jak testy jednostkowe, ale przy użyciu wszelkiego rodzaju testów automatycznych. Błąd, który występuje w części aplikacji, gdy potwierdzenia są weryfikowane w czasie wykonywania, jest dokładnie lokalizowany przez pierwsze nieudane potwierdzenie.
Do pewnego stopnia specyfikacje mogą być również przechowywane w celu weryfikacji i audytu w aplikacji produkcyjnej, jeśli ich weryfikacja nie wpływa na wydajność. Stają się wtedy potężnym środkiem wykrywania błędów w rzeczywistych warunkach.
Uważa się jednak, że metoda ta nadal umożliwia uzyskanie oprogramowania lepszej jakości i przyspieszenie faz debugowania.
Funkcję obliczającą pierwiastek kwadratowy z liczby rzeczywistej można zweryfikować w następujący sposób w pseudokodzie.
Warunek wstępny zapewnia, że programista prawidłowo używa funkcji, podczas gdy warunek końcowy pozwala programiście zaufać funkcji. Należy zadbać o to, aby wyrażenie można było skutecznie sprawdzić, np. Tutaj należałoby zadbać o błędy obliczeń numerycznych.