Skip to content

Code Conventions

Jump to bottom
Kassing edited this page Mar 30, 2026 · 1 revision

Eclipse Settings

Also have a look at Configure Eclipse where several mandatory settings are explained which also take care of aspects like code formatting.

Code Style

  • The project language is English. Use English for all identifiers, comments and documentation, whatever your mother tongue may be.

  • Please use the code formatter that is set up in Configure Eclipse before committing to the main branch. E.g., use 4 spaces instead of tabs.

  • Please do not use save actions that cause many modifications, which might lead to merge conflicts.

  • Put javadoc comments on top of each class and above each public method (apart from those where the semantics are really obvious). Use comments also inside your code, the person who will maintain your code (i.e., until you leave the project: you) will be grateful for this. Don't just explain what you did, but why you did it (the rationale for your code).

  • Problem classes and data structures should be immutable if possible. This decreases the possibility of very nasty bugs. If it is not immutable, then there is a good, documented-with-comments reason not to.

Good Code

Exceptions:

Throw specific exceptions: Do not write throw new Exception();, but write throw new MyFooException(); instead. Here, MyFooException is a new class that extends Exception or RuntimeException. Reason: If you throw a new Exception(), the caller of your method will have to catch any Exception, although many RuntimeExceptions like NullPointerException or ArrayOutOfBoundsException that may originate from code that you have called usually should not be caught. Instead, they should be allowed to lead to a program crash, because they may indicate severe bugs that need to be detected and fixed.

Stick to the Java Collection Rules:

Stick to the java collections rules on equals, hashCode, and compareTo methods unless there is a good, documented-with-comments reason not to, specifically:

  • equals should be symmetric, i.e. a.equals(b) should be true iff b.equals(a). This is easily violated when you override a superclass equals() implementation with your own
  • When implementing equals, you must implement hashCode too (otherwise, the requirement a.equals(b) => (a.hashCode() == b.hashCode()) will be violated)
  • compareTo should only return 0 when the objects are equal, specifically, you should throw ClassCastException, not return 0, when an object cannot be compared. (Something to keep in mind is that a TreeMap / TreeSet will not call equals, when compareTo returns 0 it will assume "already in there")
  • usually, implement the generic version of compareTo, this will keep you from having to bother with casting in the first place.

Assertions:

Use assertions in order to make sure that certain properties hold, but wrap them inside if (Globals.useAssertions) { /* your assertions */ } where Globals is aprove.Globals. This is a good idea because there is no better way to tell the compiler to exclude the assertion code from compilation, which (for complicated assertions that pre-compute some data before the actual assert-statement) is desired for maximum performance of AProVE. Note that you should never put any code with side effects inside an if (Globals.useAssertions) block. Doing so may lead to some really nasty bugs that are hard to track down. Assertions are meant for detecting erroneous program behavior, not for correcting it!

We enforce whether assertions are to be checked at runtime or not (so that starting aprove in the "wrong" assertion mode will fail, at least if you have not set the debug mode to NONE in aprove.Globals). This is done via the flag aprove.Globals.useAssertions. Nowadays assertions should be enabled all the time, though.

Output for Debugging

To write some outputs for debug without loss of efficiency you should wrap your debug outputs in an if-block. The if-condition is a static final boolean so that the compiler is able to remove unused stuff. Each member of the AProVE team has her/his own constant in aprove/Globals.java. To use your wrapped debugging code, you have to replace the following line in aprove/GlobalSettings.java

private static final long DEBUG_MODE = NONE; by: private static final long DEBUG_MODE = DEBUG_#username;

where DEBUG_#username should be the constant of the team member whose debugging code you would like to use. To use debugging code of more than one team member, just sum up the constants, e.g.

private static final long DEBUG_MODE = DEBUG_#user1 + DEBUG_#user2;

But make sure that you do not commit your modified Globals.java file.

Clone this wiki locally