合金：用于字符串答案

【问题标题】：Alloy: use to String合金：用于字符串
【发布时间】：2013-09-18 15:02:37
【问题描述】：

如何获取Alloy中String的长度？

如果我想说密码必须至少有8个字符，我该如何表达那个字符串的长度？

我的密码签名是：

sig Password{ 密码：一个字符串}

【问题讨论】：

【解决方案1】：

Alloy 中的String 与任何其他 sig 非常相似。唯一的区别是您可以将字符串文字分配给 String 类型的字段，例如，

some p: Password | p.password = "secret"

Alloy 不支持字符串函数。解决诸如

之类的约束

some p: Password | len[p.password] > 5

需要专门的字符串求解器，而 Alloy 不需要。

如果你只关心密码长度，你可以这样做

sig Char {}
sig Password { 
   password: seq Char 
} { 
   #password > 5
}

如果您需要能够解决更复杂的字符串约束（包括正则表达式），您应该研究专门的字符串求解器，例如 Hampi。

【讨论】：