string - 合金: 弦に使用

Question

合金の弦の長さはどのように取ることができますか?

パスワードは 8 文字以上である必要があると言いたい場合、その文字列の長さはどのように表現できますか?

パスワードの署名は次のとおりです。

sig Password{ パスワード: 1 つの文字列 }

Answer 1

Stringin Alloy は他のシグとほとんど同じです。唯一の違いは、文字列リテラルを 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などの特殊な文字列ソルバーを調べる必要があります。