Re: [Jmlspecs-developers] why are final model fields not permitted

[Erik P. <eri...@cs...>]

Hi Patrice,

> Why are final model fields not permitted?  Is this merely a temporary 
> limitation?

I ran into exactly this issue a few weeks back, when adding some "final" 
modifiers to the JML model classes.

I thought a bit about the pros & cons of having final model fields.
A problem with them will be enforcing that a final model field is 
not "assigned" to: you'd have to enforce that you do not do any 
assignments to fields that it depends on. Or one could insist that 
only final fields are allowed in the associated datagroup.

In the end, I came to the conclusion that in cases where you need a final 
model field, it seems simpler to use a final ghost variable instead, as 
for this it's easier to enforce finality.

Erik