Блог

У меня есть функция, которая определяет язык, давайте вызовем L, эта функция получает слово и возвращает True или False.

У меня также есть детерминированные конечные осенние данные, которые предполагают принимать слова, которые есть на языке, и сожалеть о словах, которых нет на языке L.

Моя миссия состоит в том, чтобы получить контрпример, который будет различать функцию dfa и функцию python.

Интересно, может ли перекрестие быть полезным для этой задачи.

Я ожидаю чего-то вроде:

 counterexmaple = checker(dfa, func)
 

Спасибо

Краткие сведения

Возможно, вы сможете использовать перекрестие для решения такого рода проблем. Однако выполнение детерминированных конечных автоматов (DFA) будет связано с большим количеством ветвистых действий, и CrossHair не очень хорошо работает в этой ситуации. В большинстве случаев вам может быть лучше использовать рандомизированный подход к тестированию с гипотезой. Я опишу оба подхода.

Предварительные мероприятия

Во-первых, вы захотите иметь возможность выразить свой DFA на python, чтобы сравнить реализации. Вот один из примеров:

 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, 'a'): 1,
    (1, 'b'): 2,
    # state #2: we've seen "ab"                                                                                                                                               
    (2, 'a'): 1,
    (2, 'c'): 3,
    # state #3: we've seen "abc" (final state)                                                                                                                                
    (3, 'a'): 1,
}

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")
 

Решение перекрестия

Вы можете предоставить пользовательской реализации контракт, в котором указано, что его результат совпадает с 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)
 

И он находит контрпример «bc», который принимается incorrect_custom_checker(), но отклоняется DFA.

Кроме того, существует совершенно новая, в значительной степени недокументированная команда crosshair, которая делает подобные вещи еще проще. Вы можете сравнить любые две произвольные функции python, используя:

 $ crosshair diffbehavior example.incorrect_custom_checker example.dfa_checker
  given: (s='bc')
- returns: True
  returns: False
 

Если вам нужно сделать это полностью программно, вы можете обратиться к внутренним устройствам CrossHair, которые делают это здесь. Этот подход будет нарушен по мере развития кодовой базы 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».