From: Rod Chapman <roderick.chapman@googlemail.com>
Subject: Re: SPARK - refactoring and refinement of own state
Date: Thu, 20 Aug 2009 01:11:12 -0700 (PDT)
Date: 2009-08-20T01:11:12-07:00 [thread overview]
Message-ID: <88ecb7be-ade2-4d0b-8063-fa06d53be1e8@e34g2000vbm.googlegroups.com> (raw)
In-Reply-To: 4cc6e9da-9a4a-4a9a-8748-4c5c4a3e9362@z28g2000vbl.googlegroups.com
As for refinement..
In short: refinement only makes sense _within_ a single
package, so you can only refine "onto" states which
are logically hidden inside the package body - so either library
level state in that package body, or states of private
child packages of that package.
So...no...you can't refine from one package body to the spec
of another package, since this doesn't preserve
the abstraction.
- Rod
next prev parent reply other threads:[~2009-08-20 8:11 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
2009-08-20 8:11 ` Rod Chapman [this message]
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