ADA

Shared library project
Hello everybody! Can somebody what does this mean? The compiler outputs: "shared library project "X" cannot import project "Y" that is not a shared library project" used Windows hosted GNAT GPL and GPS 2009 and compiler, just downloaded. Thank you! ... 10 Jun 2010 16:46

SPARK : surprising failure with implication
Hi all, In an Ada/SPARK source, I had something like this: --# check (Source = 1) -> ((Source mod 2) = 1); -- (1) --# check (Source mod 2) /= 1; -- (2) --# check Source /= 1; -- (3) 1) Was proved by the simplifier (note that I needed a user rule for that)... 3 Jun 2010 13:23

ANN: VC_View 2.1.1 is Linux compatible
VC_View presents verification conditions, generated by the SPARK tools, in a way that makes them easier to interpret: 1. Only immediately relevant hypotheses are initially displayed. 2. User identifiers are replaced by upper-case letters. Version 2.1.1 of VC_View is now available and is compatible with both Wind... 8 Jun 2010 13:41

Two miscellaneous questions about GPS : Ada indentation andthen SPARK integration
On Tue, 01 Jun 2010 09:20:45 +0200 Yannick Duchêne (Hibou57) <yannick_duchene(a)yahoo.fr> wrote: I have an expected behavior with the editor : in the configuration, Edit -> Preferences -> Editor -> Ada, I have disabled the check box “Use tabulations”, to not have tab characters and just spaces. For ... 1 Jun 2010 05:23

Two miscellaneous questions about GPS : Ada indentation and thenSPARK integration
Hillo, I oftenly don't use GPS (I use a markup driven outlining editor instead), so I'm not a GPS guru. I have an expected behavior with the editor : in the configuration, Edit -> Preferences -> Editor -> Ada, I have disabled the check box “Use tabulations”, to not have tab characters and just spaces... 2 Jun 2010 05:27

Dynamically tagged expression not allowed. Why?
I'm creating a GNAT 4.4.3 on Ubuntu Ada binding for some C++ classes, using the binding generated by g++ -fdump-ada-spec as a starting point. While the binding will compile cleanly, the client code gets a compilation error, "dynamically tagged expression not allowed", when trying to set up the declarations to u... 5 Jun 2010 15:48

Child vs nested package : efficiency matter
Hillo, For some reasons, I've turned some nested package -- packages nested in the body of package -- into a set of child packages instead. I've noticed the application's execution time is now an average of 125% of that of the old implementation. The implementation did not changed otherwise and is stil... 1 Jun 2010 21:54

SPARK and modular types
Hello happy novellers, I have found some tips which shows to be useful when working with proofs on program involving modular types. 1) First of all, one you may have seen in a previous thread I've opened, is the use of Type'Pos. Many times, working with modular types, involves power of twos. The Ada's ... 29 May 2010 08:07

SPARK: What does it prove?
There has been a lot of discussion about SPARK on this group recently. That's great, but I hope those who are more interested in full Ada aren't getting annoyed! :) It is common to talk about SPARK proofs but of course what the Simplifier is actually proving are the verification conditions generated by the Examin... 31 May 2010 19:40

SPARK and testing.
Peter C. Chapin wrote: 4. I might get lazy or run out of time and not complete all the proofs. I can elaborate on this a little more. In my case the program I'm working on now needs to compute the minimum model of a collection of Datalog rules (Datalog is a simple logic language that has been discussed as a ... 28 May 2010 19:15