JSON Schema is a logical language used to define the structure of JSON values. JSON Schema syntax is based on nested schema objects. In all versions of JSON Schema until Draft-07, collectively known as Classical JSON Schema, the semantics of a schema was entirely described by the set of JSON values that it validates. This semantics was the basis for a thorough theoretical study and for the development of tools to decide satisfiability and equivalence of schemas. Unfortunately, Classical JSON Schema suffered a severe limitation in its ability to express extensions of object schemas, which caused the introduction, with Draft 2019-09, of two disruptive features: annotation dependency and dynamic references. These new features undermine the previously developed semantic theory, and the algorithms used to decide satisfiability for Classical JSON Schema are not easy to extend. One possible solution is rewriting a schema written in Modern JSON Schema into an equivalent schema in Classical JSON Schema. In this paper we prove that the elimination of annotation dependent keywords cannot, in general, avoid an exponential increase of the schema dimension. We provide an algorithm to eliminate these keywords that, despite the theoretical lower bound, behaves quite well in practice, as we verify with an extensive set of experiments.
翻译:JSON Schema是一种用于定义JSON值结构的逻辑语言。JSON Schema语法基于嵌套的模式对象。在截至Draft-07的所有JSON Schema版本(统称为经典JSON Schema)中,模式的语义完全由其验证的JSON值集合所描述。该语义为深入的理论研究以及判定模式可满足性与等价性的工具开发奠定了基础。遗憾的是,经典JSON Schema在表达对象模式扩展方面存在严重局限,这导致2019-09草案引入了两个颠覆性特性:标注依赖和动态引用。这些新特性破坏了先前建立的语义理论,且用于判定经典JSON Schema可满足性的算法难以扩展。一种可能的解决方案是将现代JSON Schema编写的模式重写为等价的经典JSON Schema模式。本文证明了消除标注依赖关键词通常无法避免模式维度的指数级增长。我们提出了一种消除这些关键词的算法,尽管存在理论下界,但通过大量实验验证,该算法在实践中表现良好。