2015-05-07 14 views
5

W ostatnim pytaniu (How to define (and name) the corresponding safe term comparison predicates in ISO Prolog?) @false poprosił o implementację terminu zamawiania predykatu lt/2, wariant ISO wbudowanego (@<)/2.Testowanie predykatu "Rzędu bezpiecznego"

Prawdziwa wartość lt(T1,T2) ma być stabilna w.r.t. dowolne zmienne wiązania w T1 i T2.

W różnych odpowiedziach zaproponowano różne implementacje (oparte na ukrytym/niejawnym przewijaniu terminów). Niektóre zastrzeżenia i wskazówki zostały podniesione w komentarzach, tak samo jak kontrprzykłady.

Moje pytanie: jak można testować wdrożenia kandydatów? Jakieś brutalne podejście? Lub coś mądrzejszego?

W każdym przypadku prosimy o udostępnienie automatycznych maszyn testujących dla lt/2! To jest dla większego dobra!

+1

Istnieje już 400 nagród za pokrewne pytanie. – false

Odpowiedz

1

Dostępne są dwie strategie testowania: sprawdzanie poprawności i weryfikacja.

Walidacja: Testowanie jest zawsze takie samo. Najpierw potrzebujesz specyfikacji tego, co chcesz przetestować. Po drugie potrzebujesz implementacji tego, co chcesz przetestować.

Następnie z wdrożenia wyodrębnia się ścieżki wykonania kodu. I dla każdej ścieżki wykonania kodu ze specyfikacji uzyskujesz pożądany wynik.

A następnie piszesz przypadki testowe, łącząc poszczególne ścieżki wykonania i pożądane wyniki. Sprawdzaj nie tylko ścieżki pozytywne, ale także ścieżki negatywne.

Jeśli twój kod jest rekurencyjny, teoretycznie masz nieskończenie wiele ścieżek wykonania.

Ale może się okazać, że sub rekursji mniej więcej prosi się o to samo, co już zadał inny test. W wielu przypadkach można również testować z zestawem skończonym.

Walidacja daje pewność.

Weryfikacja: Użyłbyś pewnych formalnych metod, aby wyprowadzić poprawność swojej implementacji ze specyfikacji.

Weryfikacja daje 100% pewność.

+0

OK, więc w jaki sposób mógłbym zatwierdzić coś w stylu 'lt/2'? – repeat

+1

Standardowy dokument ISO, w tym dokumencie są szablony, specyfikacje i testy przypadków dla każdego predykatu. Spróbuj zrobić to samo dla lt/2. Następnie zbuduj test biegacza, zaprojektuj kilka pomocniczych wiązek przewodów i prawdziwe przypadki testowe. Zrobiłem to samo ostatnio dla mojego CLP (FD): http://www.jekejeke.ch/idatab/doclet/prod/en/docs/15_min/15_stdy/07_compliance/09_results/package.html Linki między raportem z testu a przypadkiem testowym powinien teraz działać. –

+0

Jeszcze jeden nowszy dodatek, małe narzędzie do obsługi kodu, które pomaga sprawdzić, czy wszystkie ścieżki są sprawdzane, czy nie: https://plus.google.com/+JekejekeCh/posts/4EP29tzxWp9 –