From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: Re: installing SPARK GPL on Windows
Date: Sat, 07 Aug 2010 22:30:16 +0200
Date: 2010-08-07T22:30:16+02:00 [thread overview]
Message-ID: <op.vg24kqvyxmjfy8@garhos> (raw)
In-Reply-To: 1d6d0e90-c9cd-4b62-a542-467a19e69095@y11g2000yqm.googlegroups.com
Le Sat, 07 Aug 2010 19:43:30 +0200, Ada novice <posts@gmx.us> a écrit:
> On a related note, if I understand correctly then SPARK GPL only
> features a subset of the Ada language. Does this implies that not
> every program in Ada will work with SPARK?
This is not a SPARK GPL limitation (if I am not failing to understand
you), this is a SPARK feature. This is a feature of SPARK to be a safe (in
some regards) subset of Ada.
SPARK GPL is still full SPARK (more or less).
--
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.
next prev parent reply other threads:[~2010-08-07 20:30 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-08-07 17:43 installing SPARK GPL on Windows Ada novice
2010-08-07 19:37 ` Phil Thornley
2010-08-07 21:00 ` Ada novice
2010-08-08 11:12 ` Rod Chapman
2010-08-08 11:44 ` Ada novice
2010-08-08 11:48 ` Ada novice
2010-08-07 20:30 ` Yannick Duchêne (Hibou57) [this message]
2010-08-07 21:04 ` Ada novice
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox