4

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!

Community
  • 1
  • 1
repeat
  • 18,496
  • 4
  • 54
  • 166

1 Answers1

1

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.

  • Ok, so how could I go about validating something like `lt/2`? – repeat Apr 18 '16 at 07:24
  • 1
    The ISO core standard document, in this document there are templates, specs and tests cases for each predicate. Try to do the same for lt/2. Then build a test runner, design some test harness helpers and real test cases. I did the same recently for my CLP(FD): http://www.jekejeke.ch/idatab/doclet/prod/en/docs/15_min/15_stdy/07_compliance/09_results/package.html Links between test report and test case should now work. –  Apr 18 '16 at 08:00
  • One more recent addition, a little code coverage tool, which helps checking whether all paths are checked or not: https://plus.google.com/+JekejekeCh/posts/4EP29tzxWp9 –  May 21 '16 at 22:04