A specification case study.

Dear Fellow Larch specifiers and provers,

I am an engineer from Mitsubishi Electric Corporation (Yokohama,
Japan) and have been visiting Jeannette Wing at Carnegie Mellon for
almost a year.  I have been busy specifying a device type hierarchy in
Larch and proving properties about the types using LP.  (The subtype
notion is based on Liskov and Wing's behavioral notion of subtyping.)

I would like to share with you my experience in writing specifications
and doing proofs in LP.  I have just created a home page for my
specification case study:


which has links to the LSL and LCL specifications and LP proofs.
Feel free to browse.  Your comments are welcome!

Kiyotaka Kuroda