From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
Subject: Re: task discriminants and invariant expressions in SPARK
Date: Thu, 03 Nov 2011 15:15:06 +0100
Date: 2011-11-03T15:15:06+01:00 [thread overview]
Message-ID: <4eb2a1ea$0$6580$9b4e6d93@newsspool3.arcor-online.net> (raw)
In-Reply-To: <4eb28508$0$6565$9b4e6d93@newsspool4.arcor-online.net>
On 03.11.11 13:11, Georg Bauhaus wrote:
> On 03.11.11 10:34, Phil Thornley wrote:
>
>> I can't find anything relevant in the documentation - there's no list
>> of known deficiences in the GPL release note.
>>
>> It is probably worth reporting this even if you are not a supported
>> customer - use spark@adacore.com as the address (and include "SPARK"
>> in the subject line otherwise it gets dumped in the spam bucket).
>
> Thanks for having a look. A report is now sent.
I've got a reply! Both, discriminant-is-constant and
discriminant-turned-variable through making it a parameter
would be expected in the current RavenSPARK model, and
deliberately. Good to know.
prev parent reply other threads:[~2011-11-03 14:15 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-10-31 12:38 [Q] task discriminants and invariant expressions in SPARK Georg Bauhaus
2011-10-31 13:04 ` Georg Bauhaus
2011-11-03 9:34 ` Phil Thornley
2011-11-03 12:11 ` Georg Bauhaus
2011-11-03 14:15 ` Georg Bauhaus [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox