Document Open Access Logo

Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design

Authors Siddhartha Prasad , Ben Greenman , Tim Nelson , Shriram Krishnamurthi

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.26.pdf
  • Filesize: 4.69 MB
  • 29 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Human-centered computing → Visualization toolkits
  • Software and its engineering → Constraint and logic languages
  • Software and its engineering → Specification languages
Keywords
  • formal methods
  • diagramming
  • visualization
  • language design

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi. Lightweight Diagramming for Lightweight Formal Methods: A Grounded Language Design. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 26:1-26:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.26

Author Details

Siddhartha Prasad
  • Brown University, Providence, RI, USA
Ben Greenman
  • University of Utah, Salt Lake City, UT, USA
Tim Nelson
  • Brown University, Providence, RI, USA
Shriram Krishnamurthi
  • Brown University, Providence, RI, USA

Funding

This work is partially supported by US NSF grant DGE-2208731.

Acknowledgements

We thank Tristan Dyer for sharing his insights on Sterling. We are also deeply grateful to Rob Goldstone for gently educating us about cognitive science. We thank Skyler Austen and Ji Won Chung for their feedback on study design and supplementary material.

Supplementary Materials

References

  1. Greg J Badros, Alan Borning, and Peter J Stuckey. The Cassowary linear arithmetic constraint solving algorithm. ACM Transactions on Computer-Human Interaction (TOCHI), 8(4):267-306, 2001. URL: https://doi.org/10.1145/504704.504705.
  2. Leilani Battle, Danni Feng, and Kelli Webber. Exploring D3 implementation challenges on Stack Overflow. In 2022 IEEE Visualization and Visual Analytics (VIS), pages 1-5. IEEE, 2022. URL: https://doi.org/10.1109/VIS54862.2022.00009.
  3. Michael Bostock, Vadim Ogievetsky, and Jeffrey Heer. D³ data-driven documents. IEEE Transactions on Visualization and Computer Graphics, 17(12):2301-2309, 2011. URL: https://doi.org/10.1109/TVCG.2011.185.
  4. Stanley J Cantrell, Bruce N Walker, and Øystein Moseng. Highcharts sonification studio: an online, open-source, extensible, and accessible data sonification tool. In Proceedings of the International Conference on Auditory Display, volume 2, 2021. Google Scholar
  5. Hsuanwei Michelle Chen. Information visualization principles, techniques, and software. Library Technology Reports, 53(3):8-16, 2017. Google Scholar
  6. Rui Couto, José Creissac Campos, Nuno Macedo, and Alcino Cunha. Improving the visualization of Alloy instances. In Paolo Masci, Rosemary Monahan, and Virgile Prevosto, editors, Proceedings 4th Workshop on Formal Integrated Development Environment, volume 284, pages 37-52, 2018. URL: https://doi.org/10.4204/EPTCS.284.4.
  7. Edsger W Dijkstra. Self-stabilizing systems in spite of distributed control. Communications of the ACM, 17(11):643-644, 1974. URL: https://doi.org/10.1145/361179.361202.
  8. Tim Dwyer. cola.js: Constraint-based layout in the browser, 2017. Accessed: 2024-12-02. URL: https://ialab.it.monash.edu/webcola/.
  9. Tim Dwyer, Kim Marriott, and Michael Wybrow. Topology preserving constrained graph layout. In Graph Drawing: 16th International Symposium, GD 2008, Heraklion, Crete, Greece, September 21-24, 2008. Revised Papers 16, pages 230-241. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00219-9_22.
  10. Tristan Dyer. Sterling JS demo, 2024. Accessed: 2024-11-12. URL: https://sterling-js.github.io/demo/.
  11. Tristan Dyer and John Baugh. Sterling: A web-based visualizer for relational modeling languages. In International Conference on Rigorous State-Based Methods, pages 99-104. Springer, 2021. Google Scholar
  12. Tristan Dyer, Tim Nelson, Kathi Fisler, and Shriram Krishnamurthi. Applying cognitive principles to model-finding output: the positive value of negative information. Proceedings of the ACM on Programming Languages, 6(OOPSLA1):1-29, 2022. URL: https://doi.org/10.1145/3527323.
  13. Frank Elavsky, Lucas Nadolskis, and Dominik Moritz. Data navigator: an accessibility-centered data navigation toolkit. IEEE transactions on visualization and computer graphics, 30(1):803-813, 2023. URL: https://doi.org/10.1109/TVCG.2023.3327393.
  14. Robert Goldstone. An efficient method for obtaining similarity data. Behavior Research Methods, Instruments, & Computers, 26:381-386, 1994. Google Scholar
  15. D. Jackson and J. Wing. Lightweight formal methods. IEEE Computer, pages 21-22, April 1996. Google Scholar
  16. Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2nd edition, 2012. Google Scholar
  17. Kurt Koffka. Perception: an introduction to the Gestalt-Theorie. Psychological bulletin, 19(10), 1922. Google Scholar
  18. Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier, and Michael Leuschel. A translation from Alloy to B. In Conference on Abstract State Machines, Alloy, B, and Z, pages 71-86, 2018. URL: https://doi.org/10.1007/978-3-319-91271-4_6.
  19. Lukas Ladenberger and Michael Leuschel. BMotionWeb: A tool for rapid creation of formal prototypes. In Software Engineering and Formal Methods, pages 403-417, 2016. URL: https://doi.org/10.1007/978-3-319-41591-8_27.
  20. Jill H Larkin and Herbert A Simon. Why a diagram is (sometimes) worth ten thousand words. Cognitive science, 11(1):65-100, 1987. URL: https://doi.org/10.1111/J.1551-6708.1987.TB00863.X.
  21. Michael Leuschel and Michael Butler. ProB: A model checker for B. In Keijiro Araki, Stefania Gnesi, and Dino Mandrioli, editors, International Symposium on Formal Methods (FM), 2003. URL: https://doi.org/10.1007/978-3-540-45236-2_46.
  22. Dor Ma'ayan, Wode Ni, Katherine Ye, Chinmay Kulkarni, and Joshua Sunshine. How domain experts create conceptual diagrams and implications for tool design. In Proceedings of the 2020 CHI Conference on Human Factors in Computing Systems, pages 1-14, 2020. URL: https://doi.org/10.1145/3313831.3376253.
  23. John Maloney, Mitchel Resnick, Natalie Rusk, Brian Silverman, and Evelyn Eastmond. The Scratch programming language and environment. ACM Transactions on Computing Education (TOCE), 10(4):1-15, 2010. URL: https://doi.org/10.1145/1868358.1868363.
  24. Niloofar Mansoor, Hamid Bagheri, Eunsuk Kang, and Bonita Sharif. An empirical study assessing software modeling in Alloy. In 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), pages 44-54. IEEE, 2023. URL: https://doi.org/10.1109/FORMALISE58978.2023.00013.
  25. Lean Manual. The user-widgets system. https://lean-lang.org/lean4/doc/examples/widgets.lean.html, 2024. [Accessed Nov 19, 2024].
  26. Vajih Montaghami and Derek Rayside. Bordeaux: A tool for thinking outside the box. In Fundamental Approaches to Software Engineering: 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings 20, pages 22-39. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54494-5_2.
  27. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pages 625-635. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  28. Lekha Nair, Sujala Shetty, and Siddhanth Shetty. Interactive visual analytics on big data: Tableau vs D3.js. Journal of e-Learning and Knowledge Society, 12(4), 2016. Google Scholar
  29. Mitchell J. Nathan, Kenneth R. Koedinger, and Martha W. Alibali. Expert blind spot: When content knowledge eclipses pedagogical content knowledge. In Proceedings of the Third International Conference on Cognitive Science, pages 644-648, 2001. URL: https://api.semanticscholar.org/CorpusID:14779203.
  30. Mitchell J Nathan and Anthony Petrosino. Expert blind spot among preservice teachers. American Educational Research Journal, 40(4):905-928, 2003. Google Scholar
  31. Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An extensible user interface for Lean 4. In Adam Naumowicz and René Thiemann, editors, Interactive Theorem Proving, volume 268 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:20, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.24.
  32. Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney LeVine, Julianne Rudner, Ben Ryjikov, Alexander Varga, Andrew Wagner, Luke West, and Shriram Krishnamurthi. Forge: A tool and language for teaching formal methods. Proceedings of the ACM on Programming Languages, 8(OOPSLA1):613-641, 2024. URL: https://doi.org/10.1145/3649833.
  33. Ulrich Neumerkel and Stefan Kral. Declarative program development in Prolog with GUPU. arXiv preprint cs/0207044, 2002. Google Scholar
  34. Ulrich Neumerkel, Christoph Rettig, and Christian Schallart. Visualizing solutions with viewers. In LPE, pages 43-50, 1997. Google Scholar
  35. Sandra Pauletto and Andy Hunt. A toolkit for interactive sonification. In ICAD, 2004. Google Scholar
  36. Chris Pettitt and contributors. Dagre: A JavaScript library for directed graph layouts. https://github.com/dagrejs/dagre, 2014. Accessed: 2024-11-21.
  37. Josh Pollock, Catherine Mei, Grace Huang, Elliot Evans, Daniel Jackson, and Arvind Satyanarayan. Bluefish: Composing diagrams with declarative relations. In Proceedings of the 37th Annual ACM Symposium on User Interface Software and Technology, pages 1-21, 2024. URL: https://doi.org/10.1145/3654777.3676465.
  38. Siddhartha Prasad, Ben Greenman, Tim Nelson, and Shriram Krishnamurthi. sidprasad/copeanddrag. Software, (visited on 2025-06-16). URL: https://github.com/sidprasad/copeanddrag/tree/ecoop-25
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23608
  39. Helen Purchase. Which aesthetic has the greatest effect on human understanding? In International Symposium on Graph Drawing, pages 248-261. Springer, 1997. URL: https://doi.org/10.1007/3-540-63938-1_67.
  40. Derek Rayside, Felix Sheng-Ho Chang, Greg Dennis, Robert Seater, and Daniel Jackson. Automatic visualization of relational logic models. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 7, 2007. URL: https://doi.org/10.14279/tuj.eceasst.7.94.
  41. Lothar Spillmann, editor. On Perceived Motion and Figural Organization. MIT Press, 2012. Includes English translations of Max Wertheimer’s 1912 and 1923 papers on Gestalt psychology. Google Scholar
  42. Ion Stoica, Robert Morris, David Karger, M Frans Kaashoek, and Hari Balakrishnan. Chord: A scalable peer-to-peer lookup service for internet applications. ACM SIGCOMM computer communication review, 31(4):149-160, 2001. URL: https://doi.org/10.1145/383059.383071.
  43. J Ridley Stroop. Studies of interference in serial verbal reactions. Journal of experimental psychology, 18(6):643, 1935. Google Scholar
  44. John Sweller and Paul Chandler. Evidence for cognitive load theory. Cognition and instruction, 8(4):351-362, 1991. Google Scholar
  45. Edward R. Tufte. The Visual Display of Quantitative Information. Graphics Press, Cheshire, CT, 1983. Google Scholar
  46. Barbara Tversky. Spatial schemas in depictions. In M. Gattis, editor, Spatial schemas and abstract thought, pages 79-112. The MIT Press, 2001. Google Scholar
  47. Michelle Werth and Michael Leuschel. VisB: A lightweight tool to visualize formal models with SVG graphics. In Rigorous State Based Methods, pages 260-265, 2020. URL: https://doi.org/10.1007/978-3-030-48077-6_21.
  48. Max Wertheimer. Experimentelle studien über das sehen von bewegung. Zeitschrift für Psychologie, 61:161-265, 1912. Google Scholar
  49. Benjamin W White. Interference in identifying attributes and attribute names. Perception & Psychophysics, 6:166-168, 1969. Google Scholar
  50. David Wren. animate-lean-proofs, 2021. Accessed: 2024-11-22. URL: https://github.com/dwrensha/animate-lean-proofs.
  51. Katherine Ye, Wode Ni, Max Krieger, Dor Ma'ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, and Keenan Crane. Penrose: from mathematical notation to beautiful diagrams. ACM Transactions on Graphics (TOG), 39(4):144-1, 2020. Google Scholar
  52. Jonathan Zong, Isabella Pedraza Pineros, Mengzhu Chen, Daniel Hajas, and Arvind Satyanarayan. Umwelt: Accessible structured editing of multi-modal data representations. In Proceedings of the 2024 CHI Conference on Human Factors in Computing Systems, pages 1-20, 2024. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact