[Prev][Next][Index]
No Subject
Thank you for responding to my message. Be sure to let me know if I should
be using another forum for these questions rather than mailling you
directly. I am hesitant to do this kind of exploring in a public
forum (as opposed to getting advice or answers to specific questions).
I guess it seems that if one trait can be specified in terms of another
trait, it follows that one interface should be specifiable in terms of
another. This would allow (for example) the specification of a buffered
stream I/O system on top of an unbuffered blocked I/O system. Any one
who has done I/O with the standard 'C' library realizes that the
specification of 'fprintf()' is not independant of 'write()'. It may be
argued that they should be independant, but... So, even if one wanted to
write a Larch specification for the Standard C Library, one needs somehow to
indicate what happens if 'fprintf' and 'write' are used together. Can this
be done properly at the 'trait' level?
It seems that is should not be difficult to support operations of the form:
given an pre-environment described by an interface x,
if interface y is used as an operator on this environment
then predicate P holds in the post-environment.
Proof obligations for LP could be generated for interface y with the
(stricter) environment implied by interface x.
Thanks again for your time.
doug makofka
makofka@monet.vill.edu