2020/06/05 by Boro Sitnikovski, Sitnikovski, Boro · 1 voice
Computer Science · #cs.LO
paper · pdf · doi:10.48550/arxiv.2006.03525
Text editors represent one of the fundamental tools that writers use - software developers, book authors, mathematicians. A text editor must work as intended in that it should allow the users to do their job. We start by introducing a small subset of a text editor - line editor. Next, we will give a concrete definition (specification) of what a complete text editor means. Afterward, we will provide an implementation of a line editor in Coq, and then we will prove that it is a complete text editor.