TY - GEN
T1 - Auto-Generating Visual Editors for Formal Logics with Blockly
AU - Ferrando, Angelo
AU - Lu, Peng
AU - Malvone, Vadim
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.
PY - 2026/1/1
Y1 - 2026/1/1
N2 - Formal logics are central to the specification and verification of computational systems, yet their adoption outside highly specialised domains is hindered by steep learning curves and error-prone textual notations. Making these notations more approachable is particularly important in education and in settings where non-expert stakeholders need to engage with formal reasoning. We present a framework that automatically generates block-based visual editors for formal logics using the Blockly library. From a structured JSON specification of syntax and composition rules, our tool produces browser-based editors in which formulas are constructed by combining graphical blocks rather than writing code. This approach lowers syntactic barriers for learners and non-experts, while allowing experts to define new logics without manual interface design. Although integration with verification backends is planned, the tool already provides a reusable foundation for accessible and customisable logic editors.
AB - Formal logics are central to the specification and verification of computational systems, yet their adoption outside highly specialised domains is hindered by steep learning curves and error-prone textual notations. Making these notations more approachable is particularly important in education and in settings where non-expert stakeholders need to engage with formal reasoning. We present a framework that automatically generates block-based visual editors for formal logics using the Blockly library. From a structured JSON specification of syntax and composition rules, our tool produces browser-based editors in which formulas are constructed by combining graphical blocks rather than writing code. This approach lowers syntactic barriers for learners and non-experts, while allowing experts to define new logics without manual interface design. Although integration with verification backends is planned, the tool already provides a reusable foundation for accessible and customisable logic editors.
KW - Block-Based Specification
KW - Blockly
KW - Logic Editor Generation
UR - https://www.scopus.com/pages/publications/105022907523
U2 - 10.1007/978-3-032-10794-7_22
DO - 10.1007/978-3-032-10794-7_22
M3 - Conference contribution
AN - SCOPUS:105022907523
SN - 9783032107930
T3 - Lecture Notes in Computer Science
SP - 451
EP - 459
BT - Integrated Formal Methods - 20th International Conference, iFM 2025, Proceedings
A2 - Damiani, Ferruccio
A2 - Farrell, Marie
PB - Springer Science and Business Media Deutschland GmbH
T2 - 20th International Conference on integrated Formal Methods, iFM 2025
Y2 - 19 November 2025 through 21 November 2025
ER -