Alloy中'private'关键字的含义？'enum'声明的含义？

Question

的合金4语法允许签名声明(和其他一些东西)携带private关键字.它还允许允许规范包含表单的枚举声明

enum nephews { hughie, louis, dewey }
enum ducks { donald, daisy, scrooge, nephews }

语言参考没有(据我所知)描述private关键字或enum构造的含义.

有文件吗？或者它们是否在语法中作为为将来的规范保留的构造？

Answer 1

这是我对这两个关键词的非正式理解。

enum nephews { hughie, louis, dewey }

在语义上等价于

open util/ordering[nephews] as nephewsOrd

abstract sig nephews {}

one sig hughie extends nephews {}
one sig louis extends nephews {}
one sig dewey extends nephews {}

fact {
  nephewsOrd/first = hughie
  nephewsOrd/next = hughie -> louis + louis -> dewey
}

该private关键字意味着如果一个 sig 具有该private属性，则其标签在同一模块内是私有的。这同样适用于私有字段和私有函数。