Uściślenie (przetwarzanie) - Refinement (computing)

Transformacja danych
Koncepcje
Języki transformacji
Techniki i przemiany
Aplikacje
Związane z

Udoskonalanie to ogólny termin informatyki, który obejmuje różne podejścia do tworzenia poprawnych programów komputerowych i upraszczania istniejących programów, aby umożliwić ich formalną weryfikację.

Udoskonalenie programu

W metodach formalnych , Program dystynkcja jest weryfikowalne transformacja w abstrakcyjnej (wysokiego szczebla) specyfikacji formalnej do betonu (niski poziom) program wykonywalny . Stopniowe udoskonalanie pozwala na wykonywanie tego procesu etapami. Logicznie rzecz biorąc, udoskonalenie zwykle wiąże się z implikacjami , ale mogą wystąpić dodatkowe komplikacje.

Progresywne, dokładnie na czas przygotowywanie zaległości produktu (listy wymagań) w zwinnych podejściach do tworzenia oprogramowania , takich jak Scrum , jest również powszechnie określane jako udoskonalanie.

Udoskonalenie danych

Udoskonalanie danych służy do konwersji abstrakcyjnego modelu danych ( na przykład pod względem zbiorów ) w możliwe do zaimplementowania struktury danych (takie jak tablice ). Udoskonalenie operacji przekształca specyfikację operacji w systemie na program możliwy do zaimplementowania (np. Procedurę ). W tym procesie warunek końcowy może zostać wzmocniony i / lub warunek wstępny osłabiony. Zmniejsza to niedeterminizm w specyfikacji, zazwyczaj do całkowicie deterministycznej implementacji.

Na przykład x ∈ {1, 2, 3} (gdzie x jest wartością zmiennej x po operacji) można zawęzić do x ∈ {1,2}, a następnie x ∈ {1} i zaimplementować jako x  : = 1. Implementacje x  : = 2 i x  : = 3 byłyby równie akceptowalne w tym przypadku, przy użyciu innej ścieżki do uściślenia. Musimy jednak uważać, aby nie zawęzić do x ∈ {} (odpowiednik fałszu ), ponieważ jest to niemożliwe; nie można wybrać członka z pustego zestawu .

Czasami używany jest również termin reifikacja (ukuty przez Cliffa Jonesa ). Retrenchment to alternatywna technika, gdy formalne udoskonalenie nie jest możliwe. Przeciwieństwem wyrafinowania jest abstrakcja .

Rachunek uściślający

Rachunek udoskonalający to formalny system (inspirowany logiką Hoare'a ), który promuje udoskonalanie programu. System transformacji FermaT to przemysłowa implementacja wyrafinowania. Metoda B jest również formalną metodą, która rozszerza rachunek uściślenia o język składowy: jest używana w rozwoju przemysłu.

Rodzaje uściślenia

Główny artykuł: rodzaj uszlachetnienia

W teorii typów , A typ dystynkcja jest rodzajem obdarzony orzecznika, który zakłada do ładowni dla każdego elementu wyrafinowanej typu. Typy doprecyzowujące mogą wyrażać warunki wstępne, gdy są używane jako argumenty funkcji lub warunki końcowe, gdy są używane jako typy zwracane : na przykład typ funkcji, która akceptuje liczby naturalne i zwraca liczby naturalne większe niż 5, można zapisać jako . Typy uściślenia są zatem powiązane z podtypami behawioralnymi .

Zobacz też

Bibliografia