Probador de alerce

El Larch Prover , o LP para abreviar, es un sistema interactivo de demostración de teoremas para lógica de primer orden multisortada . Se utilizó en el MIT y en otros lugares durante la década de 1990 para razonar sobre diseños de circuitos , algoritmos concurrentes , hardware y software. ^{[ 1 ]}

A diferencia de la mayoría de los demostradores de teoremas, que intentan encontrar pruebas automáticamente para conjeturas correctamente formuladas, LP fue diseñado para ayudar a los usuarios a encontrar y corregir errores en las conjeturas , la actividad predominante en las primeras etapas del proceso de diseño. Funcionaba de manera eficiente con problemas grandes, contaba con muchas ventajas importantes para el usuario y podía ser utilizado por usuarios relativamente inexpertos.

LP fue desarrollado por Stephen Garland y John Guttag en el Laboratorio de Ciencias de la Computación del MIT con la asistencia de James Horning y James Saxe en el Centro de Investigación de Sistemas DEC , como parte del proyecto Larch sobre especificaciones formales . ^{[ 2 ]} Extendió el sistema de reescritura de términos ecuacionales REVE 2 desarrollado por Pierre Lescanne, ^{[ 3 ]} Randy Forgaard ^{[ 4 ]} con la asistencia de David Detlefs y Katherine Yelick . Admite demostraciones mediante reescritura de términos ecuacionales (para términos con operadores asociativos-conmutativos), casos, contradicción, inducción, generalización y especialización.

LP fue escrito en el lenguaje de programación CLU .

declarar tipos E, S declarar variables e, e1, e2: E, x, y, z: S declaran operadores {}: -> S {__}: E -> S insertar: E, S -> S __ \unión __: S, S -> S __ \in __: E, S -> Booleano __ \subseteq __: S, S -> Bool ... nombre del conjunto conjuntoAxiomas afirmar ordenar S generado por {}, insertar; {e} = insertar(e, {}); ~(e \in {}); e \in insert(e1, x) <=> e = e1 \/ e \in x; {} \subset x; insertar(e, x) \subseteq y <=> e \in y /\ x \subseteq y; e ∈ (x ∪ y) <=> e ∈ x / e ∈ y ... establecer extensión de nombre afirmar \A e (e \in x <=> e \in y) => x = y 

conjunto nombre conjuntoTeoremas demostrar e \in {e} qed probar \E x \A e (e \in x <=> e = e1 \/ e = e2) reanudar especializando x para insertar(e2, {e1}) qed % Tres teoremas sobre la unión (demostrados mediante la extensionalidad) demostrar x \union {} = x instanciar y por x \union {} en extensionalidad qed Demuestre que x ∪ insert(e, y) = insert(e, x ∪ y) reanudar por contradicción lema del nombre del conjunto pares críticos *Hipótesis con extensionalidad qed probar ac \unión reanudar por contradicción lema del nombre del conjunto pares críticos *Hipótesis con extensionalidad reanudar por contradicción lema del nombre del conjunto pares críticos *Hipótesis con extensionalidad qed % Tres teoremas sobre subconjuntos establecer métodos de prueba =>, normalización Demuestre por inducción sobre x que e ∈ x / x ∪ y => e ∈ y resumen por caso ec = e1c lema del nombre del conjunto completo qed demostrar que x ∪ y / y ∪ x => x = y lema del nombre del conjunto Demuestre que e \in xc <=> e \in yc mediante <=> completo completo Instanciar x mediante xc, y mediante yc en extensionalidad qed Demuestre que (x ∪ y) ⊆ z <=> x ⊆ z / y ⊆ z por inducción sobre x. qed % Una regla de inducción alternativa Demuestra el tipo S generado por {}, {__}, \union lema del nombre del conjunto currículum por inducción pares críticos *GenHyp con *GenHyp pares críticos *Inducción de Hipótesis con lema qed 

Pascal André, Annya Romanczuk, Jean-Claude Royer y Aline Vasconcelos, "Comprobación de la consistencia de los diagramas de clases UML mediante Larch Prover", Actas de la Conferencia Internacional de 2000 sobre Métodos Rigurosos Orientados a Objetos , página 1, York, Reino Unido, BCS Learning & Development Ltd., Swindon, GBR, enero de 2000.

Boutheina Chetali, "Verificación formal de programas concurrentes utilizando el probador Larch", IEEE Transactions on Software Engineering 24:1, páginas 46 – 62, enero de 1998. doi: 10.1109/32.663997.

Manfred Broy, "Experiencias con la especificación y verificación de software utilizando LP, el asistente de pruebas de Larch", Métodos formales en el diseño de sistemas 8:3, páginas 221 – 272, 1996.

Urban Engberg, Peter Grønning y Leslie Lamport, "Verificación mecánica de sistemas concurrentes con TLA", Verificación asistida por computadora , G. v. Bochmann y DK Probst editores, Actas de la Cuarta Conferencia Internacional CAV'92), Lecture Notes in Computer Science 663, Springer-Verlag, junio de 1992, páginas 44-55 .

Urban Engberg, Razonamiento en la lógica temporal de las acciones , Serie de tesis doctorales BRICS DS 96 – 1, Departamento de Ciencias de la Computación, Universidad de Aarhus, Dinamarca, agosto de 1996. ISSN 1396-7002.

Stephen J. Garland y John V. Guttag, "Métodos inductivos para razonar sobre tipos de datos abstractos", Decimoquinto Simposio Anual de la ACM sobre Principios de Lenguajes de Programación , páginas 219-228 , San Diego, California, enero de 1988.

Stephen J. Garland y John V. Guttag, "LP: The Larch Prover", Novena Conferencia Internacional sobre Deducción Automatizada, Notas de Clase en Ciencias de la Computación 310, páginas 748-749 , Argonne, Illinois, mayo de 1988. Springer-Verlag.

Stephen J. Garland, John V. Guttag y Jørgen Staunstrup, "Verificación de circuitos VLSI mediante LP", The Fusion of Hardware Design and Verification , páginas 329-345, Glasgow, Escocia, 4-6 de julio de 1988. IFIP WG 10.2, Holanda Septentrional.

Stephen J. Garland y John V. Guttag, "Una visión general de LP, el probador Larch", Tercera Conferencia Internacional sobre Técnicas y Aplicaciones de Reescritura, Notas de clase en Ciencias de la Computación 355, páginas 137-151 , Chapel Hill, Carolina del Norte, abril de 1989. Springer-Verlag.

Stephen J. Garland y John V. Guttag, "Uso de LP para depurar especificaciones", Conceptos y métodos de programación , Mar de Galilea, Israel, 2-5 de abril de 1990. IFIP WG 2.2/2.3, North-Holland.

Stephen J. Garland y John V. Guttag, Guía de LP: el probador Larch , Laboratorio de Ciencias de la Computación del MIT, diciembre de 1991. También publicado como Informe 82 del Centro de Investigación de Sistemas de Digital Equipment Corporation, 1991.

Victor Luchangco, Ekrem Söylemez, Stephen Garland y Nancy Lynch, "Verificación de las propiedades de temporización de algoritmos concurrentes", FORTE '94: Séptima Conferencia Internacional sobre Técnicas de Descripción Formal , páginas 259-273, Berna, Suiza, 4-7 de octubre de 1994. Chapman & Hall.

Ursula Martin y Michael Lai, "Algunos experimentos con un demostrador de teoremas de completitud", Journal of Symbolic Computation 13:1, 1992, páginas 81-100 , ISSN 0747-7171.

Ursula Martin y Jeannette M. Wing, editoras, Primer Taller Internacional sobre Larch , Actas del Primer Taller Internacional sobre Larch, Dedham, Massachusetts, 13-15 de julio de 1992 , Workshops in Computing, Springer-Verlag, 1992.

• Michel Bidoit y Rolf Hennicker, "Cómo demostrar teoremas observacionales con programación lineal", páginas 18-35
• Boutheina Chetali y Pierre Lescanne, "Un ejercicio de programación lineal: la demostración de un circuito de división no restaurador", páginas 55-68 .
• Christine Choppy y Michel Bidoit, "Integrando ASSPEGIQUE y LP", páginas 69-85
• Niels Mellergaard y Jørgen Staunstrup, "Generación de obligaciones de prueba para circuitos", páginas 185 – 200
• EA Scott y KJ Norrie, "Uso de LP para estudiar el lenguaje PL ₀ ⁺ ", páginas 227-245
• Frédéric Voisin, "Una nueva interfaz para el Larch Prover", páginas 282-296
• JM Wing, E. Rollins y A. Moorman Zaremski, "Reflexiones sobre un alerce/ML y una nueva aplicación para LP", páginas 297-312

Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli y Nancy Lynch, "Uso de la ejecución simulada en la verificación de algoritmos distribuidos", Software Tools for Technology Transfer 6:1, Lenore D. Zuck , Paul C. Attie, Agostino Cortesi y Supratik Mukhopadhyay (editores), páginas 67-76 . Springer-Verlag, julio de 2004.

Tsvetomir P. Petrov, Anya Pogosyants, Stephen J. Garland, Victor Luchangco y Nancy A. Lynch, "Verificación asistida por computadora de un algoritmo para marcas de tiempo concurrentes", Formal Description Techniques IX: Theory, Application, and Tools (FORTE/PSTV) , Reinhard Gotzhein y Jan Bredereke (editores), páginas 29-44 , Kaiserslautern, Alemania, 8-11 de octubre de 1996. Chapman & Hall.

James B. Saxe, Stephen J. Garland, John V. Guttag y James J. Horning, "Uso de transformaciones y verificación en el diseño de circuitos", Métodos formales en el diseño de sistemas 3:3 (diciembre de 1993), páginas 181-209 .

Jørgen F. Søgaard-Anderson, Stephen J. Garland, John V. Guttag, Nancy A. Lynch y Anya Pogosyants, "Pruebas de simulación asistidas por computadora", Quinta Conferencia sobre Verificación Asistida por Computadora (CAV '03) , Costas Courcoubetis (editor), Lecture Notes in Computer Science 697, páginas 305-319 , Elounda, Grecia, junio de 1993. Springer-Verlag.

Jørgen Staunstrup, Stephen J. Garland y John V. Guttag, "Verificación localizada de descripciones de circuitos", Métodos de verificación automática para sistemas de estados finitos , Lecture Notes in Computer Science 407, páginas 349-364 , Grenoble, Francia, junio de 1989. Springer-Verlag.

Jørgen Staunstrup, Stephen J. Garland y John V. Guttag, "Verificación mecanizada de descripciones de circuitos utilizando el probador Larch", Theorem Provers in Circuit Design , Victoria Stavridou, Thomas F. Melham y Raymond T. Boute (editores), IFIP Transactions A-10 , páginas 277-299 , Nijmegen, Países Bajos, 22-24 de junio de 1992. North-Holland.

Mark T. Vandevoorde y Deepak Kapur, "Distributed Larch Prover (DLP): un experimento para paralelizar un probador basado en reglas de reescritura", Conferencia Internacional sobre Técnicas y Aplicaciones de Reescritura RTA 1996 , Lecture Notes in Computer Science 1103, páginas 420-423 . Springer-Verlag.

Frédéric Voisin, "Un nuevo gestor de pruebas e interfaz gráfica para el probador Larch", Conferencia Internacional sobre Técnicas y Aplicaciones de Reescritura RTA 1996 , Lecture Notes in Computer Science 1103, páginas 408-411 . Springer-Verlag.

Jeannette M. Wing y Chun Gong, Experiencia con el probador Larch, ACM SIGSOFT Software Engineering Notes 15:44, septiembre de 1990, páginas 140-143 https://doi.org/10.1145/99571.99835

• Sitio web de Larch
• Documentación en línea para LP