SOC 2 Composition 2 slide-23

Definitions and Assumptions

A Web Service may have	inputs (at least one),
	preconditions,
	outputs,
	effects, and/or
	contracts (ignore for now)

Each input and output name is a unique property. Inputs expect a value to be assigned to the property upon a call to the service. Outputs assign a value to properties. Efects and Preconditions are Conditions.

Conditions consist of a fluent together with a set of properties, each of which may or may not have a bound value for any one or all states in which the service is called:
e.g., (Transfered (amount $500) (from-account 8238) (to-account 2834))

Assumptions:
a) If a property's value is changed by the service, it is mentioned not only as an input but also as an output.
b) All properties mentioned in an effect are mentioned as input or outputs of the service.
c) If a property in a precondition is not mentioned as an input to the service, then the precondition must be provable in that state.