private namespace

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).

Example 1: private sig, private field, private function, and private predicate

module moduleA
open moduleB

module moduleB
sig Person {
  favorite: Book,
  knows: set Person,
  private likes: set Person
}

private sig Book { year: Int }

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.

Example 2: private open

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”.