Larch Prover
   HOME

TheInfoList



OR:

The Larch Prover, or LP for short, was an interactive
theorem In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of th ...
proving system for multi-sorted
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
. It was used at
MIT The Massachusetts Institute of Technology (MIT) is a private land-grant research university in Cambridge, Massachusetts. Established in 1861, MIT has played a key role in the development of modern technology and science, and is one of the m ...
and elsewhere during the 1990s to reason about designs for circuits, concurrent
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
s, hardware, and software. 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 John Vogel Guttag (born March 6, 1949) is an American computer scientist, professor, and former head of the department of Electrical Engineering and Computer Science at MIT. Education and career John Guttag was raised in Larchmont, New York, th ...
at the MIT Laboratory for Computer Science with assistance from James Horning and
James Saxe James is a common English language surname and given name: *James (name), the typically masculine first name James * James (surname), various people with the last name James James or James City may also refer to: People * King James (disambiguat ...
at the
DEC Systems Research Center The Systems Research Center (SRC) was a research laboratory created by Digital Equipment Corporation (DEC) in 1984, in Palo Alto, California. DEC SRC was founded by a group of computer scientists, led by Robert Taylor, who left the Computer ...
, as part of the Larch project on formal specifications. It extended the REVE 2 equational term
rewriting In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a well-formed formula, formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewr ...
system developed by Pierre Lescanne, Randy ForgaardRandy 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. with assistance from David Detlefs and
Katherine Yelick Katherine "Kathy" Anne Yelick is an American computer scientist, a professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley, and the Associate Laboratory Director for Computing Sciences at Lawrence Berk ...
. 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;
   = 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 
qed

prove \E x \A e (e \in x <=> e = e1 \/ e = e2)
  resume by specializing x to insert(e2, )
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

{{Reflist


External links


Larch website


Theorem proving software systems