Learning about SPARK dependency contracts

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?

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

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

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?

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

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

Hi.
What surprises me is that when you define an Abstract_State and mentions in in an output contract, then if said State is comprised of several variable, you are obliged in the refinement to mention not just the one variable than you use but all the State’s constituents. What’s the point of a refinement that won’t let you be precise ?

procedure Update (It: Iterator; Item: Element_type)
    with Global => (Output => Internal_List);
____________
package body Double_List
   with Refined_State => (Internal_List => (Memory, Count, Free_List, Free))

   procedure Update (It: Iterator; Item: Element_type)
      with Refined_Global => (Output => Memory) is
   begin
      Memory (It).Value := Item;
   end Update;

error: “Output” state “Internal_List” must be replaced by all its constituents in global refinement
error: constituent “Count” is missing in output list
error: constituent “Free_List” is missing in output list
error: constituent “Free” is missing in output list

What happens if you use this?

with Refined_Global => (Output => Memory, null => Count, Free_List, Free)

The refinement would be incorrect. Don’t forget that in SPARK, out parameters/globals need to be initialized by the subprogram. So from the outside it looks like you are initializing the entire state, while in reality you are only initializing part of it.

Yes, part of it, and that refinement is done in the body, that where we see and know that the abstraction is virtual. the program knows that such and such variables relate to the abstract state, so I don’t see that it makes sense to maintain that illusion in that place ?