[e-lang] Joe-E 2.0 Release
tyler.close at gmail.com
Wed Mar 12 11:45:39 EDT 2008
On Wed, Mar 12, 2008 at 8:00 AM, David-Sarah Hopwood
<david.hopwood at industrial-designers.co.uk> wrote:
> David Wagner wrote:
> > 1. Joe-E programmers would normally put their Joe-E code into
> > separate packages that contain only Joe-E code. They would add
> > the @verified annotation to those packages.
> Just a nitpick: if I understand correctly, this is an assertion that
> the code is intended to be verifiable, not that it has been verified.
> So, I think @org.joe_e.verifiable would a better name for the annotation.
The assumption that the code is what it says it is, is already used by
all of the other marker types used by the Joe-E verifier, such as
org.joe_e.Immutable. I think we should stick to the convention we've
In general, the convention I've used in Waterken code is that you
can't make any assumptions about assertions implied by an interface
name. Such assumptions are only warranted for classes, where I also
follow the convention that all classes are final.
More information about the e-lang