Lärkprover

The Larch Prover , eller LP för kort, var ett interaktivt teorembevisande system för multi-sorterad första ordningens logik . Den användes vid MIT och på andra håll under 1990-talet för att resonera kring design för kretsar , samtidiga algoritmer , hårdvara och mjukvara.

Till skillnad från de flesta teorembevisare, som försöker hitta bevis automatiskt för korrekt angivna gissningar, var LP avsedd att hjälpa användare att hitta och korrigera brister i gissningar - den dominerande aktiviteten i de tidiga stadierna av designprocessen. Det fungerade effektivt på stora problem, hade många viktiga användarbekvämligheter och kunde användas av relativt naiva användare.

Utveckling

LP utvecklades av Stephen Garland och John Guttag vid MIT Laboratory for Computer Science med hjälp av James Horning och James Saxe vid DEC Systems Research Center , som en del av Larch-projektet om formella specifikationer . Den utökade REVE 2-systemet för ekvationell termomskrivning som utvecklats av Pierre Lescanne, Randy Forgaard med hjälp av David Detlefs och Katherine Yelick . Den stöder bevis genom ekvationell termomskrivning (för termer med associativ-kommutativa operatorer), fall, motsägelse, induktion, generalisering och specialisering.

LP skrevs i programmeringsspråket CLU .

Exempel på LP-axiomatisering 

deklarera sorterar E, S deklarerar variabler e, e1, e2: E, x, y, z: S deklarerar operatorer {}: -> S {__}: E -> S infoga: E, S -> S __ \union __ : S, S -> S __ \in __: E, S -> Bool __ \subseteq __: S, S -> Bool .. set namn setAxioms hävda sortera S genererad av {}, infoga; {e} = infoga(e, {}); ~(e \i {}); e \in infoga(e1, x) <=> e = e1 \/ e \in x; {} \subseteq x; infoga(e, x) \subseteq y <=> e \in y /\ x \subseteq y; e \in (x \union y) <=> e \in x \/ e \in y .. set namnförlängning hävda \A e (e \in x <=> e \in y) => x = y

Exempel på LP-prov 

set namn setTheorems bevisa e \in {e} qed bevisa \E x \A e (e \in x <=> e = e1 \/ e = e2) återuppta genom att specialisera x för att infoga(e2, {e1}) qed % Tre satser om union (bevisat med extensionalitet) bevisar x \union {} = x instansiera y med x \union {} i extensionalitet qed bevisa x \union insert(e, y) = infoga(e, x \union y) återuppta med motsägelseuppsättningsnamn lemma kritiska-par *Hyp med extensionalitet qed bevisa ac \union resume genom motsägelseuppsättningsnamn lemma kritiska-par *Hyp med extensionalitet CV genom motsägelseuppsättningsnamn lemma kritiska-par *Hyp med extensionalitet qed % Tre satser om delmängdsmängdsbevis -metoder =>, normalisering bevisa e \in x /\ x \subseteq y => e \in y genom induktion på x CV per case ec = e1c set namn lemma komplett qed bevisa x \subseteq y /\ y \subseteq x = > x = y set namn lemma bevisa e \in xc <=> e \in yc by <=> komplett fullständig instansiera x by xc, y by yc i extensionalitet qed bevisa (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z genom induktion på x qed % En alternativ induktionsregel bevisar sort S genererad av {}, {__}, \union set namn lemma CV genom induktion kritiska-par *GenHyp med *GenHyp kritiska-par *InductHyp med lemma qed

Bibliografi

Pascal André, Annya Romanczuk, Jean-Claude Royer och Aline Vasconcelos, "Kontrollera konsistensen av UML-klassdiagram med Larch Prover", Proceedings of the 2000 International Conference on Rigorous Object- Oriented Methods , sida 1, York, Storbritannien, BCS Learning & Development Ltd., Swindon, GBR, januari 2000.

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

Manfred Broy, "Erfarenheter med mjukvaruspecifikation och verifiering med LP, lärksäkra assistent", Formal Methods in System Design 8:3, sidorna 221–272, 1996.

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

Urban Engberg, Reasoning in the Temporal Logic of Actions , BRICS Dissertation Series DS 96–1, Institutionen för datavetenskap, Aarhus Universitet, Danmark, augusti 1996. ISSN 1396-7002.

Stephen J. Garland och John V. Guttag, "Induktiva metoder för resonemang om abstrakta datatyper," Femtonde årliga ACM Symposium on Principles of Programming Languages, sidorna 219–228, San Diego, CA, januari 1988.

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

Stephen J. Garland, John V. Guttag och Jørgen Staunstrup, "Verification of VLSI circuits using LP," The Fusion of Hardware Design and Verification , sidorna 329–345, Glasgow, Skottland, 4–6 juli 1988. IFIP WG 10.2 , Norra Holland.

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

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

Stephen J. Garland och John V. Guttag, A Guide to LP: the Larch Prover , MIT Laboratory for Computer Science, december 1991. Även publicerad som Digital Equipment Corporation Systems Research Center Report 82, 1991.

Victor Luchangco, Ekrem Söylemez, Stephen Garland och Nancy Lynch, "Verifying timing properties of concurrent algorithms," FORTE '94: Seventh International Conference on Formal Description Techniques , sidorna 259–273, Bern, Schweiz, 4–7 oktober 1994. Chapman & Hall.

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

Ursula Martin och Jeannette M. Wing, redaktörer, First International Workshop on Larch , Proceedings of the First International Workshop non Larch, Dedham, Massachusetts, 13–15 juli 1992, Workshops in Computing, Springer-Verlag, 1992.

  • Michel Bidoit och Rolf Hennicker, "Hur man bevisar observationssatser med LP", sidorna 18–35
  • Boutheina Chetali och Pierre Lescanne, "En övning i LP: beviset på en icke-återställande divisionskrets", sidorna 55–68
  • Christine Choppy och Michel Bidoit, "Integrating ASSPEGIQUE and LP", sidorna 69–85
  • Niels Mellergaard och Jørgen Staunstrup, "Generating proof obligations for circuits", sid 185–200
  • 0 EA Scott och KJ Norrie, "Using LP to study the language PL + ", sid 227–245
  • Frédéric Voisin, "A new front-end for the Larch Prover", sidorna 282–296
  • JM Wing, E. Rollins och A. Moorman Zaremski, "Thoughts on a Larch/ML and a new application for LP", sidorna 297–312

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

Tsvetomir P. Petrov, Anya Pogosyants, Stephen J. Garland, Victor Luchangco och Nancy A. Lynch, "Datorassisterad verifiering av en algoritm för samtidiga tidsstämplar," Formal Description Techniques IX: Theory, Application, and Tools (FORTE/PSTV) ) , Reinhard Gotzhein och Jan Bredereke (redaktörer), sidorna 29–44, Kaiserslautern, Tyskland, 8–11 oktober 1996. Chapman & Hall.

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

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

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

Jørgen Staunstrup, Stephen J. Garland och John V. Guttag, "Mechanized verification of circuit descriptions using the Larch Prover", Theorem Provers in Circuit Design , Victoria Stavridou, Thomas F. Melham och Raymond T. Boute (redaktörer), IFIP Transaktioner A-10 , sidorna 277–299, Nijmegen, Nederländerna, 22–24 juni 1992. North-Holland.

Mark T. Vandevoorde och 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, sidorna 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, sidorna 408–411. Springer-Verlag.

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

externa länkar

Hämtad från " https://en.wikipedia.org/w/index.php?title=Larch_Prover&oldid=1062700235 "