JPMS Module Path question

[Alex Buckley]

On 6/14/2017 5:59 AM, Peter Kriens wrote:
> I am trying to formally specify JPMS using Alloy.

A quick note on http://aqute.biz/2017/06/14/jpms-the-sequel.html, which 
seems to have misunderstand a (now rather out of date) JLS draft.

"PackageDeclaration in a module declaration seems topsy turvy and it 
does not compile. So ignoring this."

Not sure what this means. PackageDeclaration is not "in" a module 
declaration. The JLS has never allowed a compilation unit that contains 
both PackageDeclaration and ModuleDeclaration.

"The module name in the declaration uses a different production then the 
module name in the requires. They are identical but it is sloppy."

One is a declaration of an entity (introduces a name for the entity by 
specifying identifiers) and one is a use of a previously declared entity 
(specifies a previously introduced name). It so happens that the 
syntactic forms are the same, but it is proper to distinguish 
declaration from use as has been done throughout the JLS since 1996.

Alex