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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Auto-Generating Visual Editors for Formal Logics with Blockly

  • Angelo Ferrando,
  • Peng Lu,
  • Vadim Malvone

摘要

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.