Specification for Testing - Formal Methods and Hybrid Real-Time Systems - page 290

The link needs to include steps such as logging out from administrator a 's account,
logging in to user u 's account, opening the post and then viewing the message. Those
steps assume that the tester (or the test execution engine) knows the password of r 's
account. If this assumption is false, the situation cannot be tested. If the password is not
known, the test case for the CreateMessage function can define a series of preparatory
steps that includes the creation of a specific dummy user for whom the tester should
record the password to be used later. Administrator a then creates a message for this
dummy user. However, the testing is restricted to just that dummy user.
A similar situation exists while creating a client. The implementation does not pro-
vide any actual information about the status of the operation. There is no way way of
verifying that the client has indeed been created and users for it can be created. The
link must try to add a user to the client and then delete the user. If this succeeds the
client has been created. In this case the person creating the client is an administrator
and does not have the right to create a user. Hence the test script needs to logout and
login as manager to test the creation of a client. The system must allow this process for
the testing to be automated.
Such situations are now examined in a more systematic fashion and it is shown how
these problems lead to a tradeoff between specification and implementation.

4Laws

State-based specifications and algebraic specifications feature quite different styles of
requirements capture. Nonetheless the state-based specifier is typically aware of laws
relating the operations being described in the state-based notation. For example, a
'do' operation is often accompanied in a system by an 'undo', in which case their
composition—perhaps under some assumption, or by abstracting some components of
state—leaves state unchanged. The following examples demonstrate those ideas using
Webbo .

4.1 Laws in Webbo

Creation of a client followed by its removal leaves the state of Webbo unchanged.
Conversely, removal of a client followed by its creation may not leave state invariant
because the manager assigned during client creation may not coincide with that just
deleted in client removal; but other state components are unchanged.
For this some notation is required. Suppose that (state) schema S includes an observ-
able a : A . Then the schema with that observable abstracted, and its identity function,
are defined:
State a =

∃ a : A · State

s .
(In practice it may be simpler to list, as subscripts there, the state components that are
present rather than those that are not; but this notation is more convenient in theory.)
Now the previous laws can be expressed:

id[ State a ]= λ s : State a ·

CreateClient

9 RemoveClient = id

RemoveClient

9 CreateClient = id[ Webbo State mng ] .