Counting test

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.

General Information

  • Backend: Silicon
  • Language: Java
  • Features: Sequences, Arrays, Summation patterns
  • Path to Example File: floats/
  • Should Verify: Yes
  • Date: 2017-06-16
  • Lines of Code: 44 (comments not included)
  • Lines of Specification: 21 (47.7% of total)
  • Computation Time: 39.7 seconds