JavaModelingLanguage / RefMan

4 stars 0 forks source link

Deprecate the keywords field, method and constructor #45

Closed davidcok closed 2 years ago

davidcok commented 2 years ago

Classic JML defines the keywords field, method and constructor. In the grammar they are like pseudo modifiers. Though the grammar defines them, there is no discussion of them in the DRM. I've never implemented or used them, nor can I think of a use-case for them.

I advocate deprecating them.

mattulbrich commented 2 years ago

+1

leavens commented 2 years ago

These were originally intended to help with parsing, but if they are not needed (as they appear not to be) then I am also fine with deprecating them.