Infrastructure to write tests

Test cases are important in AlgoVer. All data structures and algorithms in the core are to have test cases.

In order to be able to write them effectively, the following infrastructure is available:

Flags

Adding -Dalgover.verbose=true makes some test cases to produce more output. If your tests propduce lots of output, you are encouraged to make this output conditional using

if(TestUtil.VERBOSE) {
    // output code
}

to clutter the standard output less.

TestUtil.java

in package edu.kit.iti.algover.util in core/test:

• Project mockProject(String s):
  Create a project by parsing the string s as the content of a single dafny file. The filename is set to some bogus dummy filename.

• Project mockProject(DafnyTree t):
  If you already have a single tree (compilation unit), turn that into a project.

• Project mockProject(ProjectBuilder pb):
  If you already have a builder, turn that into a project.

• setField, call, callStatic, ...:
  In order to test private methods and fields, theses methods can be used, e.g.

// ...
TestUtil.class(o, "somePrivateMethodInSomeClass", param1, param2);

ProofMockUtil.java

in same package.

• makeProof(String termStr):
  Create a Proof object from a proof condition which makes the formula to show. Use the builtin symbols.

• makeProof(SymbolTable table, String termStr):
  see above. Use a specific table

• makeProof(Sequent sequent):
  Make proof for a particular sequent.

• `mockProofNode(...):
  ‼️ @JonasKlamroth

MockPVCBuilder.java

in package ...algover.proof. This class can be used to create arbitrary PVCs (which are not derived from a method or function).