Histogram with summations
Verification example of a method that calculates the histogram of an input array `a`. Summation patterns (i.e. the use of "\sum" expressions) are used in the verification.
|Features||Arrays, Sequences, Summation patterns|
|Path to example file||floats/TestHist.java|
|Lines of code||34 lines (comments not included)|
|Lines of specification||15 lines (44.12% of the total)|
|Computation time||71529 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.