SPARK code samples
in [ADA]
|
Prev: Ada 2012: An Oops in the new Ada amendments ? (in 10.1.2 Context Clauses - With Clauses)
Next: Generic_Roots
From: Dmitry A. Kazakov on 11 Aug 2010 13:33 On Wed, 11 Aug 2010 17:26:05 +0200, Yannick Duch�ne (Hibou57) wrote: > Le Wed, 11 Aug 2010 10:44:58 +0200, Dmitry A. Kazakov > <mailbox(a)dmitry-kazakov.de> a �crit: >> http://rosettacode.org/wiki/Main_Page > I use to see reference to it from place to place. Just have a quick look a > few seconds ago. Is it on purpose if all examples seems to lack comments ? > I do not see any unsolved task for SPARK. I suppose it is because the site's maintenance script hasn't yet built the list. In fact no task is implemented. The list of all tasks is here: http://rosettacode.org/wiki/Category:Programming_Tasks (the first 200 (:-)) Pick any you wish. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Ada novice on 11 Aug 2010 13:39 On Aug 11, 7:32 pm, Mark Lorenzen <mark.loren...(a)gmail.com> wrote: > > I also think there is a risk of getting stuck with SPARK if you try to > design a SPARK program with Ada in mind. You constantly bump into a > useful feature of Ada that is not in SPARK (discriminated types, array > slicing etc.) and you think "why the h... isn't that a part of SPARK > when it's so easy to do in Ada?". So it's probably a way of tuning > your mindset from "Ada with restrictions" into SPARK. > So you're saying not to think in terms of Ada when approaching SPARK? I have yet to lay my hands on a copy of Barnes' SPARK book to learn SPARK syntax and I can understand that SPARK is not just Ada with some annotations. YC
From: (see below) on 11 Aug 2010 13:45 On 11/08/2010 18:39, in article bbc93c1c-9e12-4682-912d-9ff961c3a7a5(a)p7g2000yqa.googlegroups.com, "Ada novice" <ycalleecharan(a)gmx.com> wrote: > On Aug 11, 7:32�pm, Mark Lorenzen <mark.loren...(a)gmail.com> wrote: >> >> I also think there is a risk of getting stuck with SPARK if you try to >> design a SPARK program with Ada in mind. You constantly bump into a >> useful feature of Ada that is not in SPARK (discriminated types, array >> slicing etc.) and you think "why the h... isn't that a part of SPARK >> when it's so easy to do in Ada?". So it's probably a way of tuning >> your mindset from "Ada with restrictions" into SPARK. >> > > So you're saying not to think in terms of Ada when approaching SPARK? > I have yet to lay my hands on a copy of Barnes' SPARK book to learn > SPARK syntax and I can understand that SPARK is not just Ada with some > annotations. Yebbut. It is. -- Bill Findlay <surname><forename> chez blueyonder.co.uk
From: Ada novice on 11 Aug 2010 14:00 On Aug 11, 7:45 pm, "(see below)" <yaldni...(a)blueyonder.co.uk> wrote: > On 11/08/2010 18:39, in article > bbc93c1c-9e12-4682-912d-9ff961c3a...(a)p7g2000yqa.googlegroups.com, "Ada > > novice" <ycalleecha...(a)gmx.com> wrote: > > On Aug 11, 7:32 pm, Mark Lorenzen <mark.loren...(a)gmail.com> wrote: > > >> I also think there is a risk of getting stuck with SPARK if you try to > >> design a SPARK program with Ada in mind. You constantly bump into a > >> useful feature of Ada that is not in SPARK (discriminated types, array > >> slicing etc.) and you think "why the h... isn't that a part of SPARK > >> when it's so easy to do in Ada?". So it's probably a way of tuning > >> your mindset from "Ada with restrictions" into SPARK. > > > So you're saying not to think in terms of Ada when approaching SPARK? > > I have yet to lay my hands on a copy of Barnes' SPARK book to learn > > SPARK syntax and I can understand that SPARK is not just Ada with some > > annotations. > > Yebbut. It is. > > -- > Bill Findlay > <surname><forename> chez blueyonder.co.uk In this article: "The Exterminators---A small British firm shows that software bugs aren't inevitable" available at http://spectrum.ieee.org/computing/software/the-exterminators/0 it is mentioned, I quote: "that the two-step translation--from English to Z and from Z to Spark--lets engineers keep everything in mind" I haven't yet personally written any programs in SPARK but does one has necessarily to understand the Z language in order to use SPARK? I recall reading somewhere that Barnes's book doesn't discuss the Z language (I might be wrong though). Thanks YC
From: Yannick Duchêne (Hibou57) on 11 Aug 2010 14:17
Le Wed, 11 Aug 2010 20:00:53 +0200, Ada novice <ycalleecharan(a)gmx.com> a écrit: > I haven't yet personally written any programs in SPARK but does one > has necessarily to understand the Z language in order to use SPARK? I > recall reading somewhere that Barnes's book doesn't discuss the Z > language (I might be wrong though). It is not required (just that if I'm not wrong, SPARK itself was checked with Z). Z is one the language/method in this area (some are language, some others are language and methods), which are mainly : SPARK, Z, B, VDM, ACSL (the latter is special, it targets C :p ) You can use SPARK without knowledge of Z, while this may be interesting if you can (I just use to know it a few). This is part of culture. Talking about culture, in the domain of logic applied to computer science, you may be interested into learning about Intuitionistic Logic (deals with constructive proof creation, which talks well to computer science) |