2025/06/22 by Lyes Attouche, Mohamed-Amine Baazizi, Dario Colazzo +5 · 1 voice
Computer Science · #Algorithms and Data Compression #Formal Methods in Verification #Software Testing and Debugging Techniques
paper · pdf · doi:10.1145/3735106.3736532
openalex publication_date 2025/06/22 · openalex created_date 2025/06/25 · openalex updated_date 2026/07/29
JSON Schema validators are essential tools in the JSON ecosystem. However, today's validators are primarily designed to be used programmatically. Even web-based tools are not didactic in their feedback regarding the oftentimes subtle interactions between schemas and JSON instances. We present JTutor, a validation framework specifically designed with humans in mind, that lets users explore the mutual dependencies between a schema and a candidate instance in JSON Schema validation: Users explore schemas and candidate instances interactively, by navigating between subschemas and the JSON instance based on a detailed proof tree that is generated by a well-principled and rule-based validator. JTutor comes with a "Smart Format" feature that generates a focused view of the proof tree. "Smart Format" highlights branches that are relevant for understanding why an instance is valid or invalid, while deemphasizing others. This focused view can serve as an explanation of the validation. Although JTutor is designed to be educational, it can also help developers debug schemas. In this paper, we explain the internals of JTutor and demonstrate the tool itself.