Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre...
Transcript of Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre...
![Page 1: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/1.jpg)
Un Método Práctico para Razonar sobreProcedimientos en la Programación Basada en
Invariantes
Brian Plüss
Director
Prof. Ralph-Johan BackCo-Director
Johannes Eriksson
Departamento de Ciencias de la ComputaciónFacultad de Ciencias Exactas, Ingeniería y Agrimensura
Universidad Nacional de Rosario
15 de septiembre de 2008
![Page 2: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/2.jpg)
Contenidos
1 IntroducciónMotivaciónDescripción del ProblemaProgramación Basada en Invariantes
2 ProcedimientosDeclaraciónContrato FormalMúltiples Salidas
3 Llamadas a ProcedimientoLlamadas de Única SalidaLlamadas de Múltiples SalidasLlamadas a en IBP
4 Recursión y TerminaciónLlamadas RecursivasRecursión SimpleRecursión Mutua
5 Conclusiones y Trabajos Futuros
![Page 3: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/3.jpg)
Motivación I
�We envision a world in which computer programs are always the most
reliable component of any system or device that contains them�
Hoare & Misra
Veri�cación Formal de Programas
Demostrar con precisión matemática que un programa es correctorespecto de su especi�cación.
En programación imperativa esto es vincular dos cosas:
Programa
Código que modi�ca el estado
←−−→
Especi�cación
Lógica sobre el estado
![Page 4: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/4.jpg)
Motivación I
�We envision a world in which computer programs are always the most
reliable component of any system or device that contains them�
Hoare & Misra
Veri�cación Formal de Programas
Demostrar con precisión matemática que un programa es correctorespecto de su especi�cación.
En programación imperativa esto es vincular dos cosas:
Programa
Código que modi�ca el estado
←−−→
Especi�cación
Lógica sobre el estado
![Page 5: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/5.jpg)
Motivación I
�We envision a world in which computer programs are always the most
reliable component of any system or device that contains them�
Hoare & Misra
Veri�cación Formal de Programas
Demostrar con precisión matemática que un programa es correctorespecto de su especi�cación.
En programación imperativa esto es vincular dos cosas:
Programa
Código que modi�ca el estado
←−−→
Especi�cación
Lógica sobre el estado
![Page 6: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/6.jpg)
Motivación I
�We envision a world in which computer programs are always the most
reliable component of any system or device that contains them�
Hoare & Misra
Veri�cación Formal de Programas
Demostrar con precisión matemática que un programa es correctorespecto de su especi�cación.
En programación imperativa esto es vincular dos cosas:
Programa
Código que modi�ca el estado←−−→
Especi�cación
Lógica sobre el estado
![Page 7: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/7.jpg)
Motivación I
�We envision a world in which computer programs are always the most
reliable component of any system or device that contains them�
Hoare & Misra
Veri�cación Formal de Programas
Demostrar con precisión matemática que un programa es correctorespecto de su especi�cación.
En programación imperativa esto es vincular dos cosas:
Programa
Código que modi�ca el estado←−−→
Especi�cación
Lógica sobre el estado
![Page 8: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/8.jpg)
Motivación II
Tres enfoques de veri�cación:
A Posteriori
Difícil y costoso
Invariantescomplejos
Conocimientoperdido
Por Construcción
Invariantescomplejos
Basada en Invariantes
¾Es escalable?
Empecemos por losprocedimientos...
![Page 9: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/9.jpg)
Motivación II
Tres enfoques de veri�cación:
A Posteriori
Difícil y costoso
Invariantescomplejos
Conocimientoperdido
Por Construcción
Invariantescomplejos
Basada en Invariantes
¾Es escalable?
Empecemos por losprocedimientos...
![Page 10: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/10.jpg)
Motivación II
Tres enfoques de veri�cación:
A Posteriori
Difícil y costoso
Invariantescomplejos
Conocimientoperdido
Por Construcción
Invariantescomplejos
Basada en Invariantes
¾Es escalable?
Empecemos por losprocedimientos...
![Page 11: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/11.jpg)
Motivación II
Tres enfoques de veri�cación:
A Posteriori
Difícil y costoso
Invariantescomplejos
Conocimientoperdido
Por Construcción
Invariantescomplejos
Basada en Invariantes
¾Es escalable?
Empecemos por losprocedimientos...
![Page 12: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/12.jpg)
Motivación II
Tres enfoques de veri�cación:
A Posteriori
Difícil y costoso
Invariantescomplejos
Conocimientoperdido
Por Construcción
Invariantescomplejos
Basada en Invariantes
¾Es escalable?
Empecemos por losprocedimientos...
![Page 13: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/13.jpg)
Motivación II
Tres enfoques de veri�cación:
A Posteriori
Difícil y costoso
Invariantescomplejos
Conocimientoperdido
Por Construcción
Invariantescomplejos
Basada en Invariantes
¾Es escalable?
Empecemos por losprocedimientos...
![Page 14: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/14.jpg)
Motivación II
Tres enfoques de veri�cación:
A Posteriori
Difícil y costoso
Invariantescomplejos
Conocimientoperdido
Por Construcción
Invariantescomplejos
Basada en Invariantes
¾Es escalable?
Empecemos por losprocedimientos...
![Page 15: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/15.jpg)
Motivación II
Tres enfoques de veri�cación:
A Posteriori
Difícil y costoso
Invariantescomplejos
Conocimientoperdido
Por Construcción
Invariantescomplejos
Basada en Invariantes
¾Es escalable?
Empecemos por losprocedimientos...
![Page 16: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/16.jpg)
Programación Basada en Invariantes (IBP)+ Procedimientos
IBP
Formalismo visual, soportadopor el cálculo de re�namientos.
Los invariantes se escribenprimero y el código seestructura alrededor.
Sin reglas de prueba complejas:las condiciones de veri�caciónse leen del diagrama.
Corrección total (incluyendoterminación).
+
Procedimientos
Abstracción y reutilización.
Pero acarrean complejidadsemántica.
Recursión simple y recursiónmutua.
Pero podrían no terminar.
Manejo de excepciones.
Pero tendrán variaspostcondiciones.
![Page 17: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/17.jpg)
Programación Basada en Invariantes (IBP)+ Procedimientos
IBP
Formalismo visual, soportadopor el cálculo de re�namientos.
Los invariantes se escribenprimero y el código seestructura alrededor.
Sin reglas de prueba complejas:las condiciones de veri�caciónse leen del diagrama.
Corrección total (incluyendoterminación).
+
Procedimientos
Abstracción y reutilización.
Pero acarrean complejidadsemántica.
Recursión simple y recursiónmutua.
Pero podrían no terminar.
Manejo de excepciones.
Pero tendrán variaspostcondiciones.
![Page 18: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/18.jpg)
Programación Basada en Invariantes (IBP)+ Procedimientos
IBP
Formalismo visual, soportadopor el cálculo de re�namientos.
Los invariantes se escribenprimero y el código seestructura alrededor.
Sin reglas de prueba complejas:las condiciones de veri�caciónse leen del diagrama.
Corrección total (incluyendoterminación).
+
Procedimientos
Abstracción y reutilización.
Pero acarrean complejidadsemántica.
Recursión simple y recursiónmutua.
Pero podrían no terminar.
Manejo de excepciones.
Pero tendrán variaspostcondiciones.
![Page 19: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/19.jpg)
Programación Basada en Invariantes IEjemplo.
Replace
Dados un arreglo de enteros a y enteros x e y, reemplaza todas lasocurrencias de x en a por y, contando los cambios en n.
Elementos de IBP
Scope.
Constantes y de�niciones.Variables.
Situaciones.
Anidamiento.Iniciales y �nales.Variante.
Transiciones.
Sentencias.Salidas simples y múltiples.Selección y guardas.
![Page 20: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/20.jpg)
Programación Basada en Invariantes IEjemplo.
Replace
Dados un arreglo de enteros a y enteros x e y, reemplaza todas lasocurrencias de x en a por y, contando los cambios en n.
Elementos de IBP
Scope.
Constantes y de�niciones.Variables.
Situaciones.
Anidamiento.Iniciales y �nales.Variante.
Transiciones.
Sentencias.Salidas simples y múltiples.Selección y guardas.
![Page 21: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/21.jpg)
Programación Basada en Invariantes IEjemplo.
Replace
Dados un arreglo de enteros a y enteros x e y, reemplaza todas lasocurrencias de x en a por y, contando los cambios en n.
Elementos de IBP
Scope.
Constantes y de�niciones.Variables.
Situaciones.
Anidamiento.Iniciales y �nales.Variante.
Transiciones.
Sentencias.Salidas simples y múltiples.Selección y guardas.
![Page 22: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/22.jpg)
Programación Basada en Invariantes IISintáxis.
Las transiciones están etiquetadas con sentencias que operan sobreel estado del programa:
S ::= skip identidad| abort terminación incondicional (falla)| x1,...,xm:=v1, ...,vm asignación| S0;S1 composición| [b] asunción| {b} aserción| S1u ...uSm selección no determinista
![Page 23: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/23.jpg)
Programación Basada en Invariantes IIISemántica.
Existe una semántica operacional, pero no nos interesa.
La corrección total se de�ne en términos del transformador depredicados de la precondición más débil (Dijkstra '60s).
Una función wp que relaciona sentencias con predicados sobreel estado:
wp(skip,q) = q
wp(abort,q) = false
wp(x1, ...,xm := v1, ...,vm,q) = q[x1, ...,xm := v1, ...,vm]
wp(S0;S1,q) = wp(S0,wp(S1,q))
wp([b],q) = b⇒ q
wp({b},q) = b∧qwp(S1 u ...uSm,q) = wp(S1,q)∧ ...∧wp(Sm,q)
Propiedades
Si Q⇒R, entonceswp(S,Q)⇒wp(S,R)
wp(S,Q)∧wp(S,R) =wp(S,Q ∧R)
wp(S,Q)∨wp(S,R)⇒wp(S,Q ∨R) (=, si Sdeterminista)
P ⇒ wp(S ,Q)≡ {P}S{Q} + terminación
![Page 24: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/24.jpg)
Programación Basada en Invariantes IIISemántica.
Existe una semántica operacional, pero no nos interesa.
La corrección total se de�ne en términos del transformador depredicados de la precondición más débil (Dijkstra '60s).
Una función wp que relaciona sentencias con predicados sobreel estado:
wp(skip,q) = q
wp(abort,q) = false
wp(x1, ...,xm := v1, ...,vm,q) = q[x1, ...,xm := v1, ...,vm]
wp(S0;S1,q) = wp(S0,wp(S1,q))
wp([b],q) = b⇒ q
wp({b},q) = b∧qwp(S1 u ...uSm,q) = wp(S1,q)∧ ...∧wp(Sm,q)
Propiedades
Si Q⇒R, entonceswp(S,Q)⇒wp(S,R)
wp(S,Q)∧wp(S,R) =wp(S,Q ∧R)
wp(S,Q)∨wp(S,R)⇒wp(S,Q ∨R) (=, si Sdeterminista)
P ⇒ wp(S ,Q)≡ {P}S{Q} + terminación
![Page 25: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/25.jpg)
Programación Basada en Invariantes IIISemántica.
Existe una semántica operacional, pero no nos interesa.
La corrección total se de�ne en términos del transformador depredicados de la precondición más débil (Dijkstra '60s).
Una función wp que relaciona sentencias con predicados sobreel estado:
wp(skip,q) = q
wp(abort,q) = false
wp(x1, ...,xm := v1, ...,vm,q) = q[x1, ...,xm := v1, ...,vm]
wp(S0;S1,q) = wp(S0,wp(S1,q))
wp([b],q) = b⇒ q
wp({b},q) = b∧qwp(S1 u ...uSm,q) = wp(S1,q)∧ ...∧wp(Sm,q)
Propiedades
Si Q⇒R, entonceswp(S,Q)⇒wp(S,R)
wp(S,Q)∧wp(S,R) =wp(S,Q ∧R)
wp(S,Q)∨wp(S,R)⇒wp(S,Q ∨R) (=, si Sdeterminista)
P ⇒ wp(S ,Q)≡ {P}S{Q} + terminación
![Page 26: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/26.jpg)
Programación Basada en Invariantes IIISemántica.
Existe una semántica operacional, pero no nos interesa.
La corrección total se de�ne en términos del transformador depredicados de la precondición más débil (Dijkstra '60s).
Una función wp que relaciona sentencias con predicados sobreel estado:
wp(skip,q) = q
wp(abort,q) = false
wp(x1, ...,xm := v1, ...,vm,q) = q[x1, ...,xm := v1, ...,vm]
wp(S0;S1,q) = wp(S0,wp(S1,q))
wp([b],q) = b⇒ q
wp({b},q) = b∧qwp(S1 u ...uSm,q) = wp(S1,q)∧ ...∧wp(Sm,q)
Propiedades
Si Q⇒R, entonceswp(S,Q)⇒wp(S,R)
wp(S,Q)∧wp(S,R) =wp(S,Q ∧R)
wp(S,Q)∨wp(S,R)⇒wp(S,Q ∨R) (=, si Sdeterminista)
P ⇒ wp(S ,Q)≡ {P}S{Q} + terminación
![Page 27: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/27.jpg)
Programación Basada en Invariantes IVVeri�cación.
Veri�cación en IBP
Corrección Total = Consistencia + Vitalidad + Terminación
Consistencia: una transición de I1 a I2 etiquetada con S es consistentesii I1⇒ wp(S , I2)
Vitalidad: una situación no terminal I está viva sii I implica ladisyunción de las guardas
Terminación: un diagrama termina si en cada ciclo ninguna transiciónincrementa el variante y al menos una lo decrementa
![Page 28: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/28.jpg)
Programación Basada en Invariantes IVVeri�cación.
Veri�cación en IBP
Corrección Total = Consistencia + Vitalidad + Terminación
Consistencia: una transición de I1 a I2 etiquetada con S es consistentesii I1⇒ wp(S , I2)
Vitalidad: una situación no terminal I está viva sii I implica ladisyunción de las guardas
Terminación: un diagrama termina si en cada ciclo ninguna transiciónincrementa el variante y al menos una lo decrementa
![Page 29: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/29.jpg)
Programación Basada en Invariantes IVVeri�cación.
Veri�cación en IBP
Corrección Total = Consistencia + Vitalidad + Terminación
Consistencia: una transición de I1 a I2 etiquetada con S es consistentesii I1⇒ wp(S , I2)
Vitalidad: una situación no terminal I está viva sii I implica ladisyunción de las guardas
Terminación: un diagrama termina si en cada ciclo ninguna transiciónincrementa el variante y al menos una lo decrementa
![Page 30: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/30.jpg)
Programación Basada en Invariantes IVVeri�cación.
Veri�cación en IBP
Corrección Total = Consistencia + Vitalidad + Terminación
Consistencia: una transición de I1 a I2 etiquetada con S es consistentesii I1⇒ wp(S , I2)
Vitalidad: una situación no terminal I está viva sii I implica ladisyunción de las guardas
Terminación: un diagrama termina si en cada ciclo ninguna transiciónincrementa el variante y al menos una lo decrementa
![Page 31: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/31.jpg)
Contenidos
1 IntroducciónMotivaciónDescripción del ProblemaProgramación Basada en Invariantes
2 ProcedimientosDeclaraciónContrato FormalMúltiples Salidas
3 Llamadas a ProcedimientoLlamadas de Única SalidaLlamadas de Múltiples SalidasLlamadas a en IBP
4 Recursión y TerminaciónLlamadas RecursivasRecursión SimpleRecursión Mutua
5 Conclusiones y Trabajos Futuros
![Page 32: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/32.jpg)
Procedimientos en IBP IEjemplo.
Replace
Replace hecho procedimiento.
Observaciones
Signatura.
Clasi�cadores.
Contrato.
Pre y Post(s).Condición de marco.Recursión y progreso.
Asignación implícita paravalores iniciales.
Contornos.
![Page 33: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/33.jpg)
Procedimientos en IBP IEjemplo.
Replace
Replace hecho procedimiento.
Observaciones
Signatura.
Clasi�cadores.
Contrato.
Pre y Post(s).Condición de marco.Recursión y progreso.
Asignación implícita paravalores iniciales.
Contornos.
![Page 34: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/34.jpg)
Procedimientos en IBP IEjemplo.
Replace
Replace hecho procedimiento.
Observaciones
Signatura.
Clasi�cadores.
Contrato.
Pre y Post(s).Condición de marco.Recursión y progreso.
Asignación implícita paravalores iniciales.
Contornos.
![Page 35: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/35.jpg)
Procedimientos en IBP IIContrato Formal.
De�nición
El contrato formal de un procedimiento está dado por su nombre, susignatura y la especi�cación en términos de pre- y postcondiciones,condiciones de marco y expresiones de progreso o recursión.
Contrato formal para Replace
Los parámetros resultado y las constantes de valor inicial paraparámetros valor-resultado (e.g. a0) no pueden aparecer en laprecondición.
Transparency requirement para parámetros valor.
![Page 36: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/36.jpg)
Procedimientos en IBP IIContrato Formal.
De�nición
El contrato formal de un procedimiento está dado por su nombre, susignatura y la especi�cación en términos de pre- y postcondiciones,condiciones de marco y expresiones de progreso o recursión.
Contrato formal para Replace
Los parámetros resultado y las constantes de valor inicial paraparámetros valor-resultado (e.g. a0) no pueden aparecer en laprecondición.
Transparency requirement para parámetros valor.
![Page 37: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/37.jpg)
Procedimientos en IBP IIContrato Formal.
De�nición
El contrato formal de un procedimiento está dado por su nombre, susignatura y la especi�cación en términos de pre- y postcondiciones,condiciones de marco y expresiones de progreso o recursión.
Contrato formal para Replace
Los parámetros resultado y las constantes de valor inicial paraparámetros valor-resultado (e.g. a0) no pueden aparecer en laprecondición.
Transparency requirement para parámetros valor.
![Page 38: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/38.jpg)
Procedimientos en IBP IIIMúltiples Salidas.
De�nición
Un procedimiento de múltiples salidas es uno que puede teminar en unade un conjunto de posibles postcondiciones.
Replace
Variación de Replace donde la ausencia de x en elarreglo original es considerada un caso excepcional.
![Page 39: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/39.jpg)
Procedimientos en IBP IIIMúltiples Salidas.
De�nición
Un procedimiento de múltiples salidas es uno que puede teminar en unade un conjunto de posibles postcondiciones.
Replace
Variación de Replace donde la ausencia de x en elarreglo original es considerada un caso excepcional.
![Page 40: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/40.jpg)
Contenidos
1 IntroducciónMotivaciónDescripción del ProblemaProgramación Basada en Invariantes
2 ProcedimientosDeclaraciónContrato FormalMúltiples Salidas
3 Llamadas a ProcedimientoLlamadas de Única SalidaLlamadas de Múltiples SalidasLlamadas a en IBP
4 Recursión y TerminaciónLlamadas RecursivasRecursión SimpleRecursión Mutua
5 Conclusiones y Trabajos Futuros
![Page 41: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/41.jpg)
Llamadas a Procedimiento IÚnica Salida. Sintaxis.
Extendemos las sentencias:
S ::= skip identidad| abort terminación incondicional (falla)
...| P(a1, ...,am) llamada a de única salida
Los parámetros actuales deben coincidir en número y tipo con losformales.
Expresiones para parámetros valor, variables para resultado yvalor-resultado.
Nonaliasing requirement para parámetros resultado yvalor-resultado.
![Page 42: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/42.jpg)
Llamadas a Procedimiento IÚnica Salida. Sintaxis.
Extendemos las sentencias:
S ::= skip identidad| abort terminación incondicional (falla)
...| P(a1, ...,am) llamada a de única salida
Los parámetros actuales deben coincidir en número y tipo con losformales.
Expresiones para parámetros valor, variables para resultado yvalor-resultado.
Nonaliasing requirement para parámetros resultado yvalor-resultado.
![Page 43: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/43.jpg)
Llamadas a Procedimiento IIÚnica Salida. Semántica I.
Sin perder generalidad, suponemos los parámetros ordenados enlistas por clasi�cador:
x : valor
y : valor-resultado
z : resultado
P(x , valres y , result z)
Sean a, b y c, listas de parámetros actuales correspondientes a x , yy z . Se de�ne wp para una llamada P(a,b,c) como:
wp(P(a,b,c),q) = wp({P.Pre[x ,y := a,b]};[P.Post[x ,y0,y ,z := a,b,b1,c1]];
b,c := b1,c1,
q)
donde b1 y c1 son variables frescas.
![Page 44: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/44.jpg)
Llamadas a Procedimiento IIÚnica Salida. Semántica I.
Sin perder generalidad, suponemos los parámetros ordenados enlistas por clasi�cador:
x : valor
y : valor-resultado
z : resultado
P(x , valres y , result z)
Sean a, b y c, listas de parámetros actuales correspondientes a x , yy z . Se de�ne wp para una llamada P(a,b,c) como:
wp(P(a,b,c),q) = wp({P.Pre[x ,y := a,b]};[P.Post[x ,y0,y ,z := a,b,b1,c1]];
b,c := b1,c1,
q)
donde b1 y c1 son variables frescas.
![Page 45: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/45.jpg)
Llamadas a Procedimiento IIIÚnica Salida. Semántica II.
¾De dónde sale?
Cálculo de Re�namientos.
Re�nar: quitar no determinismo, preservando corrección.
Cuando un procedimiento se prueba correcto, éste re�na a suespeci�cación.
Una llamada denota el cuerpo del procedimiento conparámetros formales reemplazados por actuales.
La llamada re�na a la sentencia de especi�cación:
{P.Pre[x ,y := a,b]}; [P.Post[x ,y0,y ,z := a,b,b1,c1];b,c := b1,c1
Principio de Sustitución
A los efectos de probar corrección, es lo mismo razonarsustituyendo la llamada por la sentencia de especi�cación.
¾Localidad?
![Page 46: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/46.jpg)
Llamadas a Procedimiento IIIÚnica Salida. Semántica II.
¾De dónde sale? Cálculo de Re�namientos.
Re�nar: quitar no determinismo, preservando corrección.
Cuando un procedimiento se prueba correcto, éste re�na a suespeci�cación.
Una llamada denota el cuerpo del procedimiento conparámetros formales reemplazados por actuales.
La llamada re�na a la sentencia de especi�cación:
{P.Pre[x ,y := a,b]}; [P.Post[x ,y0,y ,z := a,b,b1,c1];b,c := b1,c1
Principio de Sustitución
A los efectos de probar corrección, es lo mismo razonarsustituyendo la llamada por la sentencia de especi�cación.
¾Localidad?
![Page 47: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/47.jpg)
Llamadas a Procedimiento IIIÚnica Salida. Semántica II.
¾De dónde sale? Cálculo de Re�namientos.
Re�nar: quitar no determinismo, preservando corrección.
Cuando un procedimiento se prueba correcto, éste re�na a suespeci�cación.
Una llamada denota el cuerpo del procedimiento conparámetros formales reemplazados por actuales.
La llamada re�na a la sentencia de especi�cación:
{P.Pre[x ,y := a,b]}; [P.Post[x ,y0,y ,z := a,b,b1,c1];b,c := b1,c1
Principio de Sustitución
A los efectos de probar corrección, es lo mismo razonarsustituyendo la llamada por la sentencia de especi�cación.
¾Localidad?
![Page 48: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/48.jpg)
Llamadas a Procedimiento IIIÚnica Salida. Semántica II.
¾De dónde sale? Cálculo de Re�namientos.
Re�nar: quitar no determinismo, preservando corrección.
Cuando un procedimiento se prueba correcto, éste re�na a suespeci�cación.
Una llamada denota el cuerpo del procedimiento conparámetros formales reemplazados por actuales.
La llamada re�na a la sentencia de especi�cación:
{P.Pre[x ,y := a,b]}; [P.Post[x ,y0,y ,z := a,b,b1,c1];b,c := b1,c1
Principio de Sustitución
A los efectos de probar corrección, es lo mismo razonarsustituyendo la llamada por la sentencia de especi�cación.
¾Localidad?
![Page 49: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/49.jpg)
Llamadas a Procedimiento IIIÚnica Salida. Semántica II.
¾De dónde sale? Cálculo de Re�namientos.
Re�nar: quitar no determinismo, preservando corrección.
Cuando un procedimiento se prueba correcto, éste re�na a suespeci�cación.
Una llamada denota el cuerpo del procedimiento conparámetros formales reemplazados por actuales.
La llamada re�na a la sentencia de especi�cación:
{P.Pre[x ,y := a,b]}; [P.Post[x ,y0,y ,z := a,b,b1,c1];b,c := b1,c1
Principio de Sustitución
A los efectos de probar corrección, es lo mismo razonarsustituyendo la llamada por la sentencia de especi�cación.
¾Localidad?
![Page 50: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/50.jpg)
Llamadas a Procedimiento IIIÚnica Salida. Semántica II.
¾De dónde sale? Cálculo de Re�namientos.
Re�nar: quitar no determinismo, preservando corrección.
Cuando un procedimiento se prueba correcto, éste re�na a suespeci�cación.
Una llamada denota el cuerpo del procedimiento conparámetros formales reemplazados por actuales.
La llamada re�na a la sentencia de especi�cación:
{P.Pre[x ,y := a,b]}; [P.Post[x ,y0,y ,z := a,b,b1,c1];b,c := b1,c1
Principio de Sustitución
A los efectos de probar corrección, es lo mismo razonarsustituyendo la llamada por la sentencia de especi�cación.
¾Localidad?
![Page 51: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/51.jpg)
Llamadas a Procedimiento IIIÚnica Salida. Semántica II.
¾De dónde sale? Cálculo de Re�namientos.
Re�nar: quitar no determinismo, preservando corrección.
Cuando un procedimiento se prueba correcto, éste re�na a suespeci�cación.
Una llamada denota el cuerpo del procedimiento conparámetros formales reemplazados por actuales.
La llamada re�na a la sentencia de especi�cación:
{P.Pre[x ,y := a,b]}; [P.Post[x ,y0,y ,z := a,b,b1,c1];b,c := b1,c1
Principio de Sustitución
A los efectos de probar corrección, es lo mismo razonarsustituyendo la llamada por la sentencia de especi�cación.
¾Localidad?
![Page 52: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/52.jpg)
Llamadas a Procedimiento IIIÚnica Salida. Semántica II.
¾De dónde sale? Cálculo de Re�namientos.
Re�nar: quitar no determinismo, preservando corrección.
Cuando un procedimiento se prueba correcto, éste re�na a suespeci�cación.
Una llamada denota el cuerpo del procedimiento conparámetros formales reemplazados por actuales.
La llamada re�na a la sentencia de especi�cación:
{P.Pre[x ,y := a,b]}; [P.Post[x ,y0,y ,z := a,b,b1,c1];b,c := b1,c1
Principio de Sustitución
A los efectos de probar corrección, es lo mismo razonarsustituyendo la llamada por la sentencia de especi�cación.
¾Localidad?
![Page 53: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/53.jpg)
Llamadas a Procedimiento IVMúltiples Salidas.
Las llamadas a procedimientos de múltiples salidas:
Son sentencias de múltiplessalidas (conjuntos desentencias simples).
Sirven para manejo deexcepciones (de a un paso).
Pseudo-sintaxis: P(a1, ...,am)bl1→ (T1, I1), ..., lk → (Tk , Ik)cPseudo-semántica:
wp∗(P(a1, ...,am)bl1→ (T1, I1), ..., lk → (Tk , Ik)c)= wp({P.Pre[x ,y := a,b]},
(wp([P.l1[x ,y0,y ,z := a,b,b1,c1]];b,c := b1,c1;T1, I1)
∧...∧wp([P.lk [x ,y0,y ,z := a,b,b1,c1]];b,c := b1,c1;Tk , Ik))
![Page 54: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/54.jpg)
Llamadas a Procedimiento IVMúltiples Salidas.
Las llamadas a procedimientos de múltiples salidas:
Son sentencias de múltiplessalidas (conjuntos desentencias simples).
Sirven para manejo deexcepciones (de a un paso).
Pseudo-sintaxis: P(a1, ...,am)bl1→ (T1, I1), ..., lk → (Tk , Ik)c
Pseudo-semántica:
wp∗(P(a1, ...,am)bl1→ (T1, I1), ..., lk → (Tk , Ik)c)= wp({P.Pre[x ,y := a,b]},
(wp([P.l1[x ,y0,y ,z := a,b,b1,c1]];b,c := b1,c1;T1, I1)
∧...∧wp([P.lk [x ,y0,y ,z := a,b,b1,c1]];b,c := b1,c1;Tk , Ik))
![Page 55: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/55.jpg)
Llamadas a Procedimiento IVMúltiples Salidas.
Las llamadas a procedimientos de múltiples salidas:
Son sentencias de múltiplessalidas (conjuntos desentencias simples).
Sirven para manejo deexcepciones (de a un paso).
Pseudo-sintaxis: P(a1, ...,am)bl1→ (T1, I1), ..., lk → (Tk , Ik)cPseudo-semántica:
wp∗(P(a1, ...,am)bl1→ (T1, I1), ..., lk → (Tk , Ik)c)= wp({P.Pre[x ,y := a,b]},
(wp([P.l1[x ,y0,y ,z := a,b,b1,c1]];b,c := b1,c1;T1, I1)
∧...∧wp([P.lk [x ,y0,y ,z := a,b,b1,c1]];b,c := b1,c1;Tk , Ik))
![Page 56: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/56.jpg)
Llamadas en IBP I
Necesitamos una forma de visualizar la semántica de la llamada in
situ.
Replace
Nueva variación de Replace con una llamada paraencontrar los elementos a reemplazar. SearchFrom
Busca la primera ocurrenciade x en a a partir de j. Si loencuentra, pone el índice en j.Si no, retorna la longitud de a.
![Page 57: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/57.jpg)
Llamadas en IBP I
Necesitamos una forma de visualizar la semántica de la llamada in
situ.
Replace
Nueva variación de Replace con una llamada paraencontrar los elementos a reemplazar.
SearchFromBusca la primera ocurrenciade x en a a partir de j. Si loencuentra, pone el índice en j.Si no, retorna la longitud de a.
![Page 58: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/58.jpg)
Llamadas en IBP I
Necesitamos una forma de visualizar la semántica de la llamada in
situ.
Replace
Nueva variación de Replace con una llamada paraencontrar los elementos a reemplazar. SearchFrom
Busca la primera ocurrenciade x en a a partir de j. Si loencuentra, pone el índice en j.Si no, retorna la longitud de a.
![Page 59: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/59.jpg)
Llamadas en IBP I
Necesitamos una forma de visualizar la semántica de la llamada in
situ.
Replace
Nueva variación de Replace con una llamada paraencontrar los elementos a reemplazar. SearchFrom
Busca la primera ocurrenciade x en a a partir de j. Si loencuentra, pone el índice en j.Si no, retorna la longitud de a.
![Page 60: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/60.jpg)
Llamadas en IBP IIContrato actual.
De�nición
El contrato actual de una llamada a procedimiento es una copia delcontrato formal, reemplazando la signatura por la llamada y losparámetros formales por los actuales, de acuerdo con la sustitución dadaen la semántica para llamadas.
Contrato actual para la llamada a SearchFrom
![Page 61: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/61.jpg)
Llamadas en IBP IIContrato actual.
De�nición
El contrato actual de una llamada a procedimiento es una copia delcontrato formal, reemplazando la signatura por la llamada y losparámetros formales por los actuales, de acuerdo con la sustitución dadaen la semántica para llamadas.
Contrato actual para la llamada a SearchFrom
![Page 62: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/62.jpg)
Llamadas en IBP IIIExpansión.
Principio de Sustitución
wp∗(SearchFrom(a,x , i)bFound→ (S1 ,Loop),Not−Found→ (T2 , I2)c)
= wp({0≤ i < len(a)},
(wp([0≤ i ≤ i1 < len(a)∧NotFoundBetween(i , i1)∧a[i1] = x]; i := i1;S1 ,Loop)
∧wp([0≤ i ≤ i1 ≤ len(a)∧NotFoundBetween(i , i1)∧ i1 = len(a)]; i := i1;T2 , I2))
![Page 63: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/63.jpg)
Llamadas en IBP IIIExpansión.
Principio de Sustitución
wp∗(SearchFrom(a,x , i)bFound→ (S1 ,Loop),Not−Found→ (T2 , I2)c)
= wp({0≤ i < len(a)},
(wp([0≤ i ≤ i1 < len(a)∧NotFoundBetween(i , i1)∧a[i1] = x]; i := i1;S1 ,Loop)
∧wp([0≤ i ≤ i1 ≤ len(a)∧NotFoundBetween(i , i1)∧ i1 = len(a)]; i := i1;T2 , I2))
![Page 64: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/64.jpg)
Llamadas en IBP IIIExpansión.
Principio de Sustitución
wp∗(SearchFrom(a,x , i)bFound→ (S1 ,Loop),Not−Found→ (T2 , I2)c)
= wp({0≤ i < len(a)},
(wp([0≤ i ≤ i1 < len(a)∧NotFoundBetween(i , i1)∧a[i1] = x]; i := i1;S1 ,Loop)
∧wp([0≤ i ≤ i1 ≤ len(a)∧NotFoundBetween(i , i1)∧ i1 = len(a)]; i := i1;T2 , I2))
![Page 65: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/65.jpg)
Llamadas en IBP IIIExpansión.
Principio de Sustitución
wp∗(SearchFrom(a,x , i)bFound→ (S1 ,Loop),Not−Found→ (T2 , I2)c)
= wp({0≤ i < len(a)},
(wp([0≤ i ≤ i1 < len(a)∧NotFoundBetween(i , i1)∧a[i1] = x]; i := i1;S1 ,Loop)
∧wp([0≤ i ≤ i1 ≤ len(a)∧NotFoundBetween(i , i1)∧ i1 = len(a)]; i := i1;T2 , I2))
![Page 66: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/66.jpg)
Llamadas en IBP IIIExpansión.
Principio de Sustitución
wp∗(SearchFrom(a,x , i)bFound→ (S1 ,Loop),Not−Found→ (T2 , I2)c)
= wp({0≤ i < len(a)},
(wp([0≤ i ≤ i1 < len(a)∧NotFoundBetween(i , i1)∧a[i1] = x]; i := i1;S1 ,Loop)
∧wp([0≤ i ≤ i1 ≤ len(a)∧NotFoundBetween(i , i1)∧ i1 = len(a)]; i := i1;T2 , I2))
![Page 67: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/67.jpg)
Llamadas en IBP IIIExpansión.
Principio de Sustitución
wp∗(SearchFrom(a,x , i)bFound→ (S1 ,Loop),Not−Found→ (T2 , I2)c)
= wp({0≤ i < len(a)},
(wp([0≤ i ≤ i1 < len(a)∧NotFoundBetween(i , i1)∧a[i1] = x]; i := i1;S1 ,Loop)
∧wp([0≤ i ≤ i1 ≤ len(a)∧NotFoundBetween(i , i1)∧ i1 = len(a)]; i := i1;T2 , I2))
![Page 68: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/68.jpg)
Llamadas en IBP IIIExpansión.
Principio de Sustitución
wp∗(SearchFrom(a,x , i)bFound→ (S1 ,Loop),Not−Found→ (T2 , I2)c)
= wp({0≤ i < len(a)},
(wp([0≤ i ≤ i1 < len(a)∧NotFoundBetween(i , i1)∧a[i1] = x]; i := i1;S1 ,Loop)
∧wp([0≤ i ≤ i1 ≤ len(a)∧NotFoundBetween(i , i1)∧ i1 = len(a)]; i := i1;T2 , I2))
![Page 69: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/69.jpg)
Llamadas en IBP IIIExpansión.
Principio de Sustitución
wp∗(SearchFrom(a,x , i)bFound→ (S1 ,Loop),Not−Found→ (T2 , I2)c)
= wp({0≤ i < len(a)},
(wp([0≤ i ≤ i1 < len(a)∧NotFoundBetween(i , i1)∧a[i1] = x]; i := i1;S1 ,Loop)
∧wp([0≤ i ≤ i1 ≤ len(a)∧NotFoundBetween(i , i1)∧ i1 = len(a)]; i := i1;T2 , I2))
![Page 70: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/70.jpg)
Contenidos
1 IntroducciónMotivaciónDescripción del ProblemaProgramación Basada en Invariantes
2 ProcedimientosDeclaraciónContrato FormalMúltiples Salidas
3 Llamadas a ProcedimientoLlamadas de Única SalidaLlamadas de Múltiples SalidasLlamadas a en IBP
4 Recursión y TerminaciónLlamadas RecursivasRecursión SimpleRecursión Mutua
5 Conclusiones y Trabajos Futuros
![Page 71: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/71.jpg)
Llamadas RecursivasEjemplo.
SearchFrom
Implementación recursiva de SearchFrom.
Observaciones
Pueden introducir noterminación.
Expresión de recursión(' variante).
Cláusula recurses
decreasing.
Para consistencia, elenfoque no cambia.
![Page 72: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/72.jpg)
Llamadas RecursivasEjemplo.
SearchFrom
Implementación recursiva de SearchFrom.
Observaciones
Pueden introducir noterminación.
Expresión de recursión(' variante).
Cláusula recurses
decreasing.
Para consistencia, elenfoque no cambia.
![Page 73: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/73.jpg)
Recursión Simple
Un procedimiento se llama a sí mismo en forma directa.
Similar a la terminación de ciclos en transiciones.
Pero la expresión de recursión (rec) debe ser reducida entre elcomienzo del cuerpo y el punto de la llamada recursiva.
Posiblemente en varios pasos.Lo resolvemos usando invariantes para propagar el progreso.
Para la condición de veri�cación hay que probar que{rec[x := a]< rec0} es consistente en el punto de la llamadarecursiva, donde x y a son listas de parámetros formales y actuales,respectivamente.
SearchFrom
Para la llamada recursiva de SearchFrom esto es:{len(a)− j < len(a)− j0}
que es consistente, pues j = j0+1 en el punto de lallamada.
![Page 74: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/74.jpg)
Recursión Simple
Un procedimiento se llama a sí mismo en forma directa.
Similar a la terminación de ciclos en transiciones.
Pero la expresión de recursión (rec) debe ser reducida entre elcomienzo del cuerpo y el punto de la llamada recursiva.
Posiblemente en varios pasos.Lo resolvemos usando invariantes para propagar el progreso.
Para la condición de veri�cación hay que probar que{rec[x := a]< rec0} es consistente en el punto de la llamadarecursiva, donde x y a son listas de parámetros formales y actuales,respectivamente.
SearchFrom
Para la llamada recursiva de SearchFrom esto es:{len(a)− j < len(a)− j0}
que es consistente, pues j = j0+1 en el punto de lallamada.
![Page 75: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/75.jpg)
Recursión Simple
Un procedimiento se llama a sí mismo en forma directa.
Similar a la terminación de ciclos en transiciones.
Pero la expresión de recursión (rec) debe ser reducida entre elcomienzo del cuerpo y el punto de la llamada recursiva.
Posiblemente en varios pasos.Lo resolvemos usando invariantes para propagar el progreso.
Para la condición de veri�cación hay que probar que{rec[x := a]< rec0} es consistente en el punto de la llamadarecursiva, donde x y a son listas de parámetros formales y actuales,respectivamente.
SearchFrom
Para la llamada recursiva de SearchFrom esto es:{len(a)− j < len(a)− j0}
que es consistente, pues j = j0+1 en el punto de lallamada.
![Page 76: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/76.jpg)
Recursión Simple
Un procedimiento se llama a sí mismo en forma directa.
Similar a la terminación de ciclos en transiciones.
Pero la expresión de recursión (rec) debe ser reducida entre elcomienzo del cuerpo y el punto de la llamada recursiva.
Posiblemente en varios pasos.
Lo resolvemos usando invariantes para propagar el progreso.
Para la condición de veri�cación hay que probar que{rec[x := a]< rec0} es consistente en el punto de la llamadarecursiva, donde x y a son listas de parámetros formales y actuales,respectivamente.
SearchFrom
Para la llamada recursiva de SearchFrom esto es:{len(a)− j < len(a)− j0}
que es consistente, pues j = j0+1 en el punto de lallamada.
![Page 77: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/77.jpg)
Recursión Simple
Un procedimiento se llama a sí mismo en forma directa.
Similar a la terminación de ciclos en transiciones.
Pero la expresión de recursión (rec) debe ser reducida entre elcomienzo del cuerpo y el punto de la llamada recursiva.
Posiblemente en varios pasos.Lo resolvemos usando invariantes para propagar el progreso.
Para la condición de veri�cación hay que probar que{rec[x := a]< rec0} es consistente en el punto de la llamadarecursiva, donde x y a son listas de parámetros formales y actuales,respectivamente.
SearchFrom
Para la llamada recursiva de SearchFrom esto es:{len(a)− j < len(a)− j0}
que es consistente, pues j = j0+1 en el punto de lallamada.
![Page 78: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/78.jpg)
Recursión Simple
Un procedimiento se llama a sí mismo en forma directa.
Similar a la terminación de ciclos en transiciones.
Pero la expresión de recursión (rec) debe ser reducida entre elcomienzo del cuerpo y el punto de la llamada recursiva.
Posiblemente en varios pasos.Lo resolvemos usando invariantes para propagar el progreso.
Para la condición de veri�cación hay que probar que{rec[x := a]< rec0} es consistente en el punto de la llamadarecursiva, donde x y a son listas de parámetros formales y actuales,respectivamente.
SearchFrom
Para la llamada recursiva de SearchFrom esto es:{len(a)− j < len(a)− j0}
que es consistente, pues j = j0+1 en el punto de lallamada.
![Page 79: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/79.jpg)
Recursión Simple
Un procedimiento se llama a sí mismo en forma directa.
Similar a la terminación de ciclos en transiciones.
Pero la expresión de recursión (rec) debe ser reducida entre elcomienzo del cuerpo y el punto de la llamada recursiva.
Posiblemente en varios pasos.Lo resolvemos usando invariantes para propagar el progreso.
Para la condición de veri�cación hay que probar que{rec[x := a]< rec0} es consistente en el punto de la llamadarecursiva, donde x y a son listas de parámetros formales y actuales,respectivamente.
SearchFrom
Para la llamada recursiva de SearchFrom esto es:{len(a)− j < len(a)− j0}
que es consistente, pues j = j0+1 en el punto de lallamada.
![Page 80: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/80.jpg)
Recursión Mutua I
Un conjunto de procedimientos se llaman mutuamente formandociclos.
Una generalización de lo anterior falla, pues los procedimientostienen espacios de estados diferentes.
Solución: expresión de recursión + progreso + grafo de llamadas.
Además de la expresión de recursión, se requiere una expresion deprogreso por cada proceso llamado en recursión mutua:
calls P with progexp
donde progexp es una relación entre identi�cadores de ambosprocedimientos con los operadores <, ≤ y =.
El progreso mide cómo se reduce el problema entre dos llamadas deun ciclo.
![Page 81: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/81.jpg)
Recursión Mutua I
Un conjunto de procedimientos se llaman mutuamente formandociclos.
Una generalización de lo anterior falla, pues los procedimientostienen espacios de estados diferentes.
Solución: expresión de recursión + progreso + grafo de llamadas.
Además de la expresión de recursión, se requiere una expresion deprogreso por cada proceso llamado en recursión mutua:
calls P with progexp
donde progexp es una relación entre identi�cadores de ambosprocedimientos con los operadores <, ≤ y =.
El progreso mide cómo se reduce el problema entre dos llamadas deun ciclo.
![Page 82: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/82.jpg)
Recursión Mutua I
Un conjunto de procedimientos se llaman mutuamente formandociclos.
Una generalización de lo anterior falla, pues los procedimientostienen espacios de estados diferentes.
Solución: expresión de recursión + progreso + grafo de llamadas.
Además de la expresión de recursión, se requiere una expresion deprogreso por cada proceso llamado en recursión mutua:
calls P with progexp
donde progexp es una relación entre identi�cadores de ambosprocedimientos con los operadores <, ≤ y =.
El progreso mide cómo se reduce el problema entre dos llamadas deun ciclo.
![Page 83: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/83.jpg)
Recursión Mutua I
Un conjunto de procedimientos se llaman mutuamente formandociclos.
Una generalización de lo anterior falla, pues los procedimientostienen espacios de estados diferentes.
Solución: expresión de recursión + progreso + grafo de llamadas.
Además de la expresión de recursión, se requiere una expresion deprogreso por cada proceso llamado en recursión mutua:
calls P with progexp
donde progexp es una relación entre identi�cadores de ambosprocedimientos con los operadores <, ≤ y =.
El progreso mide cómo se reduce el problema entre dos llamadas deun ciclo.
![Page 84: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/84.jpg)
Recursión Mutua I
Un conjunto de procedimientos se llaman mutuamente formandociclos.
Una generalización de lo anterior falla, pues los procedimientostienen espacios de estados diferentes.
Solución: expresión de recursión + progreso + grafo de llamadas.
Además de la expresión de recursión, se requiere una expresion deprogreso por cada proceso llamado en recursión mutua:
calls P with progexp
donde progexp es una relación entre identi�cadores de ambosprocedimientos con los operadores <, ≤ y =.
El progreso mide cómo se reduce el problema entre dos llamadas deun ciclo.
![Page 85: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/85.jpg)
Recursión Mutua II
La terminación se prueba en dos pasos:
1 El progreso declarado en la especi�cación, se prueba localmente(' terminación para recursión simple).
2 A nivel de las especi�caciones, se prueba que las expresiones derecursión son reducidas, cuando se colecta el progreso para cadaciclo del grafo de llamadas.
Función call_progress.
Condición de veri�cación para recursión.(Pow1→Pow1, Pow1→Pow2→Pow1, Pow2→Pow1→Pow2)
Condición de veri�cación para desviación.(Pow1→Pow1→Pow2)
![Page 86: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/86.jpg)
Recursión Mutua II
La terminación se prueba en dos pasos:
1 El progreso declarado en la especi�cación, se prueba localmente(' terminación para recursión simple).
2 A nivel de las especi�caciones, se prueba que las expresiones derecursión son reducidas, cuando se colecta el progreso para cadaciclo del grafo de llamadas.
Función call_progress.
Condición de veri�cación para recursión.(Pow1→Pow1, Pow1→Pow2→Pow1, Pow2→Pow1→Pow2)
Condición de veri�cación para desviación.(Pow1→Pow1→Pow2)
![Page 87: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/87.jpg)
Recursión Mutua II
La terminación se prueba en dos pasos:
1 El progreso declarado en la especi�cación, se prueba localmente(' terminación para recursión simple).
2 A nivel de las especi�caciones, se prueba que las expresiones derecursión son reducidas, cuando se colecta el progreso para cadaciclo del grafo de llamadas.
Función call_progress.
Condición de veri�cación para recursión.(Pow1→Pow1, Pow1→Pow2→Pow1, Pow2→Pow1→Pow2)
Condición de veri�cación para desviación.(Pow1→Pow1→Pow2)
![Page 88: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/88.jpg)
Recursión Mutua II
La terminación se prueba en dos pasos:
1 El progreso declarado en la especi�cación, se prueba localmente(' terminación para recursión simple).
2 A nivel de las especi�caciones, se prueba que las expresiones derecursión son reducidas, cuando se colecta el progreso para cadaciclo del grafo de llamadas.
Función call_progress.
Condición de veri�cación para recursión.(Pow1→Pow1, Pow1→Pow2→Pow1, Pow2→Pow1→Pow2)
Condición de veri�cación para desviación.(Pow1→Pow1→Pow2)
![Page 89: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/89.jpg)
Contenidos
1 IntroducciónMotivaciónDescripción del ProblemaProgramación Basada en Invariantes
2 ProcedimientosDeclaraciónContrato FormalMúltiples Salidas
3 Llamadas a ProcedimientoLlamadas de Única SalidaLlamadas de Múltiples SalidasLlamadas a en IBP
4 Recursión y TerminaciónLlamadas RecursivasRecursión SimpleRecursión Mutua
5 Conclusiones y Trabajos Futuros
![Page 90: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/90.jpg)
Resumen
En este trabajo vimos:
La programación basada en invariantes como enfoqueorientado a construir programas veri�cables de forma natural.
La necesidad de extender el formalismo con construccionesmás complejas: procedimientos y las di�cultades que acarrean.
Una propuesta metodológica, con fuerte base teórica, pararazonar sobre procedimientos y llamadas, contemplandodiversos mecanismos de pasaje de parámetros, manejo deexcepciones y recursión.
Además, la tesis describe:
Notación textual para programas IBP.Implementación: sistemas de reescritura, PVS, analizador yveri�cador. Posibles extensiones.Caso de estudio: biblioteca de manejo de strings.
![Page 91: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/91.jpg)
Resumen
En este trabajo vimos:
La programación basada en invariantes como enfoqueorientado a construir programas veri�cables de forma natural.
La necesidad de extender el formalismo con construccionesmás complejas: procedimientos y las di�cultades que acarrean.
Una propuesta metodológica, con fuerte base teórica, pararazonar sobre procedimientos y llamadas, contemplandodiversos mecanismos de pasaje de parámetros, manejo deexcepciones y recursión.
Además, la tesis describe:
Notación textual para programas IBP.Implementación: sistemas de reescritura, PVS, analizador yveri�cador. Posibles extensiones.Caso de estudio: biblioteca de manejo de strings.
![Page 92: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/92.jpg)
Resumen
En este trabajo vimos:
La programación basada en invariantes como enfoqueorientado a construir programas veri�cables de forma natural.
La necesidad de extender el formalismo con construccionesmás complejas: procedimientos y las di�cultades que acarrean.
Una propuesta metodológica, con fuerte base teórica, pararazonar sobre procedimientos y llamadas, contemplandodiversos mecanismos de pasaje de parámetros, manejo deexcepciones y recursión.
Además, la tesis describe:
Notación textual para programas IBP.Implementación: sistemas de reescritura, PVS, analizador yveri�cador. Posibles extensiones.Caso de estudio: biblioteca de manejo de strings.
![Page 93: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/93.jpg)
Resumen
En este trabajo vimos:
La programación basada en invariantes como enfoqueorientado a construir programas veri�cables de forma natural.
La necesidad de extender el formalismo con construccionesmás complejas: procedimientos y las di�cultades que acarrean.
Una propuesta metodológica, con fuerte base teórica, pararazonar sobre procedimientos y llamadas, contemplandodiversos mecanismos de pasaje de parámetros, manejo deexcepciones y recursión.
Además, la tesis describe:
Notación textual para programas IBP.Implementación: sistemas de reescritura, PVS, analizador yveri�cador. Posibles extensiones.Caso de estudio: biblioteca de manejo de strings.
![Page 94: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/94.jpg)
Conclusiones
El tratamiendo de las llamadas extiende IBP de forma prácticay visual, de acuerdo con sus principios.
Abordamos terminación manteniendo localidad.
Excepto para recursión mutua, pero ahí razonamos al nivel delas especi�caciones.
En la versión textual, el resultado de expandir las llamadas ytratar terminación es un programa IBP sin llamadas, tratablecon las técnicas y herramientas disponibles.
La técnica mostró ser útil en la práctica, ayudando en laconstrucción de los programas con llamadas para el caso deestudio.
![Page 95: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/95.jpg)
Conclusiones
El tratamiendo de las llamadas extiende IBP de forma prácticay visual, de acuerdo con sus principios.
Abordamos terminación manteniendo localidad.
Excepto para recursión mutua, pero ahí razonamos al nivel delas especi�caciones.
En la versión textual, el resultado de expandir las llamadas ytratar terminación es un programa IBP sin llamadas, tratablecon las técnicas y herramientas disponibles.
La técnica mostró ser útil en la práctica, ayudando en laconstrucción de los programas con llamadas para el caso deestudio.
![Page 96: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/96.jpg)
Conclusiones
El tratamiendo de las llamadas extiende IBP de forma prácticay visual, de acuerdo con sus principios.
Abordamos terminación manteniendo localidad.
Excepto para recursión mutua, pero ahí razonamos al nivel delas especi�caciones.
En la versión textual, el resultado de expandir las llamadas ytratar terminación es un programa IBP sin llamadas, tratablecon las técnicas y herramientas disponibles.
La técnica mostró ser útil en la práctica, ayudando en laconstrucción de los programas con llamadas para el caso deestudio.
![Page 97: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/97.jpg)
Conclusiones
El tratamiendo de las llamadas extiende IBP de forma prácticay visual, de acuerdo con sus principios.
Abordamos terminación manteniendo localidad.
Excepto para recursión mutua, pero ahí razonamos al nivel delas especi�caciones.
En la versión textual, el resultado de expandir las llamadas ytratar terminación es un programa IBP sin llamadas, tratablecon las técnicas y herramientas disponibles.
La técnica mostró ser útil en la práctica, ayudando en laconstrucción de los programas con llamadas para el caso deestudio.
![Page 98: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/98.jpg)
Conclusiones
El tratamiendo de las llamadas extiende IBP de forma prácticay visual, de acuerdo con sus principios.
Abordamos terminación manteniendo localidad.
Excepto para recursión mutua, pero ahí razonamos al nivel delas especi�caciones.
En la versión textual, el resultado de expandir las llamadas ytratar terminación es un programa IBP sin llamadas, tratablecon las técnicas y herramientas disponibles.
La técnica mostró ser útil en la práctica, ayudando en laconstrucción de los programas con llamadas para el caso deestudio.
![Page 99: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/99.jpg)
Trabajos Futuros
Herramientas de soporte: es fundamental, ya que evitaríatotalmente las sustituciones manuales, tediosas y propensas aerrores.
Procedimientos y llamadas.Interface grá�ca.
Caso de estudio: más procedimientos y pruebas de veri�cación.
Modulo veri�cado reutilizable.
![Page 100: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/100.jpg)
Trabajos Futuros
Herramientas de soporte: es fundamental, ya que evitaríatotalmente las sustituciones manuales, tediosas y propensas aerrores.
Procedimientos y llamadas.Interface grá�ca.
Caso de estudio: más procedimientos y pruebas de veri�cación.
Modulo veri�cado reutilizable.
![Page 101: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/101.jpg)
Trabajos Futuros
Herramientas de soporte: es fundamental, ya que evitaríatotalmente las sustituciones manuales, tediosas y propensas aerrores.
Procedimientos y llamadas.Interface grá�ca.
Caso de estudio: más procedimientos y pruebas de veri�cación.
Modulo veri�cado reutilizable.
![Page 102: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/102.jpg)
Trabajos Futuros
Herramientas de soporte: es fundamental, ya que evitaríatotalmente las sustituciones manuales, tediosas y propensas aerrores.
Procedimientos y llamadas.Interface grá�ca.
Caso de estudio: más procedimientos y pruebas de veri�cación.
Modulo veri�cado reutilizable.
![Page 103: Un Método Práctico para Razonar sobre … · Un Método Práctico para Razonar sobre Procedimientos en la Programación Basada en Invariantes Brian Plüss Director Prof. Ralph-Johan](https://reader030.fdocumento.com/reader030/viewer/2022021611/5ba1b7eb09d3f2766b8cfc78/html5/thumbnails/103.jpg)
½Gracias!
�For the absence of a bibliography I o�er neither explanation nor apology�
E.W. Dijkstra, A Discipline of Programming
¾Preguntas?