CODEWITHSUNDEEP
testingprologiso-prolog
repeat
repeat

Reputation: 18726

Testing "Safe term order" predicate

In a recent question (How to define (and name) the corresponding safe term comparison predicates in ISO Prolog?) @false asked for an implementation of the term ordering predicate lt/2, a variant of the ISO builtin (@<)/2.

The truth value of lt(T1,T2) is to be stable w.r.t. arbitrary variable bindings in T1 and T2.

In various answers, different implementations (based on implicit / explicit term traversal) were proposed. Some caveats and hints were raised in comments, so were counterexamples.

So my question: how can candidate implementations be tested? Some brute-force approach? Or something smarter?

In any case, please share your automatic testing machinery for lt/2! It's for the greater good!

Upvotes: 4

Views: 93

Answers (1)

user502187
user502187

Reputation:

There are two testing strategies: validation and verification.

Validation: Testing is always the same. First you need a specification of what you want to test. Second you need an implementation of what you want to test.

Then from the implementation you extract the code execution paths. And for each code execution path from the specification, you derive the desired outcome.

And then you write test cases combining each execution paths and the desired outcomes. Do not only test positive paths, but also negative paths.

If your code is recursive, you have theoretically infinitely many execution paths.

But you might find that a sub recursion more or less asks the same than what another test case already asked. So you can also test with a finite set in many cases.

Validation gives you confidence.

Verification: You would use some formal methods to derive the correctness of your implementation from the specification.

Verification gives you 100% assurance.

Upvotes: 1

Related Questions