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!