Es TDD la hermana pequeña de la validación formal?

[Joserra]

Me preguntaba, por que no sé por dónde leí algo así, que hemos llegado
al TDD por que somos unos "blanditos" que no nos atrevemos con la
validación formal, es decir, una validación matemática de algoritmos y
métodos.
¿qué os parece? Hace unos meses estuve en una charla de un grupo de
investigación que contaba que trabajan en la demostración matemática
de que los programas no fallan. Y bajo ciertas circunstancias de
lenguaje, podían demostrar (era complejo, eh) que un programa nunca
terminaba con un OutOfMemory, de manera que sabían que podría correr
el programa indefinidamente sin llegar a ese problema.
Acabaremos haciendo algo así con todo? :)

[José Manuel Beas]

Pues a mi me parece que la "programación metódica" [1] (libro de José
Luis Balcázar que aún conservo en mi biblioteca [2]) es una utopía en
"el mundo real". Está bien como ejercicios de laboratorio e incluso no
excluyo su aplicación en sistemas muy específicos (estoy pensando en
ámbitos como la genómica y cosas por el estilo) donde es posible
"derivar" los algoritmos a partir de las pre y post-condiciones del
mismo. Pero lo que decía un profesor en la facultad (cuyo nombre voy a
mantener en el anonimato): "En el futuro no habrá programadores sino
especificadores de algoritmos" es algo que no me parece (con las leyes
de la computación en la mano) como mínimo aplicable en general.

Otra cosa es si hablamos de análisis estático del código (uso de
herramientas como PMD [3], Testability Explorer [4], etc) o de "code
coverage" (Cobertura [5], p.ej.). Ahí sí que creo que tenemos mucho
que hacer. De hecho, Eclipse ya aplica muchas de estas técnicas de
análisis estático de código para avisarnos de ramas del código que no
son ejecutables. Echad un vistazo a Preferences / Java / Compiler /
Errors-warnings / Unnecessary code y veréis que hay varias opciones
(no todas las que me gustaría, pero algo es algo).

P.ej. probad a escribir lo siguiente:

public void foo() {
int a = 0;
while ( true ) {
break;
a = 1;
}
}

Y veréis que en la última línea os avisa de que nunca va a pasar por
ahí. ¿Mola verdad?

[1] http://apuntes.rincondelvago.com/programacion-metodica.html
[2] http://www.agapea.com/libros/Programacion-metodica-isbn-8448119576-i.htm
[3] http://pmd.sourceforge.net
[4] http://code.google.com/p/testability-explorer/
[5] http://cobertura.sourceforge.net

Un saludo,
Jose Manuel Beas

http://www.agile-spain.com
http://jmbeas.blogspot.com




2009/3/25 Joserra <jrr...@gmail.com>:

[Carlos Ble]

Yo pienso mas o menos igual. Los matematicos son buenos en matematicas
pero cuando quieren que el software tambien sean matematicas .....
mala cosa. Para escribir software tambien hay que ser psicologo,
entran muchas mas variables :-)
Lo bueno de TDD es que te permite escribir codigo preparado para el
cambio. Si te tiras mucho tiempo con un algoritmo complicadisimo que
dice no se que del software y luego te piden un cambio, entonces has
vuelto al modelo waterfall y tienes un problema :-)
Saludos



El día 25 de marzo de 2009 22:00, José Manuel Beas
<jose....@gmail.com> escribió:

[Iván Párraga García]

Hola,

Yo también tengo el libro de Balcázar en mi estantería, de hecho, él fue
(un buenísimo) profesor mío en la asignatura de nombre homólogo en la
Facultad de Informática de Barcelona.

Estoy más o menos de acuerdo que generalizar ese tipo de desarrollo
puede ser utópico en general, pero puede tener algún nicho. Estoy
pensando en software crítico con especificaciones realmente cerradas,
cosas como el planificador de rutas de un misil o de un satélite de la NASA.

Con respecto a la desaparición de los informáticos... En fin, yo creo
que la tecnología siempre va avanzando y tareas que antes necesitaban de
un ingeniero ahora se "autogeneran", pero a cambio, hay nuevas
necesidades a cubrir que siguen necesitando de una "mente humana
informática". Creo que seguiremos siendo una especie necesaria (y no
sólo como especificadores de algoritmos), pero lo que está clara es que
vamos a ser "estudiantes" toda la vida.

Un saludo,

Iván

Carlos Ble escribió:

[Pablo Carranza]

La validación formal es un proceso humano que se realiza al terminar el producto, consume horas-hombre y teoricamente se realiza por la gente de QA (Quality Assurance) nunca por los desarrolladores.

El hecho de realizar una validación formal es algo que puede ser complementario a un QC (Quality Control) que se hace con TDD, es decir, a medida que se va realizando la aplicación se escriben los tests para ir probando cada pequeño trocito de código, controlando que estos funcionan correctamente y asegurandonos de esta manera que la aplicación hace lo que debe hacer.

De esta forma cuando se llega al proceso de QA ya se tiene más de medio camino andado. De manera que muy probablemente el resultado de esta validación formal sea mucho mejor que si se utiliza un modelo de cascada sin test, basado en el orgullo de que "mi código es el mejor que hay".

¿Esto indica que somos unos blanditos? pues, puede ser, yo soy tan blandito que no me gusta corregir bugs a las 11 de la noche el día antes de una entrega, que fue el día que se hizo la "validación formal" ¿a alguien le suena esto?

Luego tienes mil formas de complicarte la vida como CMMI, etc, etc.

Personalmente TDD, integración continua y agile development es la forma de hacer las cosas.

Salu2

2009/3/26 Carlos Ble <ble.j...@gmail.com>

--
Pablo Carranza
Registered Linux User #413523
http://www.zoocial.es/

[Joserra]

Pablo, con la validación formal me refería a validación matemática de
algoritmos. entradas, invariantes, salidas, etc... No sé si tú estás
hablando de eso, no me refiero a la validación por parte de un dpto.
de QA *probando* la aplicación.

Salu2!

On Mar 26, 12:07 pm, Pablo Carranza <pcarra...@gmail.com> wrote:
> La validación formal es un proceso humano que se realiza al terminar el
> producto, consume horas-hombre y teoricamente se realiza por la gente de QA
> (Quality Assurance) nunca por los desarrolladores.
>
> El hecho de realizar una validación formal es algo que puede ser
> complementario a un QC (Quality Control) que se hace con TDD, es decir, a
> medida que se va realizando la aplicación se escriben los tests para ir
> probando cada pequeño trocito de código, controlando que estos funcionan
> correctamente y asegurandonos de esta manera que la aplicación hace lo que
> debe hacer.
>
> De esta forma cuando se llega al proceso de QA ya se tiene más de medio
> camino andado. De manera que muy probablemente el resultado de esta
> validación formal sea mucho mejor que si se utiliza un modelo de cascada sin
> test, basado en el orgullo de que "mi código es el mejor que hay".
>
> ¿Esto indica que somos unos blanditos? pues, puede ser, yo soy tan blandito
> que no me gusta corregir bugs a las 11 de la noche el día antes de una
> entrega, que fue el día que se hizo la "validación formal" ¿a alguien le
> suena esto?
>
> Luego tienes mil formas de complicarte la vida como CMMI, etc, etc.
>
> Personalmente TDD, integración continua y agile development es la forma de
> hacer las cosas.
>
> Salu2
>

> 2009/3/26 Carlos Ble <ble.jur...@gmail.com>

>
>
>
>
>
> > Yo pienso mas o menos igual. Los matematicos son buenos en matematicas
> > pero cuando quieren que el software tambien sean matematicas .....
> > mala cosa. Para escribir software tambien hay que ser psicologo,
> > entran muchas mas variables :-)
> > Lo bueno de TDD es que te permite escribir codigo preparado para el
> > cambio. Si te tiras mucho tiempo con un algoritmo complicadisimo que
> > dice no se que del software y luego te piden un cambio, entonces has
> > vuelto al modelo waterfall y tienes un problema :-)
> > Saludos
>
> > El día 25 de marzo de 2009 22:00, José Manuel Beas

> > <jose.m.b...@gmail.com> escribió:

> > > 2009/3/25 Joserra <jrra...@gmail.com>:

[Pablo Carranza]

Y crees que una validación matemática va a detectar deadlocks? o stress dada una determinada carga?... yo creo que todas esas aproximaciones son muy bonitas a nivel teórico, luego está la realidad que demuestra que no se pueden probar matemáticamente todos los casos. Los matemáticos tienen ideas muy bonitas, pero de ingeniería de software saben tanto como han estudiado del tema: poco o nada.
Al menos en aplicaciones del día a día no tiene mucho sentido, para el caso del que hablaba Iván a lo sumo, aplicaciones muy específicas que realmente realizan tareas matemáticas si necesitan este tipo de validación, pero esto nuevamente tiene sentido una vez la aplicación está desarrollada. O en su defecto, si se van obteniendo resultados parciales, siempre se puede utilizar nuevamente TDD para saber que las pequeñas partes funcionan como deberían, lo cual hará que el día de mañana todo encaje.

2009/3/26 Joserra <jrr...@gmail.com>

[José Manuel Beas]

2009/3/26 Pablo Carranza <pcar...@gmail.com>:

> Y crees que una validación matemática va a detectar deadlocks? o stress dada
> una determinada carga?...

De hecho, hay libros y libros sobre modelos que se pueden hacer para
predecir la carga de un sistema y también hay algoritmos para detectar
(en un modelo) si hemos diseñado procesos que pueden llevar a un
interbloqueo. Pero esto tiene su aplicación en entornos muy acotados,
donde todas las variables que intervienen en el modelo son
controlables y las demás son despreciables (a efectos del modelo).

> yo creo que todas esas aproximaciones son muy
> bonitas a nivel teórico, luego está la realidad que demuestra que no se
> pueden probar matemáticamente todos los casos. Los matemáticos tienen ideas
> muy bonitas, pero de ingeniería de software saben tanto como han estudiado
> del tema: poco o nada.

Uy, uy, uy... que este tipo me está tocando a Turing [1] (matemático),
Knuth [2] (que primero hizo física y luego se pasó a matemáticas),
Dijkstra [3] (físico teórico, que es como decir matemático) y no sé
cuántos más...

[1] http://es.wikipedia.org/wiki/Turing
[2] http://en.wikipedia.org/wiki/Donald_Knuth#Education_and_academic_work
[3] http://es.wikipedia.org/wiki/Dijkstra

> Al menos en aplicaciones del día a día no tiene mucho sentido, para el caso
> del que hablaba Iván a lo sumo, aplicaciones muy específicas que realmente
> realizan tareas matemáticas si necesitan este tipo de validación, pero esto
> nuevamente tiene sentido una vez la aplicación está desarrollada. O en su
> defecto, si se van obteniendo resultados parciales, siempre se puede
> utilizar nuevamente TDD para saber que las pequeñas partes funcionan como
> deberían, lo cual hará que el día de mañana todo encaje.
>

Bueno, por lo que yo recuerdo, la derivación de algoritmos (a partir
de una especificación de pre y post-condiciones en un lenguaje formal)
es posible (el libro antes citado lo demuestra), pero es
computacionalmente muy costoso. Sin contar con el coste de especificar
las pre y post-condiciones. Y siempre nos quedará la duda de si hemos
puesto todas las pre y post-condiciones necesarias...

Un saludo,
JMB

[José Manuel Beas]

2009/3/26 Iván Párraga García <ivan.parr...@gmail.com>:

>
> Hola,
>
> Yo también tengo el libro de Balcázar en mi estantería, de hecho, él fue
> (un buenísimo) profesor mío en la asignatura de nombre homólogo en la
> Facultad de Informática de Barcelona.
>
> Estoy más o menos de acuerdo que generalizar ese tipo de desarrollo
> puede ser utópico en general, pero puede tener algún nicho. Estoy
> pensando en software crítico con especificaciones realmente cerradas,
> cosas como el planificador de rutas de un misil o de un satélite de la NASA.
>

100% de acuerdo (es más o menos lo que yo decía).

> Con respecto a la desaparición de los informáticos... En fin, yo creo
> que la tecnología siempre va avanzando y tareas que antes necesitaban de
> un ingeniero ahora se "autogeneran", pero a cambio, hay nuevas
> necesidades a cubrir que siguen necesitando de una "mente humana
> informática". Creo que seguiremos siendo una especie necesaria (y no
> sólo como especificadores de algoritmos), pero lo que está clara es que
> vamos a ser "estudiantes" toda la vida.
>

Bueno, aunque nos vayamos un poco fuera del asunto de este hilo,
separemos la generación de código (que viene a ser como una ayuda,
pero que, tal y como yo lo veo, no mejoran significativamente el
resultado final) de la "captura de requisitos".

Me gustaría recomendar el libro "Bridging the Communication Gap" donde
el autor habla de las especificaciones ejecutables y de las pruebas
exploratorias. Las primeras serían ejemplos de uso del sistema que
explican qué debe hacer para cubrir las funcionalidades solicitadas
(requisitos) y que además haremos ejecutables de manera automática
(sin intervención humana). Las segundas serían las que solemos hacer
manualmente, las típicas UATs (a las que se refiere Pablo como
"validaciones formales") pero que no pueden ser exhaustivas porque
disparan el coste y también están sujetas al fallo humano.

Una de las ventajas de las primeras es que sirven para aclarar qué hay
que hacer y, más importante aún, qué NO hay que hacer. Nunca entran en
el cómo, sólo en el qué. Y en ese sentido son un poco TDD, puesto que,
con antelación a tener el sistema explicas qué quieres que haga. Más
adelante, los desarrolladores lo implementan COMO ellos decidan
(individual o colectivamente, ya sea tomando decisiones de diseño o
asumiendo las de un arquitecto, quizás).

Corolario: Es mejor impedir que surjan los defectos (con buenas
prácticas, buenos diseños, aclarando lo que hay que hacer y lo que
no...) que perseguir los defectos (porque alguno se nos puede
escapar).

Perdón por la chapa, pero es que este tema me apasiona.

[Pablo Carranza]

2009/3/26 José Manuel Beas <jose....@gmail.com>

Con lo cual estas diciendo también que a nivel teórico muy bonito, a nivel práctico y realista es costoso o no realizable....

Saludos.

[José Manuel Beas]

2009/3/26 Pablo Carranza <pcar...@gmail.com>:

> 2009/3/26 José Manuel Beas <jose....@gmail.com>
>>
>>

>> Bueno, por lo que yo recuerdo, la derivación de algoritmos (a partir
>> de una especificación de pre y post-condiciones en un lenguaje formal)
>> es posible (el libro antes citado lo demuestra), pero es
>> computacionalmente muy costoso. Sin contar con el coste de especificar
>> las pre y post-condiciones. Y siempre nos quedará la duda de si hemos
>> puesto todas las pre y post-condiciones necesarias...
>>
>> Un saludo,
>> JMB
>
> Con lo cual estas diciendo también que a nivel teórico muy bonito, a nivel
> práctico y realista es costoso o no realizable....
>
> Saludos.
>

Bueno, no exactamente, en el último post creo que lo decía mejor, pero
básicamente mi opinión es que sí tiene una aplicación práctica, pero
en entornos muy específicos donde todas las condiciones están muy
controladas y es vital asegurar el buen funcionamiento de los
algoritmos. Pero lo cierto es que no hablo ni de oidas siquiera puesto
que no conozco ningún ejemplo de aplicación práctica de la
"programación metódica", así que quizás tengas tú razón... :-)

[Jose R.]

Y crees que una validación matemática va a detectar deadlocks? o stress dada una determinada carga?... yo creo que todas esas aproximaciones son muy bonitas a nivel teórico, luego está la realidad que demuestra que no se pueden probar matemáticamente todos los casos. Los matemáticos tienen ideas muy bonitas, pero de ingeniería de software saben tanto como han estudiado del tema: poco o nada.

 No tengo ninguna duda de que se puede hacer lo que preguntas a nivel teorico, quizás no tengamos suficiente capacidad de computación para simularlo y por lo tanto, sí, te doy la razón que entonces no es algo real. PERO eso es de momento! :)
 Yo sospecho que somos los ingenieros de software los que sabemos poco de matemáticas, y no nos vendría algo mal algo más... Al final todo lo que se ejecuta en un chip son cuestiones matemáticas...

 Ya habeis hablado del gran personaje en estos temas (casi filosóficos), siempre después de leer a Dijkstra me queda un sabor agridulce. [1].

  Salu2!


[1] http://www.smaldone.com.ar/documentos/ewd/sobre_la_crueldad.html

 

[José Manuel Beas]

2009/3/26 Jose R. <jrr...@gmail.com>:

>
>
>  Ya habeis hablado del gran personaje en estos temas (casi filosóficos),
> siempre después de leer a Dijkstra me queda un sabor agridulce. [1].
>
>   Salu2!
>
>
> [1] http://www.smaldone.com.ar/documentos/ewd/sobre_la_crueldad.html
>
>

Hacía tiempo que no leía algo tan inspirador. Muchas gracias, Jose Ramón.

[Carlos Ble]

La verdad que no me he leido el enlace, pero si impartiesen todavía
mas clases de mates en la carrera vomitaria :-S

Saludos :-)

[Joserra]

> La verdad que no me he leido el enlace, pero si impartiesen todavía
> mas clases de mates en la carrera vomitaria :-S

:D :D Creo que lo malo es el enfoque de las que damos :)

Salu2!

[Pablo Carranza]

Hay mucho de eso, lamentablemente muchos profesores en la facultad consiguen que los alumnos pierdan el interes en aprender.

Salu2

2009/3/27 Joserra <jrr...@gmail.com>