From: Rod Chapman <roderick.chapman@googlemail.com>
Subject: Re: SPARK - refactoring and refinement of own state
Date: Thu, 20 Aug 2009 01:06:35 -0700 (PDT)
Date: 2009-08-20T01:06:35-07:00 [thread overview]
Message-ID: <d69c6a2b-551c-4296-a9d7-60438a3f65cd@p36g2000vbn.googlegroups.com> (raw)
In-Reply-To: 4a8cfd47$0$30230$9b4e6d93@newsspool1.arcor-online.net
On Aug 20, 8:37 am, Georg Bauhaus <rm.tsoh.plus-
bug.bauh...@maps.futureapps.de> wrote:
> Maciej Sobczak wrote:
> > However, the examiner says:
>
> > 4 package body Greetings
> > ^
> > *** Syntax Error : No DOTTED_SIMPLE_NAME can start with
> > reserved
> > word "BODY".
>
> FWIW, there is a rule about Ada with-ing versus SPARK with-ing
> that explains, IIRC, that the #clauses must go before
> the package spec, in SPARK, not just the body. It's in the
> SPARK book somewhere.
Yeah - the "inherit" anno always goes on the spec. In this
case the Examiner see the "inherit" and then expects to see
a package spec, so then objects when the word "body" appears.
We'll see if we can generate a better error message for this case.
- Rod, SPARK Team
next prev parent reply other threads:[~2009-08-20 8:06 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-08-20 7:18 SPARK - refactoring and refinement of own state Maciej Sobczak
2009-08-20 7:37 ` Georg Bauhaus
2009-08-20 8:06 ` Rod Chapman [this message]
2009-08-20 8:11 ` Rod Chapman
2009-08-20 8:44 ` Maciej Sobczak
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox