推理子类型的属性

Question

我发现自己经常遇到以下情况：

sig Property {}

abstract sig Unit {
  property: some Property
}


sig Hardware, Software, Services extends Unit {}

fact  {
  no Hardware.property & Software.property
  no Hardware.property & Services.property
  no Software.property & Services.property
}

也就是说，我有一个声明属性的抽象签名，以及一些扩展该签名的子类型。我想确保子类型之间的属性property 没有重叠。

将允许Hardware 的两个实例共享property 值，但绝不允许Hardware 和Software 实例具有公共属性。

我真的不想像那样写fact。如果我添加第四种Unit，我很容易搞砸事实。

这感觉就像我需要能够自省类型，但我不知道有什么工具可以做到这一点。

有什么建议吗？

Answer 1

这可能不是最优雅的解决方案，但您可以为每个单元子类型定义一个属性子类型。

这样，您就不需要手动编写叉积，从而减少出错的可能性:-)。

abstract sig Property {}

abstract sig Unit {
  property: some Property
}

sig Hardware, Software, Services extends Unit {}
sig PropHard , PropSoft, PropServ extends Property{}

fact {
    Hardware.property in PropHard
    Software.property in PropSoft
    Services.property in PropServ
}