Contributions to the JML project : safe arithmetic and non-null-by-default