Putting Everything So Far Together

Suppose I have an integer set, t, and in its interface is a choose action that doesn't take any arguments and removes and returns an element from t.

where choose is specified as follows:

1

 chooseĒ()/ok(int)

           		pre   

           		post    

The nondeterminism shows up in the specification for choose in the use of the set membership operator ( ) in the post-condition. I don't know which element of t will be returned; I know only that some element will be returned.

You might notice that the labels on the arcs in the state transition diagram above are different (by what is returned by choose); however, most people would still view the state transition function as nondeterministic because they would abstract from the actual value returned. In other words they would define something like this:

Finally, in a programming language that supports exception handling I would probably export a more robust interface for the choose action:

1

 chooseĒ()/okĒ(int), empty()

           		pre true

           		post   

           				            

In general, the template I use for each action in A of is:

1

 actionĒ(inputs)/  

            		pre   

            		post    

where inputs is a list of arguments and their types, is the name of one of i termination conditions (including ``ok'') and is the type of the result corresponding to . and are state predicates as defined earlier. The reserved identifiers I use are:

• ok, used in the header, to denote normal termination,
• result, used in the post-condition, to denote the value returned by an action, and
• terminates, used in the post-condition, to denote the value of termination condition. Its value can be any of the , including ``ok,'' listed in the header.

I'm glossing over a number of technicalities here regarding state variables to store input arguments and the type of the result returned, depending on how an action terminates.

Finally, for simplicity, let's assume actions return only normally unless specified otherwise (by explicitly listing exceptional conditions in their headers). Under this default case, we can avoid clutter in our specifications by not always having to write ``terminates = ok'' in the post-conditions of our actions.