This verification example demonstrates summation patterns, that is, the use of "\sum" expressions to calculate summations over sequences. The program contains both passing and failing verification cases.
Arrays, Sequences, Summation patterns
Path to example file
Lines of code
44 lines (comments not included)
Lines of specification
21 lines (47.73% of the total)
Note, verification may take a while and has a time-out of 20 seconds.