Information Technology Reference
In-Depth Information
Webbo State
Loginfo
no : N
pd : Pass
at : C
in , lock : B
no
3
in
( no = 0)
lock
( no = 3)
State
U , A , M : P Users
C : P Clients
mng : C M
log : U Loginfo
post : U × U Mess
Init
State
=
{}
A
M
= {}
U = A
M
u : U · log ( u ) . no = 0 ∧¬ log ( u ) . in
post =
A M
U
{}
Fig. 1. State for the model Webbo
ClientManagement
CreateClient
Δ( C , mng )
a ?: A
c ?: Clients
m ?: M
RemoveClient
Δ( C , mng )
a ?: A
c ?: C
log ( a ?) . in
¬∃ u : U · log ( u ) . at = c ? log ( u ) . in
C = C { c ? }
mng
log ( a ?) . in
C = C { c ? }
mng
= mng ⊕{ ( c ? , m ?) }
=
{ c ? } −
mng
Fig. 2. Client management in Webbo
Auser u ? who is logged in may send a message, with operation UserPost ,toanamed
user r ?; or may read mail without deleting it (an easy modification updates the state to
remove read post), by outputting the mail in the set ms ! of messages. Reading mail
does not change the system state; sending it updates only the state component post .See
Figure 6.
But the most subtle action is that of logging in. A user may (attempt to) log in only
if not already logged in. The attempt fails if the input password id? is wrong; on the
third consecutive failed attempt the user is locked out, but otherwise another attempt is
permitted. A successful attempt returns the count no to 0 and changes the status of the
 
Search WWH ::




Custom Search