Riposte is a tool to support developers in verifying SPARK programs. The SPARK Examiner generates verification conditions (VCs) that show that the SPARK program is type safe, free from run-time exceptions and meets the specification given in post conditions and checks. Existing tools allow true VCs to be proven automatically. Riposte augments these capabilities by generating counter examples for false VCs. These counter examples give variable assignments that cause violations in type safety, trigger exceptions or inputs that do not meet the required post conditions. The programmer can then use these to locate and fix bugs or refine the program’s specification.
The current release of Riposte is at an alpha stage and is intended to be a technology demonstration. Suggestions and feature requests are most welcome. To download the tool, please visit the Riposte project page on the Open-DO Forge.