Transcript Document

Specifications with assumptions and
guarantees (in general)
extracts from course notes for ELG7186B in 1999
• A system component functions within an environment of
other components; the component specification must take
this environment into account
• Normally, the properties specified for a component should
(only) be satisfied when certain other properties are satisfied
by the components in the environment.
• Examples:
– operating temperature should be within a given (for a computer, or a
component thereof)
» electrical power supply must be given (idem)
» disk must be formatted the right way (for a disk unit)
» line length within some bound (test processor)
Copyright 1999
G.v. Bochmann
ELG 7186B ch.2
1
Components, interfaces, architectures
component of
environment
interface
E1
I2
I3
component of
environment
specified
component
C
I1
E2
• Example: Electricity counter
– I1: electricity input (assumption: less than 100 Amps, less than 300 Volts)
– I2: electricity output (guarantee: same current and voltage as at I1)
– I3: read-out interface (guarantee: the value provided is equal to the energy
(i.e. product of current*voltage*time) that passed through the interface I2)
Copyright 1999
G.v. Bochmann
ELG 7186B ch.2
2
Specification formalism A/G
• Form of a specification of a component C: If the
environment satisfies the assumption AC then the component
C will guarantee the property GC
Note: For the case that the assumption is not satisfied, the specification does not
say anything about the desired behavior
• In first-order logic: the specification of C has the form “AC
implies GC “ (or “AC => GC “ )
• Assuming that the components in the environment have
specifications of the same form, the properties of the example
system above are those that can be derived from the
specifications of all the components, that is
P = (AC => GC) and (AE1 => GE1 ) and (AE2 => GE2)
Note: Let us hope that the assumptions made by E1 and E2 are small enough to
be able to obtain interesting system properties.
Copyright 1999
G.v. Bochmann
ELG 7186B ch.2
3
Conforming specializations
Definition: Given two specifications SC and SC’ of two
components C and C’, respectively, we say that SC’ conforms to
SC if SC’ implies SC (which means that all properties specified
for SC are implied by the properties specified for SC’). We also
say in this case that SC’ is specialization of SC .
Note: SC’ => SC
is equivalent to (AC’ => GC’) => (AC => GC )
and this is equivalent to [ ( GC’ => GC) and (AC => AC’ ) ]
If X => Y we also say that X is stronger than Y or that Y is
weaker than X.
Therfore “SC’ conforms to SC “ is equivalent to saying that the guarantees of SC’
are stronger than those of SC and that the assumptions of SC’ are weaker than
those of SC , which means [ ( GC’ => GC) and (AC => AC’ ) ]
Copyright 1999
G.v. Bochmann
ELG 7186B ch.2
4
Conforming implementations,
possibilities of replacement and reuse
• We say that an implementation conforms to a given
specification SC if the properties of the implementation
imply the specified properties. Assuming that the properties
of the implementation can be characterized in the same form,
namely by (AI => GI), then a conforming implementation
must satisfy (AI => GI) => (AC => GC ) .
– Note: this is the same form of comparison as between specifications
• Important fact: If SC’ conforms to SC then an
implementation conforming to SC’ could be used at any
place in a system where a component satisfying the
specification SC is foreseen by the system specification.
– Therefore the conforming specialization defined above should be used as
the relation which determines, within object-oriented systems, whether a
given type (or class) of object is a “specialization” (or is a “subtype” of, or
“inherits” from) another type of object.
Copyright 1999
G.v. Bochmann
ELG 7186B ch.2
5
Different kinds of refinement
• What is a “refinement”?
– The system development process usually leads from an abstract specification of
the requirements to detailed design specifications and finally to an
implementation. Each step within this process starts with a given specification
Si and leads to a “refinement” Si+1 of this specification.
– Since we want that the implementation conforms to the original requirement
specification, one usually asks that Si+1 should conform to Si . Therefore one
needs a conforming refinement.
• Special classes of refinements:
Reductions: Si+1 conforms to Si and Gi+1 is stronger than (not equal to) Gi
this is usually a reduction of nondeterminism, e.g. reduction of possible
outputs (or possible next states in state-nondeterministic systems); in the
extreme, this may lead to blocking (no output is possible, or no transition
possible)
Extensions: Si+1 conforms to Si and Ai+1 is weaker than (not equal to) Ai
Si+1 is defined for situations where Si was not defined, e.g. new allowed input
and corresponding output, function defined for input values for which Si is
undefined, etc.
Structural refinements: see next slide
Copyright 1999
G.v. Bochmann
ELG 7186B ch.2
6
Composition: Structural refinement
(an example)
C
specified
component
C3
composition :
this module C consists of
three components,
two external interfaces and
two internal interfaces
I3
I2
specified
component
C1
Copyright 1999
G.v. Bochmann
I1
specified
component
I4
C2
ELG 7186B ch.2
7
Composition: structural refinement (the
formalism)
• (Abstract) specification of component C: (AC => GC)
• The refinement of the component in terms of three subcomponents C1, C2 and C3 is given by the specifications
(ACi => GCi) , i = 1, 2, 3, respectively.
The properties of this structural refinement are given by
(AC1 => GC1) and (AC2 => GC2 ) and (AC3 => GC3)
If one wants that this refinement conforms to the original
specification (AC => GC) of the component C, one has to
verify that
[ (AC1 => GC1) and (AC2 => GC2 ) and (AC3 => GC3) ]
=> (AC => GC)
Copyright 1999
G.v. Bochmann
ELG 7186B ch.2
8