Actions with Arguments

Now suppose I want to let my integer counter's inc action take an integer argument. We see it's even more difficult to draw BigCounter's state transition diagram, only part of which is shown here:

It's much easier and more concise to write the state transition function for inc as follows:

1

 incĒ(i: int)

            		pre true

            		post x' = x + i 

I've extended the header in my specification to include a list of input arguments (and their types). I've intentionally chosen syntax to look like programming language notation.

The technical term for what I have done is lambda abstraction. Using a single template I've actually defined an infinite set of functions, one for each integer i. Instead of defining separate actions I've defined a family of actions inc(i).

According to the above specification, there is nothing preventing the input integer argument that I hand to inc from being negative. Suppose I want my counter to always increase in value, never decrease? I can capture this by strengthening the pre-condition:

1

 incĒ(i: int)

            		pre i > 0

            		post x' = x + i 

I'll call this new machine FatCounter. It's an example of a state machine with an action that has a non-trivial pre-condition.