GVim的TLA^+语言插件设计与实现

The Design and Implementation of TLA^+ Plugins for GVim

GVim是一款著名的编辑器,它允许用户为方便使用而自定义插件。TLA+语言是由Les-lie Lamport设计的基于行为时序逻辑的一门系统描述语言。本文描述了为GVim编写TLA+语言插件的详细步骤。这些插件提供了关键字高亮,插入模板,缩进,以及在图形界面下调用TLA模型检测的相关命令等功能,通过使用这些插件,在用TLA+语言描述系统时可明显提高编辑效率。

GVim is a famous editor; it allows people to write plugins for convenience. TLA^＋ is a on temporal logic of actions for specifying systems. It detailed procedure of writing TLA^＋ plugins for GVim. language based was invented by leslie Lamport. This paper describes the These plugins are written to speed up writing TLA^＋ code. This is done by highlighting code, inserting template, code indent, and introducing the method of call model checking commands in GVim.