Text editing and beyond a study in logic modeling

摘要

This paper presents a logic modeling exercise in which we develop, test and implement a logic model for a text editor and use it to test existing text editing software. We begin by presenting a first order Horn logic axiomatization of a text editor by providing domain equations for the primitive operations insert, delete and character retrieval. We show that this logic model captures the essential aspects of the text editing task and how more complex features are built using these primitives. We discuss possible implementations and conclude that any operational semantics — the set of algorithms that perform the task — must be strongly related to the logic model we present. In other words, each operational semantics constitutes a model of the logic theory. Next, we illustrate the usefulness of the model by implementing a basic text editing system and testing the correctness of an existing text editor. We conclude by describing how we are integrating these modeling techniques into a larger and more complex knowledge-based system.