Re: grassroots level SPARK Initiation

[Bojan Bozovic <bozovic.bojan@gmail.com>]

On Friday, March 23, 2018 at 3:05:25 PM UTC+1, Mehdi Saada wrote:
> Hi.
> 
> I couldn't find an initiation to verified programming using SPARK (aspects syntax) intended at beginners. I'm just trying to learn doing things right, that is, proving as much things I can, starting with the most basic things.
> If I want to learn that once I'm already working on (relatively) large codes, I'm sure it will be so much harder.
> 
> What do you think of it ? Is it too early ? Is there a thing such as "too early" ? Is there such a tuto somewhere ?

https://docs.adacore.com/spark2014-docs/html/ug/

There is also SPARK book

https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107040736

By McCormick and Chapin.

There's no too early as I've started not by using SPARK but by starting to learn predicate calculus from David Gries - The Science of Programming. And as far as I can tell, Ada isn't as much present in universities as it were during "Ada Mandate" by USA DoD. If you're learning it in an university, consider yourself lucky.