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