Aida.Bounded_String?

[bracke]

Hi

In the readme you mention the package "Aida.Bounded_String" but it seems to be missing in the source?

Kind regards
Bent Bracke

[joakim-strandberg]

Hi Bent,

The bounded string implementation was moved into the Aida package. Just look for "type Bounded_String" in aida.ads and you will find it. I will update the readme file thanks.

Best regards,
Joakim

[bracke]

Hi Joakim

Thanks for the swift response.

I was looking at your XCB thin binding. It seems to use Aida.Bounded_String.
Is it because it uses an old version of Aida?

kind regards
Bent Bracke

[joakim-strandberg]

Hi Bent,

Yes, it uses an old version of Aida (the original before it was turned into SPARK if memory serves me right). What I think of most when I think of the XCB repository is the xproto_parsing directory where there is a pure Ada 95 application that parses the xml file to generate the Ada binding. It uses the Ada 95 version of a memory pool to ensure memory safety. When I started the Aida library I was thinking of making a cross-compiler library and therefore didn't want to use the standard types Integer, Float and so on, and instead define cross-compiler basic types to use (Int32 or Int32_T and so on....). That idea didn't turn out to be fruitful because the pioneering work of AdaCore on SPARK will probably be GNAT compiler specific code for several years to come. And that's the latest change I did to the Aida library: Replacing Int32 -> Integer. Also removing the suffix _T from many type definitions.

The only regret I have when it comes to the Aida library is that I didn't manage to get SPARK to prove all verification conditions in the Aida.UTF8 package. To do it, at least in the current version of SPARK, one need to put a pragma Assume statement in order to prove all verification conditions. However, I've tried my best to avoid pragma Assume statements because if one assumes a false statement one can then derive anything, which defeats the purpose of using SPARK. In that particular pragma Assume the statement is true which I've verified by enabling gnat assertions and also written an application to verify it, but putting in a pragma Assume and then writing some comment about it does introduce uncertainty, at least in me, imagine one has a SPARK application with thousands of pragma Assume statements, how can one be sure the application is correct? In any case, the code is put on github here so that it may be reused or source for inspiration.

Best regards,
Joakim