alloy - 合金中 'private'关键字的含义？ 'enum' 声明的含义？

Question

Alloy 4 grammar允许签名声明(和其他一些东西)携带 private关键词。它还允许允许规范包含形式的枚举声明

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

The language reference没有(据我所知)描述 private 的含义关键字或 enum构造。

有可用的文档吗？还是它们在语法中是为 future 规范保留的结构？

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属性，其标签在同一模块内是私有(private)的。这同样适用于私有(private)字段和私有(private)函数。