Next: 6 Software composition Up: Monotonicity and Lattices as Previous: 4 An analogy of
Next: 6 Software composition
Up: Monotonicity and Lattices as
Previous: 4 An analogy of
A development contract is an abstract specification, which is agreed on at the beginning of a development. The contract contains nondeterministic choices (implicit or explicit) which are assigned to developers. The assigned choices may be decided upon by its developer separately. Separate programming (done in parallel) is the rationale for having a development contract in the first place.
A lattice has two explicit binary choice operations and until now, I have only seen the use for one or for as many as there are contract parties. How does it then fit together? - To answer this question, I need to understand the intuitive interpretation of the choices in program semantics. The essential difference is that one choice is determined benevolently in order to establish a desired goal. The other choice may be resolved arbitrarily, i.e. each variant establishes the desired goal anyways.
The purpose of having both choices in the programming by a development contract is as follows. After the completion of the contract, each developer replaces the choices assigned to him by ``benevolent choice'' and the choices assigned to others by ``arbitrary choice''. He then refines the altered contract to a concrete implementation, resolving the benevolent choice according to his own goals and criterias.
When all contract parties finally have completed their separate development, they combine their implementations together. Because each developer assumed an arbitrary choice of his contract partners, his own development is valid irrespectively of the others' choices. Provided the development was carried out according to valid refinement laws, the combined implementation satisfies the original abstract specification. A system test then should cause no trouble.
Philipp Heuberger