구성적 생성기 동등성 (Compositional Generator Equivalence) (확장 버전)

속성 기반 테스트 (Property-based testing, PBT)는 실행 가능한 명세인 속성 (properties)에 대한 반례를 찾고 최소화하기 위해 무작위 입력 생성기 (random input generators)와 "축소 (shrinking)" 프로세스에 의존하는 소프트웨어 검증을 위한 강력한 기술입니다. 이러한 생성기를 최적화하는 것은 테스트 효율성을 위해 매우 중요하지만, 기존 언어들은 고수준 추론에 충분히 조밀하지 않은 (coarse-grained) 구성적 의미론 (compositional semantics)이 부족하기 때문에 이러한 최적화를 공식적으로 정당화하는 것은 현재 어렵습니다. 본 논문에서는 먼저 인기 있는 PBT 프레임워크인 Hedgehog의 구문 (syntax)과 의미론 (semantics)에 대한 공식적인 설명을 제공합니다. 우리는 사용자가 일반적으로 생성기에 대해 추론하는 방식을 모델링하는 Hedgehog의 분포 의미론 (distribution semantics)이 비구성적 (non-compositional)임을 입증합니다. 나아가, Hedgehog를 위한 임의의 건전하고 완전한 (sound and complete) 구성적 의미론은 반드시 샘플링 의미론 (sampling semantics)과 동등해야 하며, 이는 일반적인 프로그램 최적화를 정당화하기에는 너무 세밀하다는 (fine-grained) 것을 증명합니다. 이 딜레마를 해결하기 위해, 우리는 화살표 계산법 (arrow calculus)에 기반한 제한된 버전의 언어인 Hedgehog$^
ightarrow$를 도입하고, Hedgehog$^
ightarrow$가 구성적 분포 의미론을 보유하고 있음을 증명합니다. 우리는 Haskell 구현을 통해 Hedgehog$^
ightarrow$를 평가하며, 이것이 구성적 생성기 동등성 증명에 필요한 공식적 토대를 제공하는 동시에 실질적인 관심 대상이 되는 생성기들을 포착할 수 있을 만큼 충분히 표현력이 풍부함을 보여줍니다.