GNAT packages in Linux distributions
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 27 May 2010 08:29 Le Thu, 27 May 2010 14:41:58 +0200, <stefan-lucks(a)see-the.signature> a écrit: > Because students appreciate coherent concepts. > > More specifically: There is a syntactic gap between SPARK and Ada. I had > given a course on Ada and SPARK recently, and my students seem to be > permanently tempted to focus on the Ada-part, while contracts and proofs > where considered a more "optional" add-on, rather than a necessary and > integral part of their work. I see, and I believe this question is close to a kind of ergonomic matter (there is something like ergonomy in languages too). -- 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: (see below) on 27 May 2010 11:21 On 27/05/2010 13:41, in article Pine.LNX.4.64.1005271422490.30605(a)medsec1.medien.uni-weimar.de, "stefan-lucks(a)see-the.signature" <stefan-lucks(a)see-the.signature> wrote: > On Wed, 26 May 2010, (see below) wrote: > >> On 26/05/2010 14:02, in article >> Pine.LNX.4.64.1005261455260.26620(a)medsec1.medien.uni-weimar.de, >> "stefan-lucks(a)see-the.signature" <stefan-lucks(a)see-the.signature> wrote: >> >>> I am a university teacher. For me, it makes quite a difference if I either >>> explain students one coherent language where contracts are an integral part >>> of (like Eiffel), or one programming language plus an additional language >>> for the annotations. >>> >> >> Why? > > Because students appreciate coherent concepts. But concepts /= language notations. > More specifically: There is a syntactic gap between SPARK and Ada. I had > given a course on Ada and SPARK recently, and my students seem to be > permanently tempted to focus on the Ada-part, while contracts and proofs > where considered a more "optional" add-on, rather than a necessary and > integral part of their work. Is that an inaccurate perception? SPARK contracts and proofs ARE add-ons. My experience is that CS/SE students always focus on "coding" at the expense of problem analysis, program design, project planning, verification, validation, documentation, and anything else they find less congenial. I doubt that the SPARK notation has much to do with that. > > Beware: My students are some of the people who will > write the software you will use tomorrow. ;-) Since they are learning SPARK/Ada I am less worried by that than I might otherwise have been. 8-) Beware: My ex-students are some of the people who wrote the software you are using today. ;-) -- Bill Findlay <surname><forename> chez blueyonder.co.uk
From: Yannick Duchêne (Hibou57) on 2 Jun 2010 23:16 Le Thu, 27 May 2010 17:21:57 +0200, (see below) <yaldnif.w(a)blueyonder.co.uk> a écrit: > My experience is that CS/SE students always focus on "coding" at the > expense > of problem analysis, program design, project planning, verification, > validation, documentation, and anything else they find less congenial. I always though this was not so much with these students. So why do they choose it if they are not aware of what it requires ? > Beware: My ex-students are some of the people who > wrote the software you are using today. ;-) > You're teacher too like Stefan ? -- 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: Brian Drummond on 3 Jun 2010 06:42 On Thu, 03 Jun 2010 05:16:14 +0200, Yannick Duch�ne (Hibou57) <yannick_duchene(a)yahoo.fr> wrote: >Le Thu, 27 May 2010 17:21:57 +0200, (see below) ><yaldnif.w(a)blueyonder.co.uk> a �crit: >> My experience is that CS/SE students always focus on "coding" at the >> expense >> of problem analysis, program design, project planning, verification, >> validation, documentation, and anything else they find less congenial. >I always though this was not so much with these students. So why do they >choose it if they are not aware of what it requires ? > >> Beware: My ex-students are some of the people who >> wrote the software you are using today. ;-) >> >You're teacher too like Stefan ? If you learned Pascal, there's a pretty good chance you learned it from his book... http://www.amazon.co.uk/PASCAL-Introduction-Methodical-Programming-Instructions/dp/0273021885/ref=sr_1_1?ie=UTF8&s=books&qid=1275561327&sr=1-1 - Brian
From: (see below) on 3 Jun 2010 09:49
On 03/06/2010 04:16, in article op.vdpfdcgoxmjfy8(a)garhos, "Yannick Duch�ne (Hibou57)" <yannick_duchene(a)yahoo.fr> wrote: > Le Thu, 27 May 2010 17:21:57 +0200, (see below) > <yaldnif.w(a)blueyonder.co.uk> a �crit: >> My experience is that CS/SE students always focus on "coding" at the >> expense >> of problem analysis, program design, project planning, verification, >> validation, documentation, and anything else they find less congenial. > I always though this was not so much with these students. So why do they > choose it if they are not aware of what it requires ? They are aware. That makes no difference. >> Beware: My ex-students are some of the people who >> wrote the software you are using today. ;-) >> > You're teacher too like Stefan ? Was. Now I'm a free man. 8-) -- Bill Findlay <surname><forename> chez blueyonder.co.uk |