Re: grassroots level SPARK Initiation

[Paul Rubin <no.email@nospam.invalid>]

Mehdi Saada <00120260a@gmail.com> writes:
> I saw there was a thing called "propositional" calculus:

https://en.wikipedia.org/wiki/Propositional_calculus

Meh, the above article probably won't help that much, but it can give an
idea.

> is it covered by Gries book ?

Gries has written many books: which one do you mean?  His most famous
one was from the early 1970s and is about compilers.  It was important
in its time but these days you are better off with newer books.

> Were you a patented programmer before reading it ?

If you mean professional programmer, I learned about propositional
calculus in math class before going into programming.

If you're trying to prove stuff with SPARK you will also need to
understand predicate calculus and probably some proof theory.  Predicate
calculus is like propositional calculus except it also includes
statements that apply to all of the members of some type, rather than
just specific members.  The article

  https://en.wikipedia.org/wiki/First-order_logic

is very good.  You might want to read a general book on logic.  Herbert
Enderton's "A Mathematical Introduction to Logic" is still popular, I
think.  I liked it.  Its approach isn't ideal for computer science but
it's a start.  I don't know what to suggest instead.  Maybe someone else
here does.

This looks interesting: http://www.logicmatters.net/tyl/