❌ About FreshRSS

Normal view

There are new articles available, click to refresh the page.
Before yesterdayAda Forum - Latest topics

SPARK Proof [title padded to meet minimum length requirement]

By: JC001
10 October 2023 at 10:38

In SparkRC I created some higher-level data structures on top of the Ada.Containers.Formal_* components, mainly to try to improve my understanding of how to get SPARK to prove things. Pkg spec prove.ads contains instantiations of these for various kinds of types to allow proofs. All of them prove completely, but as noted, the current predicates do not include proof of functional correctness. This is because proof of even very simple and obvious functional-correctness predicates fail for at least some of the types in prove.ads.

Consider, for example, the bounded-queue component. The Get operation is supposed to remove the head of the queue and put it in the Item parameter. This implies that the length of the queue will decrease and Item will contain the old head. Currently only the first part of that is being proved. Since the Peek function returns the head of a queue, I would like to add

Item = Peek (From)'Old

to the postcondition. In fact, doing so works with the instantiations for Integer and CA, but fails for CR. SPARK is unable to prove that part of the postcondition in that case. I am unable to see why or how to phrase this so that it can prove it.

Any insights?

3 posts - 2 participants

Read full topic

Qplt (Quick Plot)

By: JC001
2 June 2023 at 15:52

Seen on c.l.a:

I have created Qplt (Quick Plot), an Ada-GUI program to quickly produce a plot of a data set, and make it publicly available in hopes that it might prove useful. The program automatically selects axis ranges and tick intervals. The user may select whether points, lines, or both are plotted, and supply a title and axis labels.

Qplt is available at


10 posts - 4 participants

Read full topic