Witness Generation for JSON Schema

TL;DR

This paper introduces the first direct algorithm for witness generation in JSON Schema, enabling practical static analysis tasks like satisfiability and inclusion checks, even on large real-world schemas.

Contribution

It presents a novel, formalized witness generation algorithm for JSON Schema, addressing a gap in existing static analysis methods.

Findings

Algorithm effectively generates witnesses for large schemas

Works well despite exponential complexity of the problem

Demonstrates practical applicability on real-world schemas

Abstract

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.