1. Espiritual

Demostraciones asistidas por computadora
cómo es posible obtener programas correctos por construcción
Lourdes del Carmen González Huesca
http://www.pps.univ-paris-diderot.fr/~lgonzale
πr 2 , Lab.
Preuves, Programmes et Systèmes
Université Paris Diderot, CNRS & INRIA
Mesa Redonda: Del mundo digital a la vida real: las apps, los teléfonos
inteligentes y el mercado de telecomunicaciones actual
Casa de México
28 de Enero de 2014
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
1 / 14
Computación
Hace 50 años no era posible imaginar el potencial de las computadoras,
todos los usos que ahora tiene...
sobre todo hacer más fácil nuestra vida diaria.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
2 / 14
Computación
Pero, las computadoras, smartphones, tablets, etc.
¿son inteligentes o muestran un comportamiento inteligente?
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
2 / 14
Errores
¿por qué no funcionan bien, con sentido común o
de forma inteligente?
¿por qué se bloquean o hacen algo mal?
¿tienen la culpa estos aparatos?
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
3 / 14
Errores
¿por qué no funcionan bien, con sentido común o
de forma inteligente?
¿por qué se bloquean o hacen algo mal?
¿tienen la culpa estos aparatos?
¡NO! Generalmente son errores de programación.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
3 / 14
Errores de programación
XKCD http://imgs.xkcd.com/comics/computer_problems.png
Una computadora es una máquina para hacer cálculos,
se le debe “decir” qué hacer o darle órdenes.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
4 / 14
Errores de programación
XKCD http://imgs.xkcd.com/comics/computer_problems.png
Una computadora es una máquina para hacer cálculos,
se le debe “decir” qué hacer o darle órdenes.
Las órdenes son instrucciones de cómo hacer los cálculos,
luego entonces, los errores se encuentran en las instrucciones.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
4 / 14
Programas
Considerar a los programas como objetos de estudio:
➔ un programa es un conjunto de instrucciones ordenadas ,
➔ escrito en un lenguaje formal ,
➔ para resolver un problema.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
5 / 14
Programas
Considerar a los programas como objetos de estudio:
➔ un programa es un conjunto de instrucciones ordenadas ,
➔ escrito en un lenguaje formal ,
➔ para resolver un problema.
Los programas son una secuencia de instrucciones
para llevar a cabo un trabajo en la computadora.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
5 / 14
Programas
Hay que saber diferenciar un algoritmo de un programa.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
6 / 14
Programas
Hay que saber diferenciar un algoritmo de un programa.
Saber escribir programas que sean comprendidos por la computadora.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
6 / 14
Programas
Hay que saber diferenciar un algoritmo de un programa.
Saber escribir programas que sean comprendidos por la computadora.
Y lo que nos interesa: ¡programas sin errores!
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
6 / 14
Ciencias de la computación
¿qué son?
Grosso modo: es el estudio de la información ,
cómo se manipula y se transforma, cómo se transmite.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
7 / 14
Ciencias de la computación
¿qué son?
Grosso modo: es el estudio de la información ,
cómo se manipula y se transforma, cómo se transmite.
Más estricto: es el estudio de los principios, usos y
tecnologías del cómputo.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
7 / 14
Ciencias de la computación
¿qué son?
Grosso modo: es el estudio de la información ,
cómo se manipula y se transforma, cómo se transmite.
Más estricto: es el estudio de los principios, usos y
tecnologías del cómputo.
Sencillamente: es la ciencia de resolver problemas,
con áreas teóricas y prácticas.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
7 / 14
Ciencias de la computación
¡Programar es un proceso que requiere de mucho cuidado y
atención a los detalles!
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
8 / 14
Ciencias de la computación
¡Programar es un proceso que requiere de mucho cuidado y
atención a los detalles!
Para el manejo de información es necesario
un pensamiento crítico y razonar de forma correcta.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
8 / 14
Ciencias de la computación
¡Programar es un proceso que requiere de mucho cuidado y
atención a los detalles!
Para el manejo de información es necesario
un pensamiento crítico y razonar de forma correcta.
La lógica es un lenguaje formal para la argumentación y
el razonamiénto válido.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
8 / 14
Formalidades
Programas correctos, por constucción
matemáticas – mostrar de forma abstracta que algo existe
computación – construir ese algo para usarlo
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
9 / 14
Formalidades
Programas correctos, por constucción
matemáticas – mostrar de forma abstracta que algo existe
computación – construir ese algo para usarlo
Es decir, usar la lógica (matemática) como lenguaje para
la construccion, manipulación, uso, etc., de
conocimiento o información.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
9 / 14
Formalidades
Programas correctos, por constucción
matemáticas – mostrar de forma abstracta que algo existe
computación – construir ese algo para usarlo
Es decir, usar la lógica (matemática) como lenguaje para
la construccion, manipulación, uso, etc., de
conocimiento o información.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
9 / 14
¿¿¿Matemáticas???
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
10 / 14
¿¿¿Matemáticas???
Queremos programas sin erores, usando lenguajes formales
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
10 / 14
¿¿¿Matemáticas???
Queremos programas sin erores, usando lenguajes formales
Lógica matemática
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
10 / 14
Verificación de programas
A través de la estrecha relación entre lógica y computación
se construyen los verificadores:
las demostraciones equivalen a los programas
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
11 / 14
Verificación de programas
A través de la estrecha relación entre lógica y computación
se construyen los verificadores:
las demostraciones equivalen a los programas
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
11 / 14
Verificación de programas
A través de la estrecha relación entre lógica y computación
se construyen los verificadores:
las demostraciones equivalen a los programas
Los verificadores son teorías bien fundamentadas que han sido
estudiadas a detalle:
son pequeños programas correctos que
ayudan a revisar programas más grandes y complejos.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
11 / 14
Sistemas manejadores de pruebas
Asistente de pruebas
Ambiente para desarrollar pruebas
L. González Huesca (πr 2 -PPS)
Verificador de pruebas
Programas correctos por construcción
28-Enero-2014
12 / 14
Sistemas manejadores de pruebas
Asistente de pruebas
Ambiente para desarrollar pruebas
Verificador de pruebas
➔ un programa interactivo que
➔ sirve de guía al usuario para obtener demostraciones que
➔ son verificadas y
➔ si son correctas entonces son transformadas en programas.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
12 / 14
Sistemas manejadores de pruebas
Asistente de pruebas
Ambiente para desarrollar pruebas
Verificador de pruebas
➔ un programa interactivo que
➔ sirve de guía al usuario para obtener demostraciones que
➔ son verificadas y
➔ si son correctas entonces son transformadas en programas.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
12 / 14
Sistemas manejadores de pruebas
Asistente de pruebas
Ambiente para desarrollar pruebas
Verificador de pruebas
➔ un programa interactivo que
➔ sirve de guía al usuario para obtener demostraciones que
➔ son verificadas y
➔ si son correctas entonces son transformadas en programas.
¡creatividad del usuario!
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
12 / 14
Comentarios finales
Después de la década de 1980,
los asistentes de prueba han tenido un gran avance:
están en auge para sustentar el conocimiento científico,
además de favorecer el proceso de descubrimiento matemático.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
13 / 14
Comentarios finales
Después de la década de 1980,
los asistentes de prueba han tenido un gran avance:
están en auge para sustentar el conocimiento científico,
además de favorecer el proceso de descubrimiento matemático.
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
13 / 14
Comentarios finales
Después de la década de 1980,
los asistentes de prueba han tenido un gran avance:
están en auge para sustentar el conocimiento científico,
además de favorecer el proceso de descubrimiento matemático.
¡No sólo es verificar sino también descubrir cosas nuevas!
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
13 / 14
Comentarios finales
Después de la década de 1980,
los asistentes de prueba han tenido un gran avance:
están en auge para sustentar el conocimiento científico,
además de favorecer el proceso de descubrimiento matemático.
¡No sólo es verificar sino también descubrir cosas nuevas!
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
13 / 14
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
14 / 14
L. González Huesca (πr 2 -PPS)
Programas correctos por construcción
28-Enero-2014
14 / 14