Preliminary Draft Specification of the Sipelgatest_t1

Sipelgatest_t1 is a test coverage measurement tool that does not yet exist.


The ultimate goal of the project is to reduce, preferably eliminate altogether, the amount of text that has to be written to create tests.

Contemplation Version 0

May be in stead of writing pre-condition-like tests at the start of every/most functions, it might be possible to write only a few tests only once. Like: variables that start with prefix "s_" are always used as strings.

May be in an ideal world every major language has formal analysis toolset like the Ada has SPARC toolset. However, the world is not ideal and most libraries that "applied software developers" must depend on, are not written in languages that have a formal verification toolset.

As the creation of formal analysis tools for a main-stream language is, probably, beyond my (Martin Vahi) capabilities and probably requires years of work by a multi-member team, a practical solution might be to create a mostly programming language independent, simplistic, test-coverage toolset, which is the Sipelgatest_t1.

The answer to the question that why people can not switch to a language that has a formal verification toolset, is that software developers need to eat, need money and that means that people have to use the languages that allow to deliver products that clients, the non-freaks, non-programmers, want. On server side the Ada might do, but as of 2013 the only language that is bundled with all web browsers is JavaScript and that determines the language that money-earning software developers must use, no matter how bad it looks. The second option might be to use something that translates to JavaScript like the Google Dart or the Microsoft TypeScript, but as of 2013 those don't come with formal verification tools either.

Implementation Scheme

There's a third party parser based, Sipelgatest_t1 specific, translator that generates an instrumented version of the code. After instrumentation the start and end of every branch within the control flow has a test framework specific function that has GUID as its argument.

function foo() {
    if (cond_1() === true) {
    } else {
        if (cond_2 === true) {
        } else {
        } // else
    } // else
} // foo

The implementation of the instrumentation functions, the sipelgatest_t1_inc and the sipelgatest_t1_dec, writes the GUID to a global stack. The stack will be converted to string, where every GUID is at its own line, and test coverage tools will extract control flow information from that string and compare the paths that were taken during tests with paths that were possible by branching.

Not all paths can be taken, because correct code should not take a path like
    if (b_code_is_certainly_flawed === true) {
            throw(new Exception("This can't be happening ! "+
                                "Dear end-user, please call the panic department !"));
    } // if

Some Related Projects of Interest

Esprima, LLVM, ANTLR, Mozilla JavaScript Parser API, K-framework.

Contemplation Version 1

Try to define the Google Dart in the K-framework semantics. The hope is that due to the fact that the Dart is a typed language it is easier to define its semantics in K-framework terms than it would be for the JavaScript.