Development Log

  • SPARK Pro
    Jul 19th, 2017

    Automatically unroll static loops w/o loop invariant
    Loop invariants are a known difficulty for beginners to use formal program verification. At the same time, many loops written in exercises and to familiarize oneself with the technology have static bounds and a small range. This enhancement implements loop unrolling for such loops with static bounds and not too many iterations (current threshold is at 20 iterations maximum). This way, simple loops with static bounds are proved without requiring a loop invariant. We let the user decide if she wants to use this feature or not: - by only unrolling FOR loops that have no loop (in)variant. - by disabling this feature when the switch --no-loop-unrolling is used.