1. Here is an airline reservation program accompanied by an explanation of the notations used. The identifiers in bold face are defined in the Elephant language; identifiers in italics belong to of the particular program.
is an action defined in the Elephant language.
It means to do what is requested.
is the action of answering a query.
In general, admit(psgr,flt) means admitting the passenger psgr to the flight flt. It is an action defined in the particular program. However, it has two possible interpretations, (1) telling the agent at the gate to let the passenger in and (2) actually letting the passenger in. The first is an illocutionary act, the second is a perlocutionary act.
commitment is a function taking a future action as an argument and generating from it an abstract object called a commitment. The internal actions make and cancel and the predicate cancel apply to commitments. make, exists and cancel are part of the Elephant language and have meanings and be axiomatized independently of the particular abstract objects being made, tested and destroyed. The notion of faithfulness involving the fulfillment of commitments will not necessarily extend to other abstract entities.
In Elephant 2000, we associate to the right, so the above statement is equivalent to
Even for this simple reservation program it is worthwhile to distinguish between input-output and accomplishment specifications. The distinction comes up in the interpretation of admit(psgr,flt). If we interpret it as ordering the admission, then it's an illocutionary act. If we interpret is as making sure the passenger can actually get on, then it is a perlocutionary act.
It is an input-output specification of the program that it not order the admission of more passengers than the capacity of the flight. It is an external fact that the plane will hold its capacity and not more.
2. Similar considerations apply to a minimal program for a control tower.
It receives requests to land. It can perceive the positions of the airplanes. It can issue instructions like ``Cleared to land'' or ``You are number 3 following the red Cessna'' or ``Extend your downwind leg'' or ``Turn base now''. Its input-output specifications involve only its perceptions and its inputs and outputs. They include that it should not say ``Cleared to land'' to an airplane until the previous airplane is perceived to have actually landed. The verification of the input-output specifications involve facts about the program itself.
The accomplishment specifications provide that the airplanes should land safely and as promptly as is compatible with safety. Their verification involves assumptions about the correctness of the program's perceptions and the behavior of airplanes in response to instructions.
(The word ``perceive'' is ambiguous in English usage. The Webster's Collegiate dictionary uses ``become aware of'', and this implies that if one ``perceives that an airplane has left the runway'', then it really has left it. However, a poll of colleagues found that most considered that a person could perceive it without it actually being true. For our purposes we need both notions, so we'll add adverbs to make the meaning clear.)
A specialist in airplanes may verify that if the program meets its input-output specifications, then it will also meet its accomplishment specifications.
The concepts of input-output and accomplishment specifications apply to programs that interact with the outside world in general and not just Elephant programs. However, we expect them to be easier to state and verify for Elephant programs.