Spectre Implementation Style

Design Guidelines

We want to make the code easy to understand, in particular for new users.

The most important way to achieve this is to make independence of components explicit (If I want to understand component A and if I know that components A and B are independent, I don’t need to even look at B).

• The implementation should consist of components, where each component has a single task. E.g. the parser should not contain the analysis engine.
• If two components are independent, they should not interact with each other. E.g. the parser engine is independent from the analysis engine, so neither of them should call the other. Solution in this case: Let the main method both call the parser and feed the result into the analysis engine.
• Whenever possible, make the objects, which are passed around, constant. Note that doing so requires that all functions are const-correct.

We don’t need to be very efficient

• This is a research prototype and not an industrial-strength project
• Most of the work is done by Vampire anyways, independent from how efficient our code is.
• If there is a tradeoff between efficient code and code which is easy to read, choose readability,

Writing modern C++

• it’s encouraged to use C++11 features in Spectre. E.g. smart pointers in order to make memory management trivial (to both implement and understand) in most of the cases.
• It’s possible to use C++14 and C++17 features, if they improve readability.
• if there is already a solution in the standard library (STL), use that solution, at least if you don’t have a strong reason to do otherwise (and performance is in 99% of the time not a strong reason)
• use CppCoreGuidelines https://github.com/isocpp/CppCoreGuidelines/blob/master/CppCoreGuidelines.md

Coding Style

• We use clang-format together with a custom style: style.clang-format in the main directory.
• apply clang-format before committing any file.