The Larch Prover, or LP for short, is an interactive theorem proving system for multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990s to reason about designs for circuits, concurrent algorithms, hardware, and software.[1]

Unlike most theorem provers, which attempt to find proofs automatically for correctly stated conjectures, LP was intended to assist users in finding and correcting flaws in conjectures—the predominant activity in the early stages of the design process. It worked efficiently on large problems, had many important user amenities, and could be used by relatively naïve users.

Development

LP was developed by Stephen Garland and John Guttag at the MIT Laboratory for Computer Science with assistance from James Horning and James Saxe at the DEC Systems Research Center, as part of the Larch project on formal specifications.[2] It extended the REVE 2 equational term rewriting system developed by Pierre Lescanne,[3] Randy Forgaard[4] with assistance from David Detlefs and Katherine Yelick. It supports proofs by equational term rewriting (for terms with associative-commutative operators), cases, contradiction, induction, generalization, and specialization.

LP was written in the CLU programming language.

Sample LP Axiomatization

declare sorts E, S
declare variables e, e1, e2: E, x, y, z: S
declare operators
  {}:                   -> S
  {__}:            E    -> S
  insert:          E, S -> S
  __ \union __:    S, S -> S
  __ \in __:       E, S -> Bool
  __ \subseteq __: S, S -> Bool
  ..

set name setAxioms
assert
  sort S generated by {}, insert;
  {e} = insert(e, {});
  ~(e \in {});
  e \in insert(e1, x) <=> e = e1 \/ e \in x;
  {} \subseteq x;
  insert(e, x) \subseteq y <=> e \in y /\ x \subseteq y;
  e \in (x \union y) <=> e \in x \/ e \in y
  ..
set name extensionality
assert \A e (e \in x <=> e \in y) => x = y

Sample LP Proofs

set name setTheorems
prove e \in {e}
qed

prove \E x \A e (e \in x <=> e = e1 \/ e = e2)
  resume by specializing x to insert(e2, {e1})
qed

% Three theorems about union (proved using extensionality)

prove x \union {} = x
  instantiate y by x \union {} in extensionality
qed

prove x \union insert(e, y) = insert(e, x \union y)
  resume by contradiction
    set name lemma
    critical-pairs *Hyp with extensionality
qed

prove ac \union
    resume by contradiction
      set name lemma
      critical-pairs *Hyp with extensionality
    resume by contradiction
      set name lemma
      critical-pairs *Hyp with extensionality
qed

% Three theorems about subset

set proof-methods =>, normalization

prove e \in x /\ x \subseteq y => e \in y by induction on x
      resume by case ec = e1c
        set name lemma
        complete
qed

prove x \subseteq y /\ y \subseteq x => x = y
    set name lemma
    prove e \in xc <=> e \in yc by <=>
        complete
        complete
    instantiate x by xc, y by yc in extensionality
qed

prove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z by induction on x
qed

% An alternate induction rule

prove sort S generated by {}, {__}, \union
    set name lemma
    resume by induction
      critical-pairs *GenHyp with *GenHyp
      critical-pairs *InductHyp with lemma
qed

Bibliography

Pascal André, Annya Romanczuk, Jean-Claude Royer, and Aline Vasconcelos, "Checking the consistency of UML class diagrams using Larch Prover", Proceedings of the 2000 International Conference on Rigorous Object-Oriented Methods, page 1, York, UK, BCS Learning & Development Ltd., Swindon, GBR, January 2000.

Boutheina Chetali, "Formal verification of concurrent programs using the Larch Prover", IEEE Transactions on Software Engineering 24:1, pages 46–62, January 1998. doi: 10.1109/32.663997.

Manfred Broy, "Experiences with software specification and verification using LP, the Larch proof assistant", Formal Methods in System Design 8:3, pages 221–272, 1996.

Urban Engberg, Peter Grønning, and Leslie Lamport, "Mechanical Verification of Concurrent Systems with TLA", Computer-Aided Verification, G. v. Bochmann and D. K. Probst editors, Proceedings of the Fourth International Conference CAV'92), Lecture Notes in Computer Science 663, Springer-Verlag, June 1992, pages 44–55.

Urban Engberg, Reasoning in the Temporal Logic of Actions, BRICS Dissertation Series DS 96–1, Department of Computer Science, University of Aarhus, Denmark, August 1996. ISSN 1396-7002.

Stephen J. Garland and John V. Guttag, "Inductive methods for reasoning about abstract data types," Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 219–228, San Diego, CA, January 1988.

Stephen J. Garland and John V. Guttag, "LP: The Larch Prover," Ninth International Conference on Automated Deduction Lecture Notes in Computer Science 310, pages 748–749, Argonne, Illinois, May 1988. Springer-Verlag.

Stephen J. Garland, John V. Guttag, and Jørgen Staunstrup, "Verification of VLSI circuits using LP," The Fusion of Hardware Design and Verification, pages 329–345, Glasgow, Scotland, July 4–6, 1988. IFIP WG 10.2, North Holland.

Stephen J. Garland and John V. Guttag, "An overview of LP, the Larch Prover," Third International Conference on Rewriting Techniques and Applications Lecture Notes in Computer Science 355, pages 137–151, Chapel Hill, NC, April 1989. Springer-Verlag.

Stephen J. Garland and John V. Guttag, "Using LP to debug specifications," Programming Concepts and Methods, Sea of Galilee, Israel, April 2–5, 1990. IFIP WG 2.2/2.3, North-Holland.

Stephen J. Garland and John V. Guttag, A Guide to LP: the Larch Prover, MIT Laboratory for Computer Science, December 1991. Also published as Digital Equipment Corporation Systems Research Center Report 82, 1991.

Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy Lynch, "Verifying timing properties of concurrent algorithms," FORTE '94: Seventh International Conference on Formal Description Techniques, pages 259–273, Berne, Switzerland, October 4–7, 1994. Chapman & Hall.

Ursula Martin and Michael Lai, "Some experiments with a completion theorem prover", Journal of Symbolic Computation 13:1, 1992, pages 81–100, ISSN 0747-7171.

Ursula Martin and Jeannette M. Wing, editors, First International Workshop on Larch, Proceedings of the First International Workshop non Larch, Dedham, Massachusetts, July 13–15 1992, Workshops in Computing, Springer-Verlag, 1992.

  • Michel Bidoit and Rolf Hennicker, "How to prove observational theorems with LP", pages 18–35
  • Boutheina Chetali and Pierre Lescanne, "An exercise in LP: the proof of a non-restoring division circuit",, pages 55–68
  • Christine Choppy and Michel Bidoit, "Integrating ASSPEGIQUE and LP", pages 69–85
  • Niels Mellergaard and Jørgen Staunstrup, "Generating proof obligations for circuits", pages 185–200
  • E. A. Scott and K. J. Norrie, "Using LP to study the language PL0+", pages 227–245
  • Frédéric Voisin, "A new front-end for the Larch Prover", pages 282–296
  • J. M. Wing, E. Rollins, and A. Moorman Zaremski, "Thoughts on a Larch/ML and a new application for LP", pages 297–312

Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli, and Nancy Lynch, Using simulated execution in verifying distributed algorithms," Software Tools for Technology Transfer 6:1, Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, and Supratik Mukhopadhyay (editors), pages 67–76. Springer-Verlag, July 2004.

Tsvetomir P. Petrov, Anya Pogosyants, Stephen J. Garland, Victor Luchangco, and Nancy A. Lynch, "Computer-assisted verification of an algorithm for concurrent timestamps," Formal Description Techniques IX: Theory, Application, and Tools (FORTE/PSTV), Reinhard Gotzhein and Jan Bredereke (editors), pages 29–44, Kaiserslautern, Germany, October 8–11, 1996. Chapman & Hall.

James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning, "Using transformations and verification in circuit design," Formal Methods in System Design 3:3 (December 1993), pages 181–209.

Jørgen F. Søgaard-Anderson, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, and Anya Pogosyants, "Computed-assisted simulation proofs," Fifth Conference on Computer-Aided Verification (CAV '03), Costas Courcoubetis (editor), Lecture Notes in Computer Science 697, pages 305–319, Elounda, Greece, June 1993. Springer-Verlag.

Jørgen Staunstrup, Stephen J. Garland, and John V. Guttag, "Localized verification of circuit descriptions," Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, pages 349–364, Grenoble, France, June 1989. Springer-Verlag.

Jørgen Staunstrup, Stephen J. Garland, and John V. Guttag, "Mechanized verification of circuit descriptions using the Larch Prover", Theorem Provers in Circuit Design, Victoria Stavridou, Thomas F. Melham, and Raymond T. Boute (editors), IFIP Transactions A-10, pages 277–299, Nijmegen, The Netherlands, June 22–24, 1992. North-Holland.

Mark T. Vandevoorde and Deepak Kapur, "Distributed Larch Prover (DLP): an experiment in parallelizing a rewrite-rule based prover", International Conference on Rewriting Techniques and Applications RTA 1996, Lecture Notes in Computer Science 1103, pages 420–423. Springer-Verlag.

Frédéric Voisin, "A new proof manager and graphic interface for the Larch prover", International Conference on Rewriting Techniques and Applications RTA 1996, Lecture Notes in Computer Science 1103, pages 408–411. Springer-Verlag.

Jeannette M. Wing and Chun Gong, Experience with the Larch Prover, ACM SIGSOFT Software Engineering Notes 15:44, September 1990, pages 140–143 https://doi.org/10.1145/99571.99835

References

  1. ↑ 1985 Larch survey, Çarnegie Mellon University
  2. ↑ John V. Guttag and James Horning with S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing, Larch: Languages and Tools for Formal Specification, Springer-Verlag Texts and Monographs in Computer Science, 1993. ISBN 978-1-4612-2704-5.
  3. ↑ Pierre Lescanne and "Computer experiments with the REVE term rewriting system generator," Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '83, Austin, Texas, Association for Computing Machinery, New York, NY, pages 99–108.
  4. ↑ Randy Forgaard and John Guttag, "REVE: a term rewriting system generator with a failure-resistant Knuth-Bendix", Proceedings of a Workshop on Term Rewriting, edited by D. Kapur and D. Musser, April 1984, pages 5–31.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.