Commons Math is a library of lightweight, self-contained mathematics and statistics components addressing the most common problems not available in the Java programming language or Commons Lang.

http://commons.apache.org/proper/commons-math/

Issue 835: https://issues.apache.org/jira/browse/MATH-835

Problem:

The percentageValue() method of the Fraction class works by first multiplying the Fraction by 100, then converting the Fraction to a double. This causes overflows when the numerator is greater than Integer.MAX_VALUE/100, even when the value of the fraction is far below this value.

Test case:

Expected:

percentage = 100 * ((double) numer) / denom

Inteads:

percentage < 0 (due to overflow)

Add this assertion into org.apache.commons.math3.fraction.Fraction.percentageValue() at line 599:

assert numerator >= 0 ? result >= 0 : true;

org.apache.commons.math3.fraction.Fraction:599 (debugLine: 603) suspiciousness: 0.96 Logic: result >= -0.0 Accuracy: 1 org.apache.commons.math3.fraction.Fraction:600 (debugLine: 604) suspiciousness: 0.96 Logic: result >= -0.0 Accuracy: 1 org.apache.commons.math3.fraction.Fraction:555 (debugLine: 558) suspiciousness: 0.92 Logic: fraction.numerator >= -0.0 Accuracy: 1 org.apache.commons.math3.fraction.Fraction:557 (debugLine: 560) suspiciousness: 0.92 Logic: fraction.numerator >= -0.0 Accuracy: 1

The following predicate is output:

fraction.numerator >= -0.0 (org.apache.commons.math3.fraction.Fraction:557)

We feed the passed test cases from Ziyuan to Daikon. After a while, Daikon creates a lot of invariants (file). We check the invariants inside the functions multiply() and percentageValue(). However, no useful invariants has been found.