Issue 6124:  Local pre/postcondition example (uml2-superstructure-ftf)
Source: NIST (Dr. Conrad Bock, conrad.bock(at)nist.gov)
Nature: Uncategorized Issue
Severity: Significant
Summary: Provide a local pre/postcondition example that is really local
Resolution: see above
Revised Text: 
Actions taken:
August 30, 2003: received issue
March 8, 2005: closed issue
Discussion: 
Modify the localPre/Postconditions for Figure 200 to read:
«localPrecondition» A drink is selected that the vending machine contains and the correct
payment is made
«localPostcondition» The vending machine dispensed the drink that is selected and
correct change is provided.
Modify the text above Figure 200.
-From: “The example below illustrates local pre and postcondition for the action of a
drink dispensing machine.”
-To: The example below illustrates local pre and postcondition for the action of a drink
dispensing machine. This is considered “local” because a drink-dispensing machine is
constrained to operate under these conditions for this particular action. For a machine
technician scenario, the situation would be different. Here, a machine technician would
have a key to open up the machine, and therefore no money need be inserted to dispense
the drink, nor change need be given. In such a situation, the global pre and
postconditions would be all that is required. (Global conditions are described in Activity
specification, in the next subsection.) For example, a global precondition for a Dispense
Drink activity could be “A drink is selected that the vending machine dispenses”; the
postcondition, then, would be “The vending machine dispensed the drink that is
selected.” In other words, there is no global requirement for money and correct change.
End of Annotations:=====
Name: Conrad Bock
Company: NIST
mailFrom: conrad.bock@nist.gov
Nature: Clarification
Severity: Significant
Subject: Local pre/postcondition example


Provide a local pre/postcondition example that is really local