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.

General information

ID58
Articlenone
Back-endSilicon
LanguageJava
FeaturesArrays, Sequences, Summation patterns
Sources
Path to example filefloats/TestHist.java
Date2017-06-16

Statistical information

Lines of code34 lines (comments not included)
Lines of specification15 lines (44.12% of the total)
Computation time71529 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.