From: Mark Lorenzen <mark.lorenzen@gmail.com>
Subject: Re: Problems with SPARK 2015 and XMLAda
Date: Thu, 20 Aug 2015 03:06:31 -0700 (PDT)
Date: 2015-08-20T03:06:31-07:00 [thread overview]
Message-ID: <5677970c-024f-42f8-a8dd-8c8050e57fc3@googlegroups.com> (raw)
In-Reply-To: <87mvxmjuyz.fsf@adaheads.sparre-andersen.dk>
On Thursday, August 20, 2015 at 9:10:46 AM UTC+2, Jacob Sparre Andersen wrote:
> If you want to program in SPARK, you shouldn't try to write Ada, and
> then just run a tool, when you're done. You should read the SPARK LRM
> (or a textbook on SPARK), and understand the language.
This is a very good advice! A SPARK program isn't just an Ada program with annotations. SPARK programs must be designed from the ground up with the SPARK restrictions in mind.
Regards,
Mark
next prev parent reply other threads:[~2015-08-20 10:06 UTC|newest]
Thread overview: 25+ messages / expand[flat|nested] mbox.gz Atom feed top
2015-08-19 15:58 Problems with SPARK 2015 and XMLAda Serge Robyns
2015-08-19 20:21 ` Simon Wright
2015-08-19 21:22 ` Serge Robyns
2015-08-20 7:10 ` Jacob Sparre Andersen
2015-08-20 10:06 ` Mark Lorenzen [this message]
2015-08-20 16:38 ` Shark8
2015-08-20 18:42 ` Peter Chapin
2015-08-20 19:13 ` Jeffrey R. Carter
2015-08-20 20:00 ` Serge Robyns
2015-08-20 20:36 ` Randy Brukardt
2015-08-20 23:21 ` Shark8
2015-08-21 6:26 ` Stefan.Lucks
2015-08-21 7:30 ` Dmitry A. Kazakov
2015-08-21 8:19 ` Stefan.Lucks
2015-08-21 9:37 ` Dmitry A. Kazakov
2015-08-21 10:09 ` G.B.
2015-08-21 11:56 ` Dmitry A. Kazakov
2015-08-21 13:46 ` G.B.
2015-08-21 14:45 ` brbarkstrom
2015-08-21 15:34 ` Dmitry A. Kazakov
2015-08-21 23:44 ` Bob Duff
2015-08-22 6:22 ` Dmitry A. Kazakov
2015-08-21 10:43 ` Stefan.Lucks
2015-08-21 12:35 ` Dmitry A. Kazakov
2015-08-24 21:32 ` Randy Brukardt
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox