Information Technology Reference
In-Depth Information
UserMail
UserPost
Δ(
post
)
u
?
,
r
?:
U
m
?:
Mess
UserRead
u
?:
U
ms
!:
P
Mess
log
(
u
?)
.
in
post
log
(
u
?)
.
in
ms
! =
=
post
⊕{
(
u
?
,
r
?
,
m
?)
}
{
m
:
Mess
|∃
s
:
U
·
(
s
,
u
?
,
m
)
∈
post
}
Fig. 6.
Sending and reading post in
Webbo
LoggingIn
OK
Δ(
log
)
u
?:
U
c
?:
C
ack
!:
ok
|
fail
Fail
Δ(
log
)
u
?:
U
ack
!:
ok
|
fail
log
(
u
?)
.
in
log
(
u
?)
.
no
¬
log
(
u
?)
.
no
= 0
=
log
(
u
?)
.
no
+ 1
log
(
u
?)
.
in
log
(
u
?)
.
at
ack
! =
fail
=
c
?
ack
! =
ok
Login
Δ(
log
)
u
?:
U
c
?:
C
id
?:
Pass
ack
!:
ok
|
fail
¬
log
(
u
?)
.
in
log
(
u
?)
.
no
<
3
log
(
u
?)
.
pd
=
log
(
u
?)
.
pd
log
(
u
?)
.
pd
=
id
?
⇒
OK
log
(
u
?)
.
pd
=
id
?
⇒
Fail
log
(
v
)
=
log
(
v
)
∀
v
:
U
·
v
=
u
?
⇒
Fig. 7.
Logging on in
Webbo
user to being logged in. A successful login returns an
ok
acknowledgement whilst an
unsuccessful one returns
fail
. Operation
Login
is described in Figure 7.
Search WWH ::
Custom Search