ADA

SPARK and testing. Was: Lost in translation (with SPARK user rules)
Pascal Obry wrote: Just curious, why do you feel that you still need to write tests after having run successfully the SPARK proof checker? Despite the proofs testing is still essential. At least that is my view. Here is why: 1. The proofs show that the subprograms obey the annotations that I provide. Ho... 28 May 2010 08:13

Sockets package in SPARK
Yannick Duch�ne wrote: Le Thu, 27 May 2010 20:41:22 +0200, Pascal Obry <pascal(a)obry.net> a �crit: Is that binding available for download? (Or is it an internal product?) Internal sorry. Jacob, if you have some needs in this area, feel free to ask me (could negotiate via e-mail if you wi... 28 May 2010 03:55

Spark, pragma
Hi, I am having trouble with Spark and pragma. If I am not wrong, Spark accepts all pragmas and generate warning when we run the examiner. In order than the examiner succeeds, we can tell in the warning control file that we want to accept some or all pragma, with "pragma all". Basically, I added a pragma Style_Che... 28 May 2010 09:18

Ada compilers written in ... (was: Re: Ada noob here! Is Ada widely used?)
In article <4bfe71ba$0$7661$9b4e6d93(a)newsspool1.arcor-online.net>, Georg Bauhaus <rm.dash-bauhaus(a)futureapps.de> wrote: Another finding is a validated Ada compiler for BS2000 by Siemens, as reported in Computerwoche 1987-07-03: (Translation, ad hoc) "The compiler, made of modules, is written in ... 28 May 2010 01:46

SPARK again : for-loop vs single loop - a strange case
Hi all, This will require some further investigation on my own side, however, I would like to open a topic about it, if ever someone wants to share about the same matter. I was proving something built around a for-loop. Every thing was going, when I've meet a trouble and decided to switch to a classic lo... 28 May 2010 19:15

Sockets package in SPARK (Was: Lost in translation (with SPARKuser rules))
Jacob, Is that binding available for download? (Or is it an internal product?) Internal sorry. -- --|------------------------------------------------------ --| Pascal Obry Team-Ada Member --| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE --|--------------------------... 27 May 2010 15:55

Ada compilers written in ... (was: Re: Ada noob here! Is Ada widelyused?)
On 25.05.10 13:41, Anonymous wrote: BTW, do you know what language Ada is written in? I'd guess C and asm. If you do some research you can find an incredible web site discussing the Ada competition in some depth. And here on this very list we have some of the people who participated in that competition... 27 May 2010 10:20

Sockets package in SPARK (Was: Lost in translation (with SPARK user rules))
Pascal Obry wrote: I had to create a binding to the OS sockets in SPARK, I can tell you that it was not easy... Is that binding available for download? (Or is it an internal product?) Greetings, Jacob -- Those who can't laugh at themselves leave the job to others. ... 27 May 2010 07:03

Ada requires too much typing!
This is just an observation on the difference between two communities. I've been recently using Scala for a project (I'd rather use Ada, but it's hard for me to justify the cost of converting... alas). Scala is a functional/OO hybrid language that targets the JVM. It prides itself on, among other things, its conc... 28 Jun 2010 22:44

Lost in translation (with SPARK user rules)
Lost in translation... do you know the movie ? No, I'm joking, this is not about this 2002 movie, that's about SPARK, and exactly, about translating some expressions in the rules language. Previously, I have successfully added these rules, in an *.RLU file: inequals(122): X/Y<1 may_be_deduced_from ... 2 Jun 2010 23:06