* grassroots level SPARK Initiation @ 2018-03-23 14:05 Mehdi Saada 2018-03-23 14:16 ` Mehdi Saada ` (3 more replies) 0 siblings, 4 replies; 12+ messages in thread From: Mehdi Saada @ 2018-03-23 14:05 UTC (permalink / raw) 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 ? ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-03-23 14:05 grassroots level SPARK Initiation Mehdi Saada @ 2018-03-23 14:16 ` Mehdi Saada 2018-03-23 14:24 ` Bojan Bozovic ` (2 subsequent siblings) 3 siblings, 0 replies; 12+ messages in thread From: Mehdi Saada @ 2018-03-23 14:16 UTC (permalink / raw) I could see there ARE students learning SPARK out there, thus Ada too, but I'm surprised to find none of them here. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-03-23 14:05 grassroots level SPARK Initiation Mehdi Saada 2018-03-23 14:16 ` Mehdi Saada @ 2018-03-23 14:24 ` Bojan Bozovic 2018-03-23 16:33 ` Shark8 2018-05-24 18:55 ` Mehdi Saada 3 siblings, 0 replies; 12+ messages in thread From: Bojan Bozovic @ 2018-03-23 14:24 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-03-23 14:05 grassroots level SPARK Initiation Mehdi Saada 2018-03-23 14:16 ` Mehdi Saada 2018-03-23 14:24 ` Bojan Bozovic @ 2018-03-23 16:33 ` Shark8 2018-04-25 15:02 ` Mehdi Saada 2018-05-24 18:55 ` Mehdi Saada 3 siblings, 1 reply; 12+ messages in thread From: Shark8 @ 2018-03-23 16:33 UTC (permalink / raw) 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.) ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-03-23 16:33 ` Shark8 @ 2018-04-25 15:02 ` Mehdi Saada 2018-04-25 15:25 ` Mehdi Saada 2018-04-26 1:59 ` Paul Rubin 0 siblings, 2 replies; 12+ messages in thread From: Mehdi Saada @ 2018-04-25 15:02 UTC (permalink / raw) 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... ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-04-25 15:02 ` Mehdi Saada @ 2018-04-25 15:25 ` Mehdi Saada 2018-04-25 16:14 ` Niklas Holsti 2018-04-26 1:59 ` Paul Rubin 1 sibling, 1 reply; 12+ messages in thread From: Mehdi Saada @ 2018-04-25 15:25 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-04-25 15:25 ` Mehdi Saada @ 2018-04-25 16:14 ` Niklas Holsti 0 siblings, 0 replies; 12+ messages in thread From: Niklas Holsti @ 2018-04-25 16:14 UTC (permalink / raw) 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 . @ . ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-04-25 15:02 ` Mehdi Saada 2018-04-25 15:25 ` Mehdi Saada @ 2018-04-26 1:59 ` Paul Rubin 1 sibling, 0 replies; 12+ messages in thread From: Paul Rubin @ 2018-04-26 1:59 UTC (permalink / raw) 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/ ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-03-23 14:05 grassroots level SPARK Initiation Mehdi Saada ` (2 preceding siblings ...) 2018-03-23 16:33 ` Shark8 @ 2018-05-24 18:55 ` Mehdi Saada 2018-05-24 20:52 ` Paul Rubin 3 siblings, 1 reply; 12+ messages in thread From: Mehdi Saada @ 2018-05-24 18:55 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-05-24 18:55 ` Mehdi Saada @ 2018-05-24 20:52 ` Paul Rubin 2018-05-24 23:50 ` Mehdi Saada 0 siblings, 1 reply; 12+ messages in thread From: Paul Rubin @ 2018-05-24 20:52 UTC (permalink / raw) 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/ ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-05-24 20:52 ` Paul Rubin @ 2018-05-24 23:50 ` Mehdi Saada 2018-05-25 1:09 ` Paul Rubin 0 siblings, 1 reply; 12+ messages in thread From: Mehdi Saada @ 2018-05-24 23:50 UTC (permalink / raw) > 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. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: grassroots level SPARK Initiation 2018-05-24 23:50 ` Mehdi Saada @ 2018-05-25 1:09 ` Paul Rubin 0 siblings, 0 replies; 12+ messages in thread From: Paul Rubin @ 2018-05-25 1:09 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 12+ messages in thread
end of thread, other threads:[~2018-05-25 1:09 UTC | newest] Thread overview: 12+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-03-23 14:05 grassroots level SPARK Initiation Mehdi Saada 2018-03-23 14:16 ` Mehdi Saada 2018-03-23 14:24 ` Bojan Bozovic 2018-03-23 16:33 ` Shark8 2018-04-25 15:02 ` Mehdi Saada 2018-04-25 15:25 ` Mehdi Saada 2018-04-25 16:14 ` Niklas Holsti 2018-04-26 1:59 ` Paul Rubin 2018-05-24 18:55 ` Mehdi Saada 2018-05-24 20:52 ` Paul Rubin 2018-05-24 23:50 ` Mehdi Saada 2018-05-25 1:09 ` Paul Rubin
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox