vdm++ - 前置条件不起作用

Question

我正在尝试创建一个简单的“注册”方法。

-- Creates a new account
public signup: String * String ==> ()
signup(username, password) == (

    -- create user
    dcl user: User := new User(username, password);

    -- add user
    users := users union {user};
)
pre (let u in set users in u.username <> username);

我遇到的问题是前提条件。如何编写前提条件“用户名是唯一的”？（即user在userswhere中没有user.username = username）

注：users是set一个User

编辑：pre (username not in set users.username)对我来说最有意义，但这甚至无法编译。

Answer 1

看起来你需要一个“forall”。您的先决条件想说“对于所有用户的用户名，新用户的名称不等于他们”。另一种方法是生成具有集合理解的现有用户名集合，然后说新用户名不在该集合中。

如果上面的语法不明显，请告诉我们。