Download Structural Usability Techniques for Dependable HCI

155
6.5 Case study 3: Casio HS-8V
6.5.2
Theorem discovery on the HS-8V device model
Running theorem discovery on the device model yields 18 theorems, which may be grouped into two
families. First, we have nine theorems:
∀06n68: •
1
n
•
∼ •
1
n
These theorems can be interpreted together as meaning after pressing the •
presses of it have no effect. Of course, in the device model, [[
no user-visible effect, pressing •
•
key once, subsequent
]] is not the identity: while it has
(for the first time) has an internal effect on the system. (In the
simulation whose models we are analysing, it sets a flag indicating that this was the most recent keypress:
presumably in the actual device the mechanism is similar.) So, these nine theorems are the device’s
model’s analogue of • ∼ λ in the user model.
Then, we have again:
1
9
∼ 1
8
and these eight theorems:
∀ 1 6 n 6 8: 1
n
•
1
(9−n)
∼ 1
n
•
1
(8−n)
These nine theorems can be interpreted together as meaning after eight digits have been entered, subsequent keypresses have no effect. Thus, they are the device model’s analogue of the singular theorem
1
9
∼ 1
8
in the user model, and they represent the limited size of the device’s display. That truth
manifests here as these nine theorems rather than just one because the pruning discussed in section
6.5.1.2 doesn’t take place here, because [[
•
]] is not the identity.
Now, neither of these insights is particular deep or surprising, but they do accurately reflect two aspects
of the device that we would expect to be true. The main thing these theorems illustrate, we propose, is
that for some purposes, it is very useful to work on models that only project user-visible state. Theorem
discovery on the user model yields two theorems which may be very clearly interpreted, whereas in the
device model, interpreting the theorems (to reach essentially the same conclusions) takes more effort.