| Æü»þ | Ê¿À®£±£²Ç¯£¸·î£¸Æü(²Ð) ¸á¸å£±»þ£³£°Ê¬¡Á£²»þ£³£°Ê¬ |
| ¹Ö±é¼Ô | Dr. David Nowak (Computing Laboratory, Oxford University) |
| ¾ì½ê | ̾¸Å²°Âç³Ø¹©³ØÉô£¸¹æ´ÛËÌ´Û£±£°£¸²ñµÄ¼¼ |
| ¹Ö±é¥¿¥¤¥È¥ë | A Unifying Approach to Data-independence |
A concurrent system is data-independent
with respect to a data type
when the only operation it can
perform on values of that
type is
equality testing.
The system
can also assign,
input,
nondeterministically choose, and output
such values. Based on this
intuitive definition,
syntactic restrictions
which ensure
data-independence have been formulated
for a variety of different
formalisms. However, it is difficult
to see how these are related. We
present the first semantic
definition of data-independence
which
allows equality testing. We
also present a theorem which,
given a
system and a specification
which are data-independent, enable
the
verification for all instantiations of the
data types to be reduced to
the verification for a finite number of finite
instantiations.
[Ìá¤ë]