GNATprove Tips and Tricks: a Lemma for Sorted Arrays
by Sylvain Dailler –
A few weeks ago, we began, working on a new feature that might help users to prove the correctness of their programs manipulating sorted arrays. We report on the creation of the first lemma of a new unit on arrays in the SPARK lemma library.
The objective is to provide users with a way to prove some complex properties on programs (complex for SMT-based automatic provers). The lemmas are written as ghost procedures with no side-effects. They are proved in SPARK and their postcondition can be reused by provers by calling the procedure.
In particular, our first lemma is on the transitivity of the order in arrays. It is used to refine this (simplified) assertion on an array Arr that states that the array is sorted by comparing adjacent elements:
(for all I in Arr'Range =>
(if I /= Arr'First then
Arr (I - 1) < Arr (I)))into this equivalent expression that the array is sorted by comparing any two elements:
(for all I in Arr'Range =>
(for all J in Arr'Range =>
(if I < J then Arr (I) < Arr (J))))This new condition is logically equivalent to the first one, but in practice it can be used by SMT provers when we need to compare two elements of the sorted array that are not adjacent. In some rare cases, provers like CVC4 ans Z3 are able to prove that the two conditions are equivalent, but this requires doing inductive reasoning which is very partially supported in such provers. So, in general, SMT provers are just unable to prove it. This is the reason for us providing this new lemma, that we proved once and for all (using the Coq proof assistant).
How to use it:
First, import the spark_lemmas library into your project file.
with "spark_lemmas";To use this lemma on an array Arr, you first need to instantiate the package SPARK.Unconstrained_Array_Lemmas with your own array index type (Index_Type), array element type (Element_T), ordering function on Element_T (Less) and create an unconstrained array type as follow:
type A is array (T_Index range <>) of T_Value;You can now instantiate the generic package:
package Test is new SPARK.Unconstrained_Array_Lemmas
(Index_Type => Index_Type,
Element_T => Element_T,
A => A,
Less => "<");To use it on an array Arr, you only need to cast your array type into A and apply the lemma:
Test.Lemma_Transitive_Order (A (Arr));Safety conditions:
Note that this lemma relies on a meta argument of correctness on the types and function we use to instantiate it. For usability reasons, we used a SPARK_Mode => Off on the library code so that users are not polluted with Coq proved conditions (also they would have needed to install Coq to get a complete proof). We proved this lemma completely in Coq for instances of the types and transitive order. And because our proof does not depend on the size and bounds of the types, which are the only semantic differences visible from the lemma implementation, user instantiated lemmas should also be correct.
So, if you are a user of SPARK and find difficult proofs in your code that would fit in a library like this one, please contact us, we might be able to provide lemmas for your problems on some cases.