JPMS Module Path question

[Alex Buckley]

On 6/14/2017 12:55 PM, Alex Buckley wrote:
> 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

Some comments on the three "interesting things" noted in the blog:

- The modeling of 'static' dependences seems to cause nothing but 
trouble, since it leads to an inaccurate 'requires static java.base'.

- The statement that "there is no rule in the JLS about [an overlap in 
packages between java.base and another module]" is incorrect. See the 
"association" of compilation units with modules in JLS9 7.3. The rule is 
specified as weakly as possible (that is, to apply to as few packages as 
possible) in order to maximize the freedom of compilers.

- The statement "The java.base module has qualified exports to other 
modules." is puzzling because the model of the java.base module -- "one 
sig JavaBaseModule ..." -- does not indicate any exports.

Alex