paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Validation of Modern JSON Schema: Formalization and Complexity

现代 JSON Schema 的验证:形式化与复杂度
POPL 8(POPL)2024匹配度 2/10 · 论文研究 JSON Schema 的形式化与验证复杂度,属于形式语义/领域特定语言的理论工作,与形式化验证有弱关联;但未涉及用户核心方向(LLM/Agent 与静态分析结合、浮点程序分析、贝叶斯程序分析)或 AI/Agentic 程序场景。引用 19 inbox
Lyes Attouche, Mohamed-Amine Baazizi, Dario Colazzo, Giorgio Ghelli, Carlo Sartiani, Stefanie Scherzinger
crossref: 2026-09-10

AI 速览

一句话:首次形式化现代 JSON Schema,并证明其数据验证问题是 PSPACE 完全,根源在动态引用。

JSON Schema 是 JSON 事实标准模式语言。Draft 2019-09 起引入动态引用与注解依赖验证等 Modern JSON Schema 特性,改变求值模型,导致规范理解困难。本文首次给出 Modern JSON Schema 的形式化语义,并与工具开发者社区讨论;进而分析数据验证复杂度,证明该问题为 PSPACE 完全。作者进一步表明其根源是 Draft 2020-12 的动态引用,而非注解依赖验证。复杂度分析显示:即使实例固定,问题对模式规模仍 PSPACE 完全;模式固定时则属 P。实验表明动态与静态引用的渐近复杂度差异在小模式上也很明显。

问题
Modern JSON Schema 的新特性使官方规范难以理解和实现,其数据验证的复杂度此前未得到明确刻画。
方法
该工作建立首个 Modern JSON Schema 形式化语义,分析数据验证问题的复杂度,并开展实验比较动态与静态引用。
评估
作者证明数据验证问题是 PSPACE 完全,并确定其根源为 Draft 2020-12 动态引用;复杂度分析区分 schema 与 data 规模,实验显示动态/静态引用的渐近差异。
原文摘要(Abstract)

JSON Schema is the de-facto standard schema language for JSON data. The language went through many minor revisions, but the most recent versions of the language, starting from Draft 2019-09, added two novel features, dynamic references and annotation-dependent validation , that change the evaluation model. Modern JSON Schema is the name used to indicate all versions from Draft 2019-09, which are characterized by these new features, while Classical JSON Schema is used to indicate the previous versions. These new “modern” features make the schema language quite difficult to understand and have generated many discussions about the correct interpretation of their official specifications; for this reason, we undertook the task of their formalization. During this process, we also analyzed the complexity of data validation in Modern JSON Schema, with the idea of confirming the polynomial complexity of Classical JSON Schema validation, and we were surprised to discover a completely different truth: data validation, which is expected to be an extremely efficient process, acquires, with Modern JSON Schema features, a PSPACE complexity. In this paper, we give the first formal description of Modern JSON Schema, which we have discussed with the community of JSON Schema tool developers, and which we consider a central contribution of this work. We then prove that its data validation problem is PSPACE-complete. We prove that the origin of the problem lies in the Draft 2020-12 version of dynamic references, and not in annotation-dependent validation. We study the schema and data complexities, showing that the problem is PSPACE-complete with respect to the schema size even with a fixed instance but is in P when the schema is fixed and only the instance size is allowed to vary. Finally, we run experiments that show that there are families of schemas where the difference in asymptotic complexity between dynamic and static references is extremely visible, even with small schemas.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2657,
  title = {Validation of Modern JSON Schema: Formalization and Complexity},
  author = {Lyes Attouche and Mohamed-Amine Baazizi and Dario Colazzo and Giorgio Ghelli and Carlo Sartiani and Stefanie Scherzinger},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632891}
}