JSON模式的证据生成
Witness Generation for JSON Schema
摘要：
JSON Schema是一种重要的、不断发展的JSON文档族标准模式语言。它基于结构断言和布尔断言的复杂组合，并具有否定和递归功能。JSON Schema文档的静态分析包括实际相关的问题，包括模式可满足性、包含性和等价性。这三个问题可以简化为见证生成：给定一个模式，如果存在，则生成该模式的一个元素，否则报告失败。模式可满足性、包含性和等价性已经被证明是可判定的，通过在交替树自动机中约简到可达性。然而，还没有证据生成算法被正式描述。我们贡献了第一个，直接的JSON模式见证生成算法。我们研究了它的有效性和效率，在实验中的几个模式集合，包括成千上万的现实世界的模式。我们的重点是语言的完整性，其中我们只排除uniqueItems运算符，以及算法在合理的时间内在大量真实世界的例子上运行的能力，尽管潜在问题的指数复杂性。
英文摘要：
JSON Schema is an important, evolving standard schema language for families of JSON documents. It is based on a complex combination of structural and Boolean assertions, and features negation and recursion. The static analysis of JSON Schema documents comprises practically relevant problems, including schema satisfiability, inclusion, and equivalence. These three problems can be reduced to witness generation: given a schema, generate an element of the schema, if it exists, and report failure otherwise. Schema satisfiability, inclusion, and equivalence have been shown to be decidable, by reduction to reachability in alternating tree automata. However, no witness generation algorithm has yet been formally described. We contribute a first, direct algorithm for JSON Schema witness generation. We study its effectiveness and efficiency, in experiments over several schema collections, including thousands of real-world schemas. Our focus is on the completeness of the language, where we only exclude the uniqueItems operator, and on the ability of the algorithm to run in a reasonable time on a large set of real-world examples, despite the exponential complexity of the underlying problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
