Re: Joe-E 2.0 Release

Tyler Close wrote:
> 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.

My suggestion follows that convention: the assertion being made is that
the code would be verifiable, if we were to verify it.

Using the name 'verified' would be analogous to using
'CheckedAsBeingImmutable' as a marker interface.

Alternatively, a name with the connotation "only Joe-E in this package"
would be more explicit.

-- 
David-Sarah Hopwood