===================== Tools and Performance ===================== Tools used =========== The following tools were used: - GNATprove 0.2w (20130414) - GPS 5.3.0w (20130415) - GNAT Pro 7.2.0w (20130414-47) - SPARK Pro toolset 11.0.0 Performance =========== The results reported in this section are from analysis on a desktop PC (i7 860, 2.8GHz, 4 CPUs, 6Gb RAM) running 64-bit Linux (Debian). The timings for GNATprove were generated by running "Clean Proofs" followed by "Prove Subprogram" from within GPS and noting the elapsed time reported in the Messages tab. It is acknowledged that these times include the time spent by GNATprove analysing and generating VCs as well as the time spent by Alt-Ergo attempting to discharge the VCs, plus any additional overhead from GPS. The SPARK 2005 timings were generated by running the command "time spadesimp subprog.vcg" and taking the reported 'real' time on the assumption that this is closest to the measure reported by GPS. (The Simplifier executable is called spadesimp.) It is acknowledged that this does not include the time spent by the Examiner analysing and generating VCs, although this has been measured separately and is only 00.15s in total for all seven subprograms in the fisr example (Exchange). For GNATprove (SPARK 2014) the option -j4 was used to specify 4 parallel processes to make use of the available processors. For SPARKsimp (SPARK 2005) the equivalent option -p=4 was used. Exchange procedure ================== ================================ ================== ================== ======== Subprogram GNATprove SPARK 2005 Comments ================================ ================== ================== ======== Exchange Proved 00.56s Proved 00.08s Exchange_No_Post Proved 00.30s Proved 00.08s Exchange_No_Post_Unused Proved 00.35s Proved 00.08s Exchange_No_Post_Uninitialized Proved 00.35s Not proved 00.08s 1 Exchange_With_Post_Unused Not proved 01.55s Not proved 00.09s 2 Exchange_With_Post_Uninitialized Not proved 01.47s Not proved 00.10s 2 Exchange_RTE Not proved 01.77s Not proved 00.11s 2 ================================ ================== ================== ======== Comments: #. Uninitialized variable results in unprovable (false) VCs in SPARK 2005. This is detected by GNATprove when run in flow analysis mode. #. VCs not provable due to deliberate error. GNATprove timings reflect the 1s timeout used. Stacks, Queues and QueueOperations ================================== ================================ ================== ================== ======== Subprogram GNATprove SPARK 2005 Comments ================================ ================== ================== ======== ReverseQueue Proved 00.40s Proved 00.08s ================================ ================== ================== ======== Stacks, Queues and QueueOperations with Proof ============================================= ================================ ================== ================== ======== Subprogram GNATprove SPARK 2005 Comments ================================ ================== ================== ======== ReverseQueue Proved 06.06s Proved 00.59s 1 ================================ ================== ================== ======== Comments: #. The timeout for GNATprove was increased to 2s for this example. The SPARK 2005 time consists of 0.516s for the Simplifier to prove 25 out of 27 VCs and 0.069s for Victor + Alt-Ergo to prove the remaining 2 VCs. Central Heating Controller ========================== RTE Proof --------- ================================ ================== ================== ======== Subprogram GNATprove SPARK 2005 Comments ================================ ================== ================== ======== HeatingSystem_DFA Proved 02.79s Proved 01.71s ================================ ================== ================== ======== Correctness Proof ----------------- ================================ ================== ================== ======== Subprogram GNATprove SPARK 2005 Comments ================================ ================== ================== ======== HeatingSystem_Proof Proved 08.41s Proved 02.64s 1 ================================ ================== ================== ======== Comments: #. There were 97 SPARK 2005 VCs of which 96 were proved by the Simplifier and the remaining one was proved by Victor + Alt-Ergo. GNATprove generated and proved 37 VCs. Advanced SPARK 2005 Training Course =================================== ================================ ================== ================== ======== Subprogram GNATprove SPARK 2005 Comments ================================ ================== ================== ======== Increment Proved 00.61s Proved 00.14s Increment2 Proved 00.88s Proved 00.17s Swap, NandGate, NextDay_* (t1q3) Proved 01.32s Proved 00.55s 1 Swap, NandGate, NextDay_* (alt) Proved 01.32s Proved 00.46s ISQRT Proved 02.18s Proved 00.29s Bounded_Add Proved 01.12s Proved 00.34s 2 Raise_To_Power Not proved Not proved 3 ================================ ================== ================== ======== Comments: #. These are the combined times for proving all the subprograms named as they are all located in the same package. (Timings for individual subprograms could be obtained by using 'Prove Subprogram' with GNATprove and by proving the individual VC files with the SPARK 2005 tools if this information was required.) GNATprove generates and discharges checks for four postconditions and a range check. The SPARK 2005 tools generate and discharge 24 VCs of which 23 are discharged by the Simplifier and the remaining one requires Victor + Alt-Ergo. #. Of the 15 SPARK 2005 VCs, 14 were discharged by the Simplifier and 1 by Victor + Alt-Ergo. #. Come back to this - open todo item in main body of report. Array Examples ============== ================================ ================== ================== ======== Subprogram GNATprove SPARK 2005 Comments ================================ ================== ================== ======== T2Q1.Swap Proved 00.56s Proved 00.20s T2Q2.Clear Proved 00.51s Proved 00.16s T2Q3.Find Proved 00.51s Proved 00.17s 1 T2Q4.Clear Proved 02.63s Proved 00.42s 2 T2Q5.MaxElement_P1B1 Proved 01.52s Proved 00.27s T2Q5.MaxElement_P2B1 Not proved 03.09s Proved 00.53s T2Q5.MaxElement_P3B1 Proved 00.86s Proved 00.10s 4 T2Q5.MaxElement_P1B2 Proved 01.62s Proved 00.38s T2Q5.MaxElement_P2B2 Not proved 03.29s Proved 00.83s 3 T2Q5.MaxElement_P3B2 Proved 01.11s Proved 00.12s T2Q5.MaxElement_P1B3 Proved 01.72s Proved 00.31s T2Q6.SumArray Proved 11.08s Proved 00.40s 5 T2Q6.SumArray_Shift Proved 09.37s Proved 00.80s 5 T2Q7.Find Proved 01.08s Proved 00.23s T2Q8.CreateFibArray Not proved 13.42s Not proved 16.62s T2Q8.CreateFibArray_RTCOnly Not proved 13.20s Not proved 16.40s ================================ ================== ================== ======== #. T2Q3 is not mentioned in the body of the report as it is identical to T2Q7 but without a postcondition. #. Of the 9 SPARK 2005 VCs, 7 were discharged by the Simplifier and 2 by Victor + Alt-Ergo. #. See observation and explanation in main body of report. #. In fact GNATprove does not generate or prove any VCs as this example is so trivial. #. The GNATprove timeout was increased to 12s. Further Advanced SPARK course examples ====================================== ================================ ================== ================== ======== Subprogram GNATprove SPARK 2005 Comments ================================ ================== ================== ======== T3Q1.Swap and Rotate3 (combined) Proved 01.32s Proved 00.39s 1 T3Q2.Double and Quadruple Proved 01.27s Proved 00.29s T3Q3.DoNothing Not proved 03.70s Not proved 1m49s T3Q4.SumArray Proved 04.60s Proved 00.45s 2 T3Q5.* (Sorting algorithm) Not proved 10.92s Proved 20.22s 3 ================================ ================== ================== ======== #. Of the 8 SPARK 2005 VCs 7 were proved by the Simplifier and 1 by Victor + Alt-Ergo. #. Of the 6 SPARK 2005 VCs 4 were proved by the Simplifier and 2 by Victor + Alt-Ergo. #. There were 32 SPARK 2005 VCs. 24 were proved by the Simplifier, 1 requiring a user-defined rule. The remainder were discharged by Victor + Alt-Ergo. Tokeneer ======== ================================ ================== ================== ======== Analysis GNATprove SPARK 2005 Comments ================================ ================== ================== ======== All core (SPARK) files 62% proved 06m49s 100% proved 06m07s 1 AuditLog 88% proved 00m38s 100% proved 01m46s 2 ================================ ================== ================== ======== #. GNATprove was run with a timeout of 5s. The SPARK 2005 proof tools were invoked via the command "sparksimp" with the default settings. As discussed in the body of the report, the full conversion to SPARK 2014 is not complete so it is not possible to make a meaningful comparison between these results. It should also be noted that of the 2433 SPARK 2005 VCs, 100 (4%) were discharged with the aid of user-defined proof rules and 23 (1%) were discharged by manual review. One VC is discharged by Victor + Alt-Ergo, although this was discharged by manual review in the original Tokeneer development (as SPARKbridge was not available at the time). If the original manual review file is reinstated and Victor is not used then the total proof time drops from 6m07s to 1m39s. #. For the SPARK 2005 version of the code, the AuditLog package produces the 1 VC in Tokeneer that is proved by Victor + Alt-Ergo. If Victor is not invoked and the original manual review file is reinstated then the proof completes in 8 seconds. The GNATprove results were generated with a timeout of 5s. Reducing this timeout to 1s halves the time taken for the proof but with one fewer VC proved. It is possible that increasing the timeout further would result in more VCs being proved at the expense of a longer analysis time, although increasing the timeout to 300s does not prove any additional VCs (but increases the total time to 15m47s).