Learning about SPARK dependency contracts

General
1

I’m learning SPARK, and I’m facing an error that I don’t understand. With this example I’ve written to practice dependency contracts (even if identifiers are in Spanish, I think will be easy to understand):

package Contactos
with
 SPARK_Mode => On,
 Abstract_State => Estado
is

  type Resultado_T is (Exito, Nombre_Demasiado_Largo, Espacio_Insuficiente);

  type Telefono_T is range 1 .. 999_999_999;

  procedure Inicializar
  with
    Global => (Output => Estado),
    Depends => (Estado => null);

  procedure Agregar_Contacto
    (Nombre : String;
     Telefono : Telefono_T;
     Resultado : out Resultado_T)
  with
    Global => (In_Out => Estado),
    Depends => (Estado => +(Nombre, Telefono),
                Resultado => (Nombre, Estado));

end Contactos;


package body Contactos
with
  Spark_Mode => On,
  Refined_State => (Estado => Array_Contactos)
is

   Longitud_Nombre : constant := 64;
   subtype Indice_Nombre is Positive range 1 .. Longitud_Nombre;
   subtype Nombre_T is String (Indice_Nombre);

   type Persona is
      record
         Nombre : Nombre_T;
         Telefono : Telefono_T;
         Usado : Boolean;
      end record;


   Capacidad_Array : constant := 128;
   subtype Indice_Array is Positive range 1 .. Capacidad_Array;
   type Array_Personas_T is array (Indice_Array) of Persona;

   Array_Contactos : Array_Personas_T;

   procedure Inicializar is
   begin
      for Contacto of Array_Contactos loop
         Contacto :=
           (Nombre => (others => ' '),
            Telefono => Telefono_T'Last,
            Usado => False);
      end loop;
   end Inicializar;

   procedure Agregar_Contacto
     (Nombre : String; Telefono : Telefono_T; Resultado : out Resultado_T)
   with
     Refined_Global => (In_Out => Array_Contactos),
     Refined_Depends => (Array_Contactos => +(Nombre, Telefono),
                         Resultado => (Nombre, Array_Contactos))
   is
      Encontrado : Boolean := False;
   begin

      if Nombre'Length > Nombre_T'Length then
         Resultado := Nombre_Demasiado_Largo;
      else

         Resultado := Espacio_Insuficiente;

         for Contacto of Array_Contactos loop
            if not Contacto.Usado then
               Encontrado := True;
               Contacto.Nombre (Contacto.Nombre'First .. Nombre'Length) := Nombre;
               Contacto.Telefono := Telefono;
               Contacto.Usado := True;
            end if;
         end loop;
      end if;

      if Encontrado then
         Resultado := Exito;
      end if;

   end Agregar_Contacto;

end Contactos;

gnatprove prints this error:

gnatprove -P contactos.gpr contactos.adb |cat
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

contactos.adb:41:26: medium: missing dependency "Resultado => Telefono"
   41 |                         Resultado => (Nombre, Array_Contactos))
      |                         ^~~~~~~~~

Why is it seeing a dependency between Resultado and Telefono? What should a SPARK programmer do in this case?

2

Hi Manu,

I also fail to see why it is giving you this warning… But it may have to do with the global state… Array_Contactos depends on Telefono as indicated in Refined_Depends => (Array_Contactos => +(Nombre, Telefono), and Resultado depends on Array_Contactos as indicated in the following line Resultado => (Nombre, Array_Contactos)). This is just a complete guess from my side. Since Telefono is a direct input to the procedure, SPARK may want to make the dependence also explicit.

The first thing I would do is increase the level of the SPARK proof. My guess is that the default proof level is not pushing the provers to their limit or it may not be using all of them. Therefore, it may jut not check the entire Depends tree.

I also know that SPARK has a “counter” proof option within the GNAT Studio IDE (possibly also through the CLI) that should explain why SPARK believes something to fail.

Best regards,
Fer

3

Thanks, Fer. I’ve found now the problem after trying your proposals. They didn’t work, but I tried further to analyze my code and in fact it contained a bug! So SPARK was indeed finding something weird, although I don’t really understand how could it warn about that missing dependency when the problem was another, although it didn’t have information for discovering the real bug.

The bug is that I don’t exit from the loop when the free node has been found, that means that all the free nodes were written with the input. How that comes to the missing dependency to Telefono I don’t know, but after just adding the missing exit inside the if not Contacto.Usado then, the dependency error is gone.

So in a case like this, I guess you have to review your assumptions about your code, because they might be false. This is after all the mission of SPARK.

1 Like
4

By the way, with the --flow-debug switch [1] I get the same output (besides the error) when the exit is present and when not, so it doesn’t give a clue about why it is coming to that conclusion.

[1] See output in How does `gnatprove --flow-debug` use graphviz?

5

I am glad the problem is solved! Just for future reference, I gave the SPARK manual a very light read and I found a couple of flags that may help in the future:

--info: which should output information about the decisions that SPARK is taking.
--counterexamples=on: enable counter examples, see 7.2. How to View GNATprove Output — SPARK User's Guide 25.0w
--level=4, which is equivalent to --prover=cvc5,z3,altergo --timeout=60 --memlimit=2000 --steps=0 --counterexamples=on
And finally, SPARK has a hard time with loops, see 7.9.2. Loop Examples — SPARK User's Guide 25.0w for more info on how to properly deal with loops in SPARK.

Best regards,
Fer

1 Like
6

I’m an Emacs and command-line addict and haven’t looked yet to what benefits GNAT Studio provides for SPARK, but I should give it a try, at least to know if I’m missing something :slight_smile:

1 Like