GNAT packages in Linux distributions
in [ADA]
|
From: Yannick Duchêne (Hibou57) on 26 May 2010 08:22 Le Wed, 26 May 2010 15:02:50 +0200, <stefan-lucks(a)see-the.signature> a écrit: > Annotations are an addition to the original language. Annotations are > typically "hidden" in comments (from the viewpoint of the original > language). This is in constrast to contracts defined as a part of the > language itself. (Technically, the language with the annotations makes a > new language ... but there is a gap between the normal part of the > language, and the comment-like annotations. This is just notation, no one can infer anything from such a premise. > I am a university teacher. For me, it makes quite a difference if I > either > explain studens one coherent language where contracts are an integral > part > of (like Eiffel), or one programming langugage plus an additional > language > for the annotations. For perception, this matter, I agree. -- There is even better than a pragma Assert: a SPARK --# check.
From: (see below) on 26 May 2010 09:06 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 studens one coherent language where contracts are an integral part > of (like Eiffel), or one programming langugage plus an additional language > for the annotations. > Why? -- Bill Findlay <surname><forename> chez blueyonder.co.uk
From: stefan-lucks on 27 May 2010 08:41 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. 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. Beware: My students are some of the people who will write the software you will use tomorrow. ;-) -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------
From: stefan-lucks on 27 May 2010 08:47 On Wed, 26 May 2010, Yannick Duch�ne (Hibou57) wrote: > Le Wed, 26 May 2010 15:02:50 +0200, <stefan-lucks(a)see-the.signature> a �crit: > >Annotations are an addition to the original language. Annotations are > >typically "hidden" in comments (from the viewpoint of the original > >language). This is in constrast to contracts defined as a part of the > >language itself. (Technically, the language with the annotations makes a > >new language ... but there is a gap between the normal part of the > >language, and the comment-like annotations. > This is just notation, no one can infer anything from such a premise. Notation is not such unimportant. And this is a bit more than just notation: You use different *tools* to compile the program-while-ignoring-all-annotations and to check the additional information provided by the annotations. This means, that psychologically the information in the annotations appears to be the "less important" stuff. E.g., a badly flawed SPARK program may still be compiled by an Ada compiler, but a syntactically incorrect Ada-program will be found flawed by the SPARK tools. > [...] For perception, this matter, I agree. See! -- ------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------ Stefan dot Lucks at uni minus weimar dot de ------ I love the taste of Cryptanalysis in the morning! ------
From: Yannick Duchêne (Hibou57) on 27 May 2010 08:26
Le Thu, 27 May 2010 14:47:15 +0200, <stefan-lucks(a)see-the.signature> a écrit: > Notation is not such unimportant. > > And this is a bit more than just notation: You use different *tools* to > compile the program-while-ignoring-all-annotations and to check the > additional information provided by the annotations. This means, that > psychologically the information in the annotations appears to be the > "less > important" stuff. Do not make this a rule, as this depends on one's expectations (so receptivity to that what looks like his/her expectations). One who wish and expect what belongs to these annotations, will see these as important things. One who does not expect these annotations and may perhaps even wish that would not exist (like a student working on an assignment) will see these as non so much important. This is a matter of receptivity. I was a bit wrong (did a shortcut) when I suggested âthis is just annotationâ, as I agree the form of an annotation is important for readability. > E.g., a badly flawed SPARK program may still be compiled > by an Ada compiler, Yes > but a syntactically incorrect Ada-program will be > found flawed by the SPARK tools. Not a rule, as not all notations oriented language may check every thing of the host language. SPARK does, but I'm pretty sure not all do (I think we were talking about the general case here, not only about the SPARK special case). -- 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. |