I wanted to try out some of the formal containers for SPARK, but I am having trouble finding the Sparklib mentioned in the Spark docs. My GNAT Studio doesn’t have a SPARK category under Help, as the SPARK manual mentions, and I usually do everything with ALR. I do see the SPARK Lemma libraries in my ALR cache of Gnatprove, but not the other libraries.

3 posts - 3 participants

Read full topic

It was nice to get an easy one after the past two days. The only hard thing was that gnatprove was either hanging or crashing, and I guessed that it didn’t like all the nested-nested-nested loops. I rewrote it so I generated an array of all coordinates and looped through that instead of the nested loops and I was able to get gnatprove to finish.

In case anyone needs help with part B:

8 posts - 4 participants

Read full topic