This verification example contains summations (i.e. the use of "\sum" expressions) over sequences of floats. Both passing and failing cases are included.
|Features||Arrays, Floats, Sequences, Summation patterns|
|Path to example file||floats/TestFloat.java|
|Lines of code||89 lines (comments not included)|
|Lines of specification||32 lines (35.96% of the total)|
|Computation time||57872 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.