在最近的一个问题中（如何在 ISO Prolog 中定义（和命名）相应的安全术语比较谓词？）@false 要求实现术语排序谓词lt/2，这是 ISO 内置的一个变体(@<)/2。
的真值是在和lt(T1,T2)中的任意变量绑定中是稳定的。T1T2
在各种答案中，提出了不同的实现（基于隐式/显式术语遍历）。评论中提出了一些警告和提示，反例也是如此。
所以我的问题是：如何测试候选实现？一些蛮力的方法？或者更聪明的东西？
无论如何，请分享您的自动测试机器lt/2！这是为了更大的利益！
有两种测试策略：验证和验证。
验证：测试总是一样的。首先，您需要指定要测试的内容。其次，您需要实现要测试的内容。
然后从实现中提取代码执行路径。对于规范中的每个代码执行路径，您都可以获得所需的结果。
然后你编写结合每个执行路径和期望结果的测试用例。不仅要测试积极的路径，还要测试消极的路径。
如果你的代码是递归的，理论上你有无限多的执行路径。
但是您可能会发现子递归或多或少地要求与另一个测试用例已经要求的相同。因此，在许多情况下，您也可以使用有限集进行测试。
验证给你信心。
验证：您将使用一些正式的方法从规范中得出实现的正确性。
验证为您提供 100% 的保证。