# Learning about SPARK dependency contracts **URL:** \ **Category:** General\ **Tags:** spark\ **Created:** [July 29, 2024, 6:27pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033 "2024-07-29T18:27:41Z")\ **Posts on this page:** 16\ **Page:** 1
**Author:** ![mgrojo](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/mgrojo/32/15_2.png) [@mgrojo](https://forum.ada-lang.io/u/mgrojo)\ **Post date:** [July 29, 2024, 6:27pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/1 "2024-07-29T18:27:41Z")
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): ```ada 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; ``` ```ada 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: ```sh 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? ---
**Author:** ![Irvise](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/i/7ba0ec/32.png) [@Irvise](https://forum.ada-lang.io/u/Irvise)\ **Post date:** [August 10, 2024, 11:37am UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/2 "2024-08-10T11:37:58Z")
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 ---
**Author:** ![mgrojo](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/mgrojo/32/15_2.png) [@mgrojo](https://forum.ada-lang.io/u/mgrojo)\ **Post date:** [August 10, 2024, 5:59pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/3 "2024-08-10T17:59:32Z")
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. ---
**Author:** ![mgrojo](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/mgrojo/32/15_2.png) [@mgrojo](https://forum.ada-lang.io/u/mgrojo)\ **Post date:** [August 10, 2024, 7:54pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/4 "2024-08-10T19:54:58Z")
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?](https://forum.ada-lang.io/t/how-does-gnatprove-flow-debug-use-graphviz/1067/1) ---
**Author:** ![Irvise](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/i/7ba0ec/32.png) [@Irvise](https://forum.ada-lang.io/u/Irvise)\ **Post date:** [August 11, 2024, 8:38am UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/5 "2024-08-11T08:38:32Z")
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](https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_view_gnatprove_output.html#understanding-counterexamples) `--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](https://docs.adacore.com/spark2014-docs/html/ug/en/source/loop.html) for more info on how to properly deal with loops in SPARK. Best regards, Fer ---
**Author:** ![mgrojo](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/mgrojo/32/15_2.png) [@mgrojo](https://forum.ada-lang.io/u/mgrojo)\ **Post date:** [August 11, 2024, 11:40am UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/6 "2024-08-11T11:40:04Z")
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 🙂 ---
**Author:** ![evanescente-ondine](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/evanescente-ondine/32/451_2.png) [@evanescente-ondine](https://forum.ada-lang.io/u/evanescente-ondine)\ **Post date:** [December 11, 2024, 12:52am UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/7 "2024-12-11T00:52:11Z")
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 ? ```ada 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 ---
**Author:** ![mgrojo](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/mgrojo/32/15_2.png) [@mgrojo](https://forum.ada-lang.io/u/mgrojo)\ **Post date:** [December 11, 2024, 10:20pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/8 "2024-12-11T22:20:56Z")
What happens if you use this? `with Refined_Global => (Output => Memory, null => Count, Free_List, Free)` ---
**Author:** ![ksson](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/ksson/32/1082_2.png) [@ksson](https://forum.ada-lang.io/u/ksson)\ **Post date:** [December 12, 2024, 12:02am UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/9 "2024-12-12T00:02:23Z")
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. ---
**Author:** ![evanescente-ondine](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/evanescente-ondine/32/451_2.png) [@evanescente-ondine](https://forum.ada-lang.io/u/evanescente-ondine)\ **Post date:** [December 12, 2024, 1:01am UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/10 "2024-12-12T01:01:49Z")
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.** ---
**Author:** ![ksson](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/ksson/32/1082_2.png) [@ksson](https://forum.ada-lang.io/u/ksson)\ **Post date:** [December 12, 2024, 8:13am UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/11 "2024-12-12T08:13:57Z")
I haven’t tried, but I think it should work if you declare `Internal_List` to be an `In_Out` of `Update`, and not an `Output`, which is closer to reality. ---
**Author:** ![Danieldy0](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/danieldy0/32/561_2.png) [@Danieldy0](https://forum.ada-lang.io/u/Danieldy0)\ **Post date:** [December 12, 2024, 6:02pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/12 "2024-12-12T18:02:45Z")
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 ---
**Author:** ![simonjwright](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/simonjwright/32/11_2.png) [@simonjwright](https://forum.ada-lang.io/u/simonjwright)\ **Post date:** [December 12, 2024, 7:47pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/13 "2024-12-12T19:47:57Z")
Go [here](https://ada-lang.io); the _Learn_ tab discusses getting started. ---
**Author:** ![OneWingedShark](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/onewingedshark/32/305_2.png) [@OneWingedShark](https://forum.ada-lang.io/u/OneWingedShark)\ **Post date:** [December 12, 2024, 9:24pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/14 "2024-12-12T21:24:52Z")
Additionally, there’s 1. [GetAdaNow.com](https://www.getadanow.com/) 2. [Alire](https://alire.ada.dev/docs/) ---
**Author:** ![jere](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/jere/32/87_2.png) [@jere](https://forum.ada-lang.io/u/jere)\ **Post date:** [December 12, 2024, 9:59pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/15 "2024-12-12T21:59:18Z")
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/](https://www.getada.dev/) Here’s one of the user’s release announcments: [Getada Has Been Released](https://forum.ada-lang.io/t/getada-has-been-released/769) It’s a wrapper around the installation of Alire for clarification ---
**Author:** ![simonjwright](https://forum.ada-lang.io/user_avatar/forum.ada-lang.io/simonjwright/32/11_2.png) [@simonjwright](https://forum.ada-lang.io/u/simonjwright)\ **Post date:** [December 12, 2024, 10:23pm UTC](https://forum.ada-lang.io/t/learning-about-spark-dependency-contracts/1033/16 "2024-12-12T22:23:49Z")
The _Learn_ tab at [ada-lang.io](http://ada-lang.io) discusses how to use Alire to get started with Ada.