Testen des Prädikats "Sicherer Ausdruck"

Question

In einer kürzlich gestellten Frage (How to define (and name) the corresponding safe term comparison predicates in ISO Prolog?) hat @false nach einer Implementierung des Begriffes Bestellprädikat lt/2 gefragt, einer Variante des eingebauten ISO (@<)/2. Der Wahrheitswert von lt(T1,T2) ist stabil zu sein w.r. beliebige variable Bindungen in T1 und T2.

In verschiedenen Antworten wurden verschiedene Implementierungen (basierend auf impliziten/expliziten Begriffstraversalen) vorgeschlagen. Einige Bemerkungen und Hinweise wurden in Kommentaren erhoben, so auch Gegenbeispiele.

Also meine Frage: Wie können Kandidatenimplementierungen getestet werden? Brute-Force-Ansatz? Oder etwas schlauer?

In jedem Fall teilen Sie bitte Ihre automatischen Prüfmaschinen für lt/2! Es ist für das größere gute!

Answer 1

Es gibt zwei Teststrategien: Validierung und Überprüfung.

Validierung: Testen ist immer gleich. Zuerst benötigen Sie eine Spezifikation dessen, was Sie testen möchten. Zweitens brauchen Sie eine Implementierung dessen, was Sie testen möchten.

Dann aus der Implementierung extrahieren Sie die Codeausführungspfade. Und für jeden Codeausführungspfad aus der Spezifikation leiten Sie das gewünschte Ergebnis ab.

Und dann schreiben Sie Testfälle, die jede Ausführungspfade und die gewünschten Ergebnisse kombinieren. Teste nicht nur positive Pfade, sondern auch negative Pfade.

Wenn Ihr Code rekursiv ist, haben Sie theoretisch unendlich viele Ausführungswege.

Aber Sie könnten feststellen, dass eine Sub-Rekursion mehr oder weniger die gleiche fragt als was ein anderer Testfall bereits gefragt. So kann man in vielen Fällen auch mit einer endlichen Menge testen.

Validierung gibt Ihnen Sicherheit.

Überprüfung: Sie würden einige formale Methoden verwenden, um die Korrektheit Ihrer Implementierung aus der Spezifikation abzuleiten.

Überprüfung gibt Ihnen 100% Sicherheit.