Czytałem kilka artykułów na temat typów zależnych i umów programowych. Z większości tego, co przeczytałem, wydaje się, że kontrakty są sprawdzane dynamicznie, a typy zależne sprawdzane statycznie.
Było kilka dokumentów, które skłoniły mnie do myślenia, że możliwe są kontrakty częściowo sprawdzane statycznie:
Na poziomie praktycznym umowy są twierdzeniami. Pozwalają sprawdzić (bez kwantyfikatora) właściwości poszczególnych wykonań programu. Kluczową ideą leżącą u podstaw sprawdzania umowy jest idea winy - w zasadzie chcesz wiedzieć, kto ponosi winę za naruszenie umowy. Może to być implementacja (która nie oblicza obiecanej wartości) lub obiekt wywołujący (który przekazał funkcji niewłaściwy rodzaj wartości).
Kluczowym wnioskiem jest to, że można śledzić winę za pomocą tej samej maszynerii, co pary osadzania i projekcji w konstrukcji odwrotnego limitu teorii domen. Zasadniczo przełączasz się z pracy z asercjami na pracę z parami asercji, z których jedna obwinia kontekst programu, a druga obwinia program. Następnie pozwala to zawijać funkcje wyższego rzędu kontraktami, ponieważ można modelować kontrawariancję przestrzeni funkcji, zamieniając parę asercji. (Zobacz na przykład artykuł Nicka Bentona „Cofanie pisania dynamicznego” ).
Typy zależne to typy. Typy określają zasady stwierdzania, czy niektóre programy są dopuszczalne, czy nie. W rezultacie nie obejmują one pojęcia winy, ponieważ ich funkcją jest przede wszystkim zapobieganie istnieniu źle działających programów. Nie można winić za to, że tylko dobrze sformułowane programy są nawet wypowiedziami gramatycznymi. Pragmatycznie oznacza to, że bardzo łatwo jest używać typów zależnych, aby mówić o właściwościach terminów z kwantyfikatorami (np. Że funkcja działa dla wszystkich danych wejściowych).
Te dwa widoki nie są takie same, ale są ze sobą powiązane. Zasadniczo chodzi o to, że w umowach zaczynamy od uniwersalnej dziedziny wartości i używamy kontraktów do obniżania wartości. Ale kiedy używamy typów, staramy się z góry określić mniejsze domeny wartości (z pożądaną właściwością). Możemy więc połączyć te dwa za pomocą rodzin relacji ukierunkowanych na typ (tj. Relacji logicznych). Na przykład zobacz najnowszą „Winy za wszystkich” Ahmeda, Findlera, Siek i Wadlera lub „Znaczenie typów: od wewnętrznej do zewnętrznej semantyki” Reynoldsa .
Ponieważ ogólnie nie można użyć testów do ustalenia uniwersalnie skwantyfikowanych właściwości funkcji, to wszystko.
Neel Krishnaswami,
3
O ile kwantyfikatory nie mieszczą się w domenach skończonych, w takim przypadku można je postrzegać jako duże koniunkcje i rozłączenia. Lub jeśli chcesz się spodobać, możesz sprawdzić pewne rodzaje wyrażeń kwantyfikowanych, pod warunkiem, że zakres kwantyrów jest większy niż typy przeszukiwalne Martina Escardo (które mogą być nieskończone).
Andrej Bauer
2
@Radu: Nazywam JML & Co. „logiką programu”. Języki asercji logiki programu nie są ograniczone do terminów z języka programów. Pozwala to wykluczyć takie twierdzenia, jak nieterminowe lub powodujące skutki uboczne, które nie mają dobrej logicznej interpretacji. (Jednak takie rzeczy mają znaczenie dla sprawdzania kontraktów - patrz ostatnia praca Pucelli i Tove w ESOP nad wykorzystaniem stanowych, bezwzględnych kontraktów do śledzenia właściwości liniowości.)
(Dość abstrakcyjny) problem, jaki atakują zarówno typy, jak i kontrakty, brzmi „Jak zapewnić, aby programy miały określone właściwości?”. Istnieje nieodłączne napięcie między zdolnością wyrażania szerszej klasy właściwości a możliwością sprawdzania, czy program ma właściwość, czy nie. Systemy typów zazwyczaj zapewniają bardzo specyficzną właściwość (program nigdy nie ulega awarii w określony sposób) i mają algorytm sprawdzania typu. Z drugiej strony, kontrakty pozwalają na określenie bardzo szerokiego zakresu właściwości (powiedzmy, wynik tego programu jest liczbą pierwszą), ale nie zawierają algorytmu sprawdzającego.
Niemniej jednak fakt, że nie ma algorytmu sprawdzania kontraktów (który zawsze działa) nie oznacza, że nie ma algorytmów sprawdzania prawie kontraktów (które zwykle działają w praktyce). Polecam zajrzeć do Spec # i wtyczki Jessie Frama-C . Oba działają, wyrażając „ten program przestrzega tej umowy” jako oświadczenie w logice pierwszego rzędu poprzez wygenerowanie warunków weryfikacji , a następnie pytając SMTsolver, aby przejść, spróbuj znaleźć dowód. Jeśli solver nie znajdzie dowodu, to albo program jest zły, albo, cóż, solver nie znalazł dowodu, który istnieje. (Dlatego jest to algorytm „prawie” sprawdzania kontraktu.) Istnieją również narzędzia oparte na symbolicznym wykonywaniu, co oznacza z grubsza, że „ten program przestrzega tej umowy” jest wyrażony jako wiązka zdań (w pewnej logice). Zobacz na przykład jStar .
Praca Flanagana stara się czerpać to, co najlepsze z obu światów, abyś mógł szybko sprawdzić właściwości podobne do typu, a następnie zająć się resztą. Nie znam się na typach hybrydowych, ale pamiętam, jak autor powiedział, że jego motywacją było wymyślenie rozwiązania, które wymaga mniej adnotacji (niż poprzednia praca nad ESC / Java). W pewnym sensie istnieje jednak pewna luźna integracja między typami i umowami w ESC / Java (i Spec #): podczas sprawdzania umów solver otrzymuje informację, że sprawdzenie typu powiodło się, aby mógł zobaczyć te informacje.
Kontrakty można sprawdzać statycznie. Jeśli spojrzysz na starą pracę Dany Xu nad ESC / Haskell , była ona w stanie wdrożyć pełne sprawdzanie kontraktu w czasie kompilacji, opierając się tylko na twierdzeniu o arytmetyki. Zakończenie jest rozwiązywane przez prosty limit głębokości, jeśli dobrze pamiętam:
Zarówno kontrakty, jak i typy pozwalają reprezentować specyfikacje funkcji w stylu Hoare'a (warunek przed / po). Oba można sprawdzić statycznie w czasie kompilacji lub dynamicznie w czasie wykonywania.
Zależne typy pozwalają zakodować bardzo szeroki zakres właściwości w systemie typów, rodzaj właściwości, których oczekują programiści. Wynika to z faktu, że mogą zależeć od wartości typu. Typy zależne mają tendencję do sprawdzania statycznego, chociaż uważam, że cytowane artykuły dotyczą alternatywnych podejść.
Ostatecznie różnica jest niewielka. Myślę, że bardziej zależne typy są logiką, w której można wyrażać specyfikacje, podczas gdy kontrakty są metodologią programowania, w której wyrażasz specyfikacje.
Trochę mylące jest twierdzenie, że adnotacje w stylu Hoare'a można sprawdzać statycznie. Jeśli logiką jest FO, jak zwykle, problem jest z pewnością nierozstrzygalny. Ale tak, wiem, że miałeś na myśli, że można spróbować, a nawet odnieść sukces w wielu sytuacjach.
Radu GRIGore
1
Miałem wrażenie, że wygenerowanie dowodu może być nierozstrzygalne, ale sprawdzenie dowodu powinno być. Wiele języków o typie zależnym polega na dostarczeniu przez użytkownika wartości dowodowej zamieszkiwania typu twierdzenia.
Jason Reich
Masz rację. Ale żyję w zautomatyzowanym świecie, w którym użytkownik zwykle nie jest proszony o dowód.
(Dość abstrakcyjny) problem, jaki atakują zarówno typy, jak i kontrakty, brzmi „Jak zapewnić, aby programy miały określone właściwości?”. Istnieje nieodłączne napięcie między zdolnością wyrażania szerszej klasy właściwości a możliwością sprawdzania, czy program ma właściwość, czy nie. Systemy typów zazwyczaj zapewniają bardzo specyficzną właściwość (program nigdy nie ulega awarii w określony sposób) i mają algorytm sprawdzania typu. Z drugiej strony, kontrakty pozwalają na określenie bardzo szerokiego zakresu właściwości (powiedzmy, wynik tego programu jest liczbą pierwszą), ale nie zawierają algorytmu sprawdzającego.
Niemniej jednak fakt, że nie ma algorytmu sprawdzania kontraktów (który zawsze działa) nie oznacza, że nie ma algorytmów sprawdzania prawie kontraktów (które zwykle działają w praktyce). Polecam zajrzeć do Spec # i wtyczki Jessie Frama-C . Oba działają, wyrażając „ten program przestrzega tej umowy” jako oświadczenie w logice pierwszego rzędu poprzez wygenerowanie warunków weryfikacji , a następnie pytając SMTsolver, aby przejść, spróbuj znaleźć dowód. Jeśli solver nie znajdzie dowodu, to albo program jest zły, albo, cóż, solver nie znalazł dowodu, który istnieje. (Dlatego jest to algorytm „prawie” sprawdzania kontraktu.) Istnieją również narzędzia oparte na symbolicznym wykonywaniu, co oznacza z grubsza, że „ten program przestrzega tej umowy” jest wyrażony jako wiązka zdań (w pewnej logice). Zobacz na przykład jStar .
Praca Flanagana stara się czerpać to, co najlepsze z obu światów, abyś mógł szybko sprawdzić właściwości podobne do typu, a następnie zająć się resztą. Nie znam się na typach hybrydowych, ale pamiętam, jak autor powiedział, że jego motywacją było wymyślenie rozwiązania, które wymaga mniej adnotacji (niż poprzednia praca nad ESC / Java). W pewnym sensie istnieje jednak pewna luźna integracja między typami i umowami w ESC / Java (i Spec #): podczas sprawdzania umów solver otrzymuje informację, że sprawdzenie typu powiodło się, aby mógł zobaczyć te informacje.
źródło
Kontrakty można sprawdzać statycznie. Jeśli spojrzysz na starą pracę Dany Xu nad ESC / Haskell , była ona w stanie wdrożyć pełne sprawdzanie kontraktu w czasie kompilacji, opierając się tylko na twierdzeniu o arytmetyki. Zakończenie jest rozwiązywane przez prosty limit głębokości, jeśli dobrze pamiętam:
źródło
Zarówno kontrakty, jak i typy pozwalają reprezentować specyfikacje funkcji w stylu Hoare'a (warunek przed / po). Oba można sprawdzić statycznie w czasie kompilacji lub dynamicznie w czasie wykonywania.
Zależne typy pozwalają zakodować bardzo szeroki zakres właściwości w systemie typów, rodzaj właściwości, których oczekują programiści. Wynika to z faktu, że mogą zależeć od wartości typu. Typy zależne mają tendencję do sprawdzania statycznego, chociaż uważam, że cytowane artykuły dotyczą alternatywnych podejść.
Ostatecznie różnica jest niewielka. Myślę, że bardziej zależne typy są logiką, w której można wyrażać specyfikacje, podczas gdy kontrakty są metodologią programowania, w której wyrażasz specyfikacje.
źródło