CODEWITHSUNDEEP
vdm++
Tirafesi
Tirafesi

Reputation: 1479

Pre-condition not working

I'm trying to create a simple 'signup' method.

-- 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);

The problem I'm having is with the pre-condition. How can I write the pre-condition 'username is unique'? (ie there is no user in users where user.username = username)

Note: users is a set of User

Edit: pre (username not in set users.username) is what makes most sense to me, but this doesn't even compile.

Upvotes: 0

Views: 89

Answers (1)

Nick Battle
Nick Battle

Reputation: 703

It looks like you need a "forall". Your precondition wants to say that "for all of the users' usernames, the new user's name is not equal to them". An alternative would be to generate the set of existing usernames with a set comprehension, and then say the new username is not in that set.

Let us know if the syntax for the above isn't obvious.

Upvotes: 1

Related Questions