[e-lang] Joe-E 2.0 Release
david.hopwood at industrial-designers.co.uk
Wed Mar 12 12:16:48 EDT 2008
Tyler Close wrote:
> 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
> 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.
More information about the e-lang