a. Black box description: trace semantics
ie., a description in terms of
the data exchanged between the component and its environment,
in terms of the I/O-trace, ie., the order of
inputs (data crossing into the component on the "set"-channel in "set"-events)
and outputs (data crossing into the environment on the "get"-channel in "get"-events).
|
| set
| |
vn ...
vk+1
| 
|
| c:variable
|
| get
| 
|
vk ...
vk ...
v1 ...
v1
|
|
Variables c are characterized by the following trace:
trace(c) = (
set:vk ·
{get:vk}*
)k:=1,...
cf. [RegTy]
| |
b. Gray box description: Value container model
|
| set
| |
vn ...
vk+1
|
|
| c:variable
|
| get
| |
|
vk ...
vk ...
v1 ...
v1
|
|
«In computing, a variable is an object that contains a value;
this value may be inspected and updated as often as desired »
[Watt 37].
| UPDATE EVENT
| = change of variable's value
to next value vk+1
(old value vk is forgotten)
|
|
|  effect
|
|
