FYI -- Lunar lander project relies on SPARK programming language
in [ADA]
|
Prev: Generic package with dynamic subprogram name?
Next: What is the best way to convert Integer to Short_Short_Integer?
From: melampus on 10 Jun 2010 08:16 Altran Praxis announced that its SPARK language has been selected by a new, NASA-funded US lunar mission. SPARK will be used to develop the software behind a CubeSat project being developed by a consortium comprising Vermont Technical College, Norwich University, St. Michael's College, and the University of Vermont. EE Times EU => http://www.electronics-eetimes.com/en/lunar-lander-project-relies-on-spark-programming-language.html?cmp_id=7&news_id=222902326&vID=296
From: Yannick Duchêne (Hibou57) on 10 Jun 2010 08:52 Le Thu, 10 Jun 2010 14:16:51 +0200, melampus <henssel(a)gmail.com> a écrit: > Altran Praxis announced that its SPARK language has been selected by a > new, NASA-funded US lunar mission. SPARK will be used to develop the > software behind a CubeSat project being developed by a consortium > comprising Vermont Technical College, Norwich University, St. > Michael's College, and the University of Vermont. > > EE Times EU => > http://www.electronics-eetimes.com/en/lunar-lander-project-relies-on-spark-programming-language.html?cmp_id=7&news_id=222902326&vID=296 Just a note: if it is SPARK, this is Ada too ;) Applause for both -- There is even better than a pragma Assert: a SPARK --# check. --# check C and WhoKnowWhat and YouKnowWho; --# assert Ada; -- i.e. forget about previous premises which leads to conclusion -- and start with new conclusion as premise.
From: Pascal Obry on 10 Jun 2010 12:19 Le 10/06/2010 14:52, Yannick Duch�ne (Hibou57) a �crit : > Just a note: if it is SPARK, this is Ada too ;) Right, would be nice to know which Ada compiler will be used to generate the code for the target. Pascal. -- --|------------------------------------------------------ --| Pascal Obry Team-Ada Member --| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE --|------------------------------------------------------ --| http://www.obry.net - http://v2p.fr.eu.org --| "The best way to travel is by means of imagination" --| --| gpg --keyserver keys.gnupg.net --recv-key F949BD3B
From: Niklas Holsti on 10 Jun 2010 14:01 Pascal Obry wrote: > Le 10/06/2010 14:52, Yannick Duch�ne (Hibou57) a �crit : >> Just a note: if it is SPARK, this is Ada too ;) > > Right, would be nice to know which Ada compiler will be used to generate > the code for the target. An earlier article on CubeSat (Ada User Journal, September 2008, page 213) says that they use(d) SofCheck's AdaMagic Ada-to-C compiler, followed by Rowley Associates' CrossWorks C compiler. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .
From: Peter C. Chapin on 11 Jun 2010 10:22
Niklas Holsti wrote: >> Right, would be nice to know which Ada compiler will be used to generate >> the code for the target. > > An earlier article on CubeSat (Ada User Journal, September 2008, page > 213) says that they use(d) SofCheck's AdaMagic Ada-to-C compiler, > followed by Rowley Associates' CrossWorks C compiler. I can speak to this issue as I am directly involved with this project. And yes, our intention is to compile the Ada to C using SofCheck's AdaMagic and then compile the C with CrossWorks. We have experience doing this with an earlier project and it works well. At the moment we are programming to the bare metal without the assistance of an operating system (although that might have to change at some point). SPARK is helpful here because the runtime support required for SPARK programs is extremely minimal due to SPARK's restrictions. Peter |