Re: Joe-E 2.0 Release

On Wed, Mar 12, 2008 at 8:00 AM, David-Sarah Hopwood
<david.hopwood-mRVxzIiVagSlV3Ge8JjJtnfLna9zW77MtUK59QYPAWc@public.gmane.org> 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
already established.

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.

--Tyler