[Prev][Next][Index]
No Subject
I have been using Larch/C to reverse engineer some code. I have run into two
problems (maybe just my understanding) that I think are related. The two
problems are: the desire to include the invocation (call) of one Larch/C
interface within another, and the desire to show the correctness of a program
which makes use of the collection of interfaces described by my Larch/C
specification.
The first problem turned up as a result of the layering used in the application
being evaluated. The top-level code causes control to be passed through
multiple layers to get 'work' done. Each of these layers has its own interface.
The upper layers count on the lower layers to the extent that their
specification could include the fact that the specifier wants the implementor
to use the lower layers: not 'go after' the underlying machine/processes/etc.
Also, it would seem natural that a claim or an ensures clause be used to
state the intended state modifications explicitly caused by the invocation of
the lower-level interface. Is there a way to do this?
The second problem has to do with my understanding of what my Larch-based
specification will be: it will be a collection of interfaces for operating
on abstract data types. What I would like is some way to specify a program
using these interfaces which is correct given some formal requirement
statement for the program. It seems as if the construct used to solve the
first problem could be used here as well, allowing reasoning about
interface usage.
doug makofka
makofka@monet.vill.edu