string - 合金：用于字符串

Question

如何获取合金中字符串的长度？

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

我的密码签名是：

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

Answer 1

Stringin Alloy 与任何其他 sig 非常相似。唯一的区别是您可以将字符串文字分配给 type 的字段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。