2026-07-23T08:19:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23318 2025-06-25T13:20:37Z ddc:004 open_access

Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design Prasad, Siddhartha Greenman, Ben Nelson, Tim Krishnamurthi, Shriram formal methods diagramming visualization language design Tools such as Alloy enable users to incrementally define, explore, verify, and diagnose specifications for complex systems. A critical component of these tools is a visualizer that lets users graphically explore generated models. As we show, however, a default visualizer that knows nothing about the domain can be unhelpful and can even actively violate presentational and cognitive principles. At the other extreme, full-blown custom visualization requires significant effort as well as knowledge that a tool user might not possess. Custom visualizations can also exhibit bad (even silent) failures. This paper charts a middle ground between the extremes of default and fully-customizable visualization. We capture essential domain information for lightweight diagramming, embodying this in a language. To identify key elements of lightweight diagrams, we ground the language design in both the cognitive science research on diagrams and in a corpus of 58 custom visualizations. We distill from these sources a small set of orthogonal primitives, and use the primitives to guide a diagramming language called Cope-and-Drag (CnD). We evaluate it on sample tasks, three user studies, and performance, and find that short CnD specifications consistently improve model comprehension over the Alloy default. CnD thus defines a new point in the design space of diagramming: a language that is lightweight, effective, and driven by sound principles. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Siddhartha Prasad and Ben Greenman and Tim Nelson and Shriram Krishnamurthi 2025 Is Part Of LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2025.26 urn:nbn:de:0030-drops-233187 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.26 eng https://creativecommons.org/licenses/by/4.0/legalcode