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?
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.
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.
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.
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.
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
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
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 ?
→ Had to make it In_Out rather than Output. Ok so it works exactly like parameter modes.
Hi everyone ,
Can someone please put me through how i can install adacore on my system to begin programming? I’m new with it… A beginner, i need someone to walk me through this
A user here on the forum @AJ-Ianozi maintains a simple installer, that handles a lot of the stuff needed to get started called GetAda (not to be confused with GetAdaNow), you can find it here: https://www.getada.dev/
