Semantic rule engine for QML. Verifying semantic rules using computational tree logic

Abstract

One of the most common tools used for verifying code quality in programming languages are linter programs. However, in many cases, specifically in new languages, there is no such tool. An example of such a language is QML. In this thesis this tooling issue is addressed by designing a rule engine, together with rules defined in a dedicated language. The idea is to use the rule engine as a framework for creating lint tools for any programming language and evaluate this by creating a sample implementation of a lint tool for QML. In order to make the rule engine agnostic to which programming language that is being verified, the rules described in the rule language will describe structural restrictions of the abstract syntax tree produced from the source code. Moreover, in order to make the rule language as expressive as possible it is constructed as a dialect of Computational Tree Logic (CTL). Although CTL is a logic traditionally used to describe temporal properties of infinite trees, CTL fundamentally only describes structural properties of a tree and all its possible sub-trees which makes it a great foundation for our purposes. An additional feature of using a dedicated language to define rules is that the rule engine becomes agnostic to what rules that are defined as well. Meaning that if a user wants to change, add or delete rules only the rule file has to be changed and nothing needs to be recompiled. By using this approach, this thesis solves both the lint tool issue for QML and creates a framework for defining lint tools for any other programming language as well.