Ayuda rapida Comandos PVS PDF

Preview

Summary

Guía de comandos PVS...

Description

Comandos b´ asicos de PVS Gilberto P´erez, Concepci´on Mart´ın, Felicidad Aguado

Grupo IRlab Departamento de Computaci´on Universidade da Coru˜ na 22 de julio de 2017

´Indice

Introducci´ on a PVS

1.

IRlab

Botiqu´ın de primeros auxilios

Esto no es m´as que un peque˜ no resumen de algunos comandos de PVS. Una documentaci´ on m´as completa se puede encontrar en http : //pvs.csl.sri.com/documentation.shtml .

1.1.

´ Ordenes de prueba emacs

Como PVS se ejecuta en el editor de texto Emacs, es necesario conocer algunos comandos de este editor. M-x parse (pa) Realiza an´alisis sint´ actico de la teor´ıa. M-x prove (pr) Inicia una prueba. Al posicionar el cursor encima de una conjetura, teorema, etc, se inicia la prueba de dicha proposici´on. Sobre una proposici´on ya probada PVS nos pregunta si queremos volver a intentar la prueba; en caso afirmativo, pregunta si queremos ejecutar la prueba existente, en otro caso devuelve el prompt “Rule?” para intentarla de nuevo. M-x tccs Visualiza las TCCs (Type-Correctness Conditions). M-x exit-pvs Sale de PVS. C-c C-c Interrumpe cualquier proceso que se est´e llevando a cabo. Es interesante su uso cuando se utiliza un comando de prueba que provoca una entrada en un bucle infinito. A continuaci´on, mediante (restore), se regresa a la situaci´on en la que se estaba antes de iniciar el proceso interrumpido. M-x help-pvs-prover Ayuda para utilizar los comandos de prueba. M-x change-context Cambia de directorio. M-x typecheck (tc), (C-c C-t) Realiza un an´alisis sem´antico de tipos. M-x typecheck-prove (tcp) Intenta probar las TCCs generadas. Es recomendable realizar esta comprobaci´on de manera habitual al ir modificando la teor´ıa, ya que las TCCs no probadas tras invocar este comando pueden sugerir errores o deficiencias en la teor´ıa. M-x new-pvs-file (nf ) Crea un nuevo fichero PVS. M-x import-pvs-file (imf ) Importa un fichero PVS. M-x whereis-pvs Busca el directorio ra´ız donde est´a instalado el sistema. M-x find-pvs-file (ff ), (C-c C-f ) Busca un fichero PVS. M-x view-prelude-file (vpf ) Muestra la librer´ıa “prelude” entera (prelude = conjunto de librer´ıas cargadas por defecto). M-x view-prelude-theory (vpt) Permite ver una teor´ıa concreta del preludio, es decir, ver sus definiciones, teoremas etc. Solicita el nombre de la teor´ıa a ver, por ejemplo, “set”. M-x x-show-proof Genera el grafo del ´arbol de prueba. Se puede grabar como un fichero. M-x status-proof-theory (spt) Muestra las f´ormulas y TCCs de una teor´ıa y su estado de prueba.

3

Introducci´ on a PVS

IRlab

M-x status-proofchain (spc) Dada una f´ormula indica su estado (probada o no) y las dependencias de prueba, es decir, qu´e otras f´ormulas, principios de inducci´on, etc. se han utilizado para la prueba. M-x prove-theory (prt) Reproduce de forma autom´atica las pruebas ya realizadas.

1.2.

Comandos del probador

Generalmente estos comandos se aplican a f´ ormulas etiquetadas por n´umeros (abreviadas por fnums en la documentaci´on de PVS), que si son positivos indican una meta y negativos una hip´otesis. Otras posibles etiquetas son +, indica todas las metas; −, todas las hip´otesis y ∗ todas las metas y todas las hip´ otesis. Los comandos tambi´en se pueden aplicar a t´erminos (una expresi´on del secuente en curso, entre comillas). (quit)

Abandona el asistente de prueba sin terminar la prueba en curso

(undo)

Vuelve hacia atr´ as en la prueba

(grind)

Utiliza repetidamente reescritura y simplificaci´on (estrategia). Cuidado con su uso, a veces entra en bucle y colapsa el asistente de prueba

(ground)

Procedimiento de decisi´on/simplificaci´on descafeinado del estilo de grind, pero no diverge nunca

(f latten)

Simplifica el secuente de prueba. Reglas: ⊢ ∨, ⇔ ⊢, ∧ ⊢ y ⊢ ⇒

(split)

Divide la meta en dos submetas. Reglas: ∨ ⊢, ⊢ ⇔, ⊢ ∧ y ⇒ ⊢

(case ′′ A′′ )

Aplica la regla de prueba por casos

(induct ”n”)

Aplica inducci´ on sobre la variable “n”. La f´ormula sobre la que se aplica debe estar en el consecuente y universalmente cuantificada

(inst f num &REST terms)

Instancia las variables cuantificadas ∀ ⊢, ⊢ ∃ por t´erminos concretos

(skolem f nums constantes)

Skolemiza las variable cuantificadas ⊢ ∀, ∃ ⊢

(lif t − if &OP T ION AL f nums)

Simplifica los IF

(expand nombre − f uncion)

Expande las definiciones

(lemma nombre − lema)

Introduce un lema en las hip´otesis

(replace f num &OP T IONAL f nums)

2. 2.1.

Reescribe f´ormulas utilizando la igualdad l = r

Un poco m´ as lejos ... o m´ as r´ apido Comandos emacs

M-x step-proof Lanza una prueba ya realizada, paso a paso. M-x x-prover-commands Lista los comandos del probador. 4

Introducci´ on a PVS

IRlab

M-x show-hidden-formulas Visualiza las f´ormulas encubiertas por el usuario. M-x prettyprint-expanded Crea un buffer nuevo en el que se muestra la teor´ıa completa, incluyendo las tccs generadas, conversiones... etc M-x show-last-proof Muestra una versi´on abreviada de la u ´ltima prueba completada. Muestra los secuentes que se van generando y los comentarios producidos por la aplicaci´on de comandos de prueba. M-x prove-importchain Reproduce de forma autom´atica todas las pruebas, tanto de la teor´ıa que se est´a considerando, como de aquellas otras teor´ıas de las que depende. Tras esto, se obtiene un sumario con el estado de cada prueba. M-x latex-theory Genera c´odigo latex para la teor´ıa dada.

2.2.

Comandos del probador de PVS (postpone) (assert) (prop ) (hide fnun) (name nombre expr ) (reveal fnum) (typepred expr ) (apply-extensionnality) (skosimp )

2.3.

Navega entre las metas de una prueba Realiza simplificaciones l´ogicas de f´ormulas e igualdades Resuelve f´ormulas proposicionales simplificando los secuentes Oculta las f´ormulas indicadas del secuente Introduce un nuevo nombre para una expresi´on, a˜ nadiendo una f´ormula en el antecedente del secuente Recupera f´ormulas escondidas (M-x show-hidden-formulas) Explicita las restricciones de tipo de una expresi´on Aplica el principio de extensionalidad para record, tuplas y funciones Utiliza las los comandos Flatten + skolem (skeep)

Importar / Exportar teor´ıas

Se importan teor´ıas mediante IMPORTING. Las declaraciones de IMPORTING se incluyen dentro de la definici´on de la teor´ıa IMPORTING series@series, reals@sqrt, series@power_series En caso de teor´ıas parametrizadas PVS es capaz de resolver los par´ametros de la teor´ıa importada.

2.4.

Estructuras de las pruebas de PVS

Durante el curso de una prueba, PVS genera un ´arbol de secuentes, donde cada secuente es una submeta generado a partir de su secuente padre por un comando de prueba PVS. Durante la realizaci´on de una prueba el control se encuentra en una hoja de dicho ´arbol de prueba. Un comando de prueba PVS puede: Pasar al siguiente secuente de prueba en el ´arbol (postpone)

5

Introducci´ on a PVS

IRlab

Deshacer un sub´arbol y retroceder a un secuente padre (undo) Probar la submeta (secuente) actual y pasar a la siguiente submeta. Generar nuevas submetas y pasar el control a la primera de ellas. No modificar el ´arbol de prueba pero proporcionar informaci´on del estado de prueba. Una prueba se completa cuando ya no quedan secuentes-hoja sin probar en el a´rbol de prueba. La prueba resultante se puede grabar/salvar, puede ser editada y re-ejecutada sobre la misma conjetura o sobre otra conjetura.

2.5.

“Comandos inapropiados”

Si durante una prueba aplicamos un comando “inapropiado”, es decir, que no se puede aplicar, PVS nos informa de ello y devuelve la misma submeta. ... Rule? (split) No change on: (split) ...

Referencias [1] http://pvs.csl.sri.com [2] Sam Owre, Nataranjan Shankarm Hohn M. Rushby, and David W. J. Stringer-Calvert. PVS Prover Guide. SRI International, 2001. Version 2.4. http://pvs.csl.sri.com/doc/pvs-proverguide.pdf [3] Emacs. http://www.gnu.org/software/emacs/

6...