grassroots level SPARK Initiation

grassroots level SPARK Initiation

[Mehdi Saada]

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 ?

Re: grassroots level SPARK Initiation

[Mehdi Saada]

I could see there ARE students learning SPARK out there, thus Ada too, but I'm surprised to find none of them here.

Re: grassroots level SPARK Initiation

[Bojan Bozovic]

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.

Re: grassroots level SPARK Initiation

[Shark8]

On Friday, March 23, 2018 at 8:05:25 AM UTC-6, Mehdi Saada wrote:
> 
> What do you think of it? Is it too early? Is there a thing such as "too early"?

I think you're on the right track; I don't know if there is a "too early", though it seems to me you should have a grasp on (a) programming and (b) Ada syntax before delving into it. (B is honestly not that hard, most C/C++ programmers complain about the verbosity rather than comprehensibility or how easy/hard it is to remember the syntactic constructs.)

Re: grassroots level SPARK Initiation

[Mehdi Saada]

The problem is, I have untold difficulties with algorithms. Even-though I may understand easily how they operate in natural language (say, binary search through a sorted container), I have great troubles actually coding it. I cannot have in mind the whole thing once I wrote 25+ lines, which is, hum, unfortunate. Then I'm "forced" to tweak things here and there, until it works.
I know I shouldn't debug like this, and I hate it too. I especially hate not knowing what I do.

I'm self-taught.
You see, I have way much more perseverance than talentedness. Probaly a tad less naturally talented than your average student. Hence I would like to have the logical structure of I write/would like to write buried in my mind before touching the keyboard. To think the least possible.
That's why finding good, step-by-step materials is vital to me...

I saw there was a thing called "propositional" calculus: is it covered by Gries book ? Were you a patented programmer before reading it ? I read the prerequisite is "one year of experience", but I'm not sure what it entails. One year of being able to actually code for living ? If so I may not be at here yet. Otherwise, of course I know the basics and purpose of programming and computer architecture, but I doubt it's enough..
To start I'll go train logical/formal reasoning in math books. Or find old books on this on the web.
If you have suggestions, feel free...

Re: grassroots level SPARK Initiation

[Mehdi Saada]

My problem is untold difficulty with algorithms. Even-though I may understand easily how they operate in natural language (say, binary search through a sorted container), I cannot code it: more than 25+ lines (of myself), and I don't understand it anymore. Then I'm "forced" to tweak things here and there, until it works. I know I shouldn't debug like this, and I hate it too. especially not knowing what I do.

I'm self-taught.
You see, I have way much more perseverance than talentedness. Probaly a tad less naturally talented than your average student. Hence I would like to have the logical structure of I write/would like to write buried in my mind before touching the keyboard. To make things as mechanical as possible, for the moment at least.
I saw there was a thing called "propositional" calculus: is it covered by Gries book ? Were you a patented programmer before reading it ? I read the prerequisite is "one year of experience", but I'm not sure what it entails. One year of being able to actually code for living ?
Well, I found it free on the web, I'll see for myself. And start train math and logical reasoning elsewhere too.

Re: grassroots level SPARK Initiation

[Niklas Holsti]

On 18-04-25 18:25 , Mehdi Saada wrote:
> My problem is untold difficulty with algorithms. Even-though I may
> understand easily how they operate in natural language (say, binary
> search through a sorted container), I cannot code it: more than 25+
> lines (of myself), and I don't understand it anymore. Then I'm
> "forced" to tweak things here and there, until it works. I know I
> shouldn't debug like this, and I hate it too. especially not knowing
> what I do.

I find it helps me to describe in prose (in comments) exactly what every 
variable, parameter, subprogram, loop, etc. is intended to do and 
represent, including all the special cases (empty array, value not 
found, etc.). Then you don't need to hold it all in your mind, but can 
refer to the written descriptions as often as needed.

And the bonus is that the descriptions remain available for anyone 
looking at or modifying the program, including a future version of 
yourself...

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: grassroots level SPARK Initiation

[Paul Rubin]

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/

Re: grassroots level SPARK Initiation

[Mehdi Saada]

I am trying both Gries' Science of Programming and Enderton's introduction to logic. As much as I enjoy the first (except the second chapter on "natural" reasoning/proof system, which I skipped as it is completely unreadable for the moment)) I quickly hated the second as, as has been said, it's QUITE not the right orientation, indeed.
It casts everything in nonsensical mumbo-jumbo (to be polite ;-) ) whereas a down-to-earth - and finitist - approach would use primarily basic field agebra, multisets and operations on them to model logical reasoning.

Re: grassroots level SPARK Initiation

[Paul Rubin]

Mehdi Saada <00120260a@gmail.com> writes:
> I am trying both Gries' Science of Programming and Enderton's
> introduction to logic.... I quickly hated the second as, as has been
> said, it's QUITE not the right orientation, indeed.  It casts
> everything in nonsensical mumbo-jumbo (to be polite ;-) ) whereas a
> down-to-earth - and finitist - approach would use primarily basic
> field agebra, multisets and operations on them to model logical
> reasoning.

Most math is fundamentally about reasoning about infinite sets, such the
integers.  The area within math that deals with finite sets is called
combinatorics and it is hard.  SPARK almost certainly deals with
infinite models.  You might want to prove that a function never crashes
for any sequence of inputs, so you have to quantity over all possible
sequences, of which there are infinitely many.

Finiteness actually makes things harder.  Like if you write a program
that does some calculations with integers, you can prove the algorithm's
correctness using the rules of arithmetic (commutative law, induction,
bla bla bla).  E.g. maybe the algorithm computes some number N and then
does something with its successor N+1.  In math that is fine, every
number has a successor, but that's because the integers are an infinite
set.  If you want to stay with finite sets, you can't say "ok I have N
so I'll compute N+1 and use it for whatever".  You have to *also* prove
that N is small enough that computing N+1 won't result in arithmetic
overflow.

I guess I can sympathize if you didn't like Enderton's book.  I liked it
but I agree that it used a lot of weird symbols whose meanings took
getting used to, etc.  Plus, it's possibly too oriented towards abstract
math and maybe even philosophy.  It's been a long time since I used it
so maybe I'm forgetting.  I typed "logic for computer science" into web
search and found tons of plausible looking books.  Maybe you could try
one of those.

Wikipedia has an article on natural deduction, though I don't know how
it compares with whatever you looked at:

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

See if you like this better than Enderton's book (it is less mathematical):

https://www.fecundity.com/codex/forallx.pdf
Info page: https://www.fecundity.com/logic/

Re: grassroots level SPARK Initiation

[Mehdi Saada]

> Most math is fundamentally about reasoning about infinite sets. 
Except men have been doing math way before last century's mania with set theory. The computer is *never* counting up to the infinite, of course... It's not *reasoning* about infinite stuff either, it's always applying a logical, step-by-step recipe, however complex. Many things *can* be cast in different formalism, be it better or not. The same happen within math... some problem are more naturally, whatever the term means, cast in some language than other. Or some properties/structures made more apparent. For more on all of that, see NJ.Wildberger, math teacher on YT ... Just be sure this stance isn't coming from nowhere, nor is devoid of reason.

> https://www.fecundity.com/codex/forallx.pdf
I'll look at it. Do you know "HOW TO PROVE IT, A Structured Approach", from Daniel J. Velleman ? It's lengthier, among other things. But like you said, many good books here.

Re: grassroots level SPARK Initiation

[Paul Rubin]

Mehdi Saada <00120260a@gmail.com> writes:
>> Most math is fundamentally about reasoning about infinite sets. 
> Except men have been doing math way before last century's mania with
> set theory.

Yes, usually with the integers (of which there are infinitely many) or
else with geometry (lines, planes, or space of infinite size).  Set
theory itself is much more recent of course.  I don't think it's really
come up in this discussion except in saying math is about infinite sets,
but if you prefer, we could say infinite structures (again the classic
example is the integers).

> The computer is *never* counting up to the infinite, of
> course... It's not *reasoning* about infinite stuff either, it's
> always applying a logical, step-by-step recipe, however complex.

We're talking about SPARK whose purpose is to prove theorems about
programs (that they don't crash, etc).  Yes, proving theorems is reasoning.

> see NJ.Wildberger, math teacher on YT ... Just be sure this stance
> isn't coming from nowhere, nor is devoid of reason.

OK, I looked at a couple minutes of video and some of the articles on
his web site, and he seems to be espousing some views in the philosophy
of mathematics connected with an idea called finitism.  That's a little
bit off the beaten path, but some good mathematicians such as Edward
Nelson have worked in that area.  But if you look at

  http://web.maths.unsw.edu.au/~norman/papers/Ordinals.pdf

it's very clear that Wildberger understands the conventional approach
perfectly well, so you should learn it too.  Also I think he objects to
completed infinities (like the ones in set theory) but seems ok with
potential infinities (like the integers under the first-order arithmetic
axioms).  Not allowing completed infinities means we can't collect the
integers into a single object, but there is still no largest integer,
and we can quantify over the integers to say "every integer has a
successor" and things like that.

Anyway Enderton's book on logic might mention set theory in a place or
two, but it's not really an important part iirc.  (He has a separate
book on set theory which you might not went to read).  You won't
encounter set theory much in computer science.  In fact the logic used
in software proofs is usually intuitionistic logic (aka constructive
logic).  Not that there's anything wrong with classical logic, but
intuitionistic logic happens to work better for the results you want.

> I'll look at it. Do you know "HOW TO PROVE IT, A Structured Approach",
> from Daniel J. Velleman ? It's lengthier, among other things.

It looks like a nice book about doing math proofs, so you should
certaintly study it if the stuff in it isn't familiar to you.  But it's
not a logic book.  It might be reasonable to put logic aside temporarily
and read Velleman's book first.