[Prev][Next][Index]

Can the Larch Prover be used on LSL traits?


I've been reading up on Larch lately... ravenously sponging up all
the stuff available over the net.

I'm getting the hang of LSL, LM3, LCL, sorts, etc., and I read some
of the Larch Prover papers. (I was trying to understand the
distinctions between the way LP reasons about things vs. the way HOL
and Nqthm reason about things, but I think I've got a few years of
study before I can really grok...)

Anyway... so far, I understand this:

* you can write LSL traits to give formal specifications of constants
and operators in its many-sorted logic with nifty syntax.

* you can check the syntax and sort usage in your LSL trait files with
the lsl tool. (and apparently generate tex/postscript and HTML from
them... are the tools for this available?)

* you can then develop interfaces in programming languages like
Modula-3, C, C++, and Smalltalk, and you can relate your interfaces
to the LSL traits using interface languages (LM3, LCL, etc.)

* you can then syntax and sort-check your interface specifications.

* tools like lclint can help you develop correct implementations of
these specification by doing (necessarily incomplete, but still handy)
checks of your code against the specifications.

* you can use LP to assist you with the gory details of proofs,
presumably related to the LSL traits underlying your software system.

I would think LP would be handy to check the "implies" portions of LSL
traits, but as far as I can tell, translating LSL traits to LP input
is a wholly manual process. I don't see any way to, for example,
"import" an LSL trait into an LP proof session.

It seems as though a set of LSL traits, interface specifications, and
related LP proof scripts would be a great way to increase the
reliability of a software system: it encourages discipline in
development, serves as detailed, yet concise documentation, provides a
form regression testing to track the scope of chages made during
maintenance, and provides arguments for correctness of key algorithms.

Suppose I had such a software system, and I want to make an
enhancement. The various tools will assist me in keeping the LSL
traits, LCL specifications, and C source in sync, but it seems that I
have to update the LP proof scripts manually, no?

Am I missing something?

Dan

p.s. in your replies, note that I'm not subscribed to the list (yet).
Follow-Up(s):