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

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

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

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

有没有可用的文档？还是它们在语法上是为将来的规范保留的构造？

最佳答案

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

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关键字意味着，如果一个信号具有private属性，则其标签在同一模块内是私有(private)的。私有(private)字段和私有(private)功能也是如此。

关于alloy - 合金中 'private'关键字的含义？ 'enum'声明的含义？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/11992831/