JSON Schema Inclusion through Refutational Normalization: Reconciling Efficiency and Completeness

TL;DR

This paper presents a novel normalization technique that combines the efficiency of rule-based methods with the completeness of witness generation for JSON Schema inclusion reasoning.

Contribution

It introduces refutational normalization, enabling more effective and scalable JSON Schema inclusion checks beyond current limitations.

Findings

Refutational normalization significantly improves inclusion checking accuracy.

The approach outperforms existing methods on real-world and synthetic schemas.

It enables reasoning tasks previously too computationally expensive.

Abstract

JSON Schema is the de facto standard for describing the structure of JSON documents. Reasoning about JSON Schema inclusion -- whether every instance satisfying a schema S1 also satisfies a schema S2 -- is a key building block for a variety of tasks, including version and API compatibility checks, schema refactoring tools, and large-scale schema corpus analysis. Existing approaches fall into two families: rule-based algorithms that are efficient but incomplete and witness generation-based algorithms that are complete but oftentimes extremely slow. This paper introduces a new approach that reconciles the efficiency of rule-based procedures with the completeness of the witness-generation technique, by enriching the latter with a specialized form of normalization. This refutational normalization paves the way for use-cases that are too hard for current tools. Our experiments with real-world and synthetic schemas show that the refutational normalization greatly advances the state-of-the-art in JSON Schema inclusion checking.