问题描述
我有一个定义语言的函数，让我们调用 L，这个函数获取一个单词并返回 True 或 False。
我还有一个确定性的有限自动机，它假设接受语言中的单词并后悔语言中没有的单词。
我的任务是得到一个反例来区分 dfa 和 python 函数。
我想知道 CrossHair 是否对这项任务有用。
我希望像这样：
counterexmaple = checker(dfa,func)
谢谢
解决方法
总结
您或许可以使用 CrossHair 来解决此类问题。但是，执行确定性有限自动机 (DFA) 将涉及许多分支行为，而 CrossHair 在这种情况下表现不佳。在大多数情况下，您最好使用带有 hypothesis 的随机测试方法。我将描述这两种方法。
预赛
首先，您需要能够在 Python 中表达您的 DFA 以比较实现。下面是一个例子：
from typing import Tuple,Dict
# We construct a DFA that accepts any string that ends
# with "abc":
_TRANSITION_TABLE: Dict[Tuple[int,str],int] = {
# state #0: we have not yet seen "a" (initial state)
(0,'a'): 1,# state #1: we've seen "a"
(1,(1,'b'): 2,# state #2: we've seen "ab"
(2,(2,'c'): 3,# state #3: we've seen "abc" (final state)
(3,}
def dfa_checker(s: str) -> bool:
state = 0
for char in s:
state = _TRANSITION_TABLE.get((state,char),0)
return state == 3
def correct_custom_checker(s: str) -> bool:
return s.endswith("abc")
def incorrect_custom_checker(s: str) -> bool:
return s.endswith("bc")
CrossHair 解决方案
您可以为自定义实现提供一个契约，声明其结果与 DFA 相同：
def incorrect_custom_checker(s: str) -> bool:
''' post: __return__ == dfa_checker(s) '''
return bool(re.fullmatch('[abc]*',s) and s.endswith("bc"))
虽然不是真正的函数所必需的，但为我们的字母表 (abc) 添加正则表达式有助于 CrossHair 找到解决方案。现在我们可以让 CrossHair 尝试反驳契约：
$ crosshair check example.py
example.py:29:error:false when calling incorrect_custom_checker(s = 'bc') (which returns True)
它找到了被不正确_custom_checker()接受但被DFA拒绝的反例“bc”。
此外，还有一个非常新的、基本上没有记录的十字准线命令，可以让这种事情变得更加容易。您可以使用以下方法比较任意两个任意 Python 函数：
$ crosshair diffbehavior example.incorrect_custom_checker example.dfa_checker
given: (s='bc')
- returns: True
+ returns: False
如果您需要完全以编程方式执行此操作，则可以访问执行此操作的 CrossHair 内部结构 here。这种方法会随着 CrossHair 代码库的发展而失效，但为了完整起见，我将其包含在此处。
假设解
正如我之前提到的，进行大量随机测试可能更适合您。下面是一种在假设中做到这一点的方法：
import hypothesis
from hypothesis.strategies import text
@hypothesis.given(text(alphabet="abc"))
def test_checkers_equivalent(s: str) -> None:
assert dfa_checker(s) == incorrect_custom_checker(s)
运行 pytest example.py 会找到相同的“bc”反例。