A new reserved keyword "private" has been added for declaring a sig, fun, pred, field, or an entire imported module as being "private" to this module (and does not show up in the namespace of other modules that import this module).
module moduleA open moduleB |
module moduleB sig Person { favorite: Book, knows: set Person, private likes: set Person } private sig Book { year: Int } fun allBook: set Book { Book } private fun union[a, b: set univ]: set univ { a+b } |
From moduleA, you can refer to "Person", "favorite", "knows", and "allBook".
You cannot refer to "likes" because it is a private field, and you cannot refer
to "union" because it is a private function.
From moduleA, you cannot refer to "Book" since it is a private sig,
and you cannot refer to "year" because it is a field in a private sig (and thus
it is automatically private).
The important thing to note here is this is purely a namespace management mechanism, and you may still be able to access these "hidden" values via other names. For example, if you have Person X, you can access X.favorite to see the Book atom corresponding to his favorite book, even though you cannot refer to the Book signature by name. Likewise, you can get every atom in the Book sig by calling the "allBook" function.
module moduleA open moduleB |
module moduleB private open moduleC open moduleD sig B { } |
module moduleC sig C { } |
module moduleD sig D { } |
In moduleB, you can certainly refer to B, C, and D.
In moduleA, you can refer to B and D, but you cannot refer to C, since moduleB imported moduleC as a "private import".