[Prev][Next][Index]

Re: Can the Larch Prover be used on LSL traits?



The Larch Prover can indeed be used to check the "implies" portions of LSL
traits.  An experimental version of the LSL Checker, lsl3.1beta3, extracts
axioms and proof obligations from LSL traits, more or less along the lines
described in the Larch book.  You can obtain the checker, along with the new
Relase 3.1 of LP, by anonymous ftp from larch.lcs.mit.edu.

Before releasing a new official version of the LSL Checker, we intend to
redesign it slightly to facilitate proof maintenance.  Now, when you change the
axioms or implications in a trait, you can use the Checker to regenerate axioms
and proof obligations for LP.  But there is no convenient way to integrate the
proof strategies in your old LP proof script with the new output of the
Checker.  We intend to remedy this.



Reference(s):