En Thu, 17 Sep 2009 11:56:38 -0300, Claudio Freire
<klaussfreire@???> escribió:
> 2009/9/16 Facundo Batista
> <facundobatista@???>
>
>> 2009/9/16 Charif Mauricio Nadir
>> <mry.shariff@???>:
>>
>> > El uso de la sentencia break está considerada como una mala práctica,
>> al
>> > igual que continue. El flujo de un programa debe ser fácil de seguir
>> sin
>> > saltos y sin interrumpir el flujo de las estructuras de control.
>>
>> No estoy de acuerdo.
>>
> El problema de los while True y los breaks es que hacen el análisis de
> correctitud y terminación por invariantes casi imposible.
> Están deprecados en el mundo de la programación porque es muy difícil,
> leyéndolos, asegurar que no es un loop infinito, y que cuando sale el
> invariante (si hay) se cumple.
Epa, no es para tanto, y más si sólo nos restringimos a la variante de
break y continue que existe en Python (sólo se puede salir o continuar el
bucle más anidado). Acá [1] se presenta una formalización de la semántica
del while con break/continue/return y excepciones para Java, pero se
aplica igual a Python (tanto como se pueda aplicar una teoria
originalmente pensada para lenguajes mucho mas restrictivos y simples...)
Para demostrar la corrección parcial, hay que tener en cuenta los 'break'
y asignarles una condición a cada uno (básicamente el 'if' previo que lo
dispara, en la gran mayoria de los programas) que pasa a ser la
postcondicion del bucle. Sí, ya no se puede considerar el cuerpo del bucle
como una "caja negra", hay que mirar qué tiene adentro... pero no es tan
dramático :)
O sea, se agrega una regla más para el while. La regla "normal" es:
{P and C} S {P}
---------------------
{P} while C: S {P and not C}
Y la regla "salida por break" es (un poco simplificada):
{P and C} S {P and C} # porque sigue dentro del bucle
{P and C} S {break(Q)}
---------------------
{P and C} while C: S {break(Q)}
[1] M. Huisman, B.P.F. Jacobs. Java Program Verification via Hoare Logic
with Abrupt Termination.
http://eprints.kfupm.edu.sa/47284/1/47284.pdf
>> ...
>> while True:
>> edad = raw_input(mssg)
>> if edad.isdigit():
>> break
>>
>> print "no nro"
>>
> Aquí, claro está, realmente podría ser un loop infinito (el usuario nunca
> tipea un número), y el único invariante deseado es "edad.isdigit()" -
> nuevamente, ese while True hace menos evidente que al salir del loop,
> edad
> es en efecto un número.
Que el bucle termina es imposible de probar, asi que solo importa
demostrar correccion parcial. El invariante P sería "la variable edad no
existe o todos sus valores previos fueron no numericos". O termina
normalmente, o termina por el break. Termina normalmente por (not True) --
o sea, nunca :) . La precondicion de break es edad.isdigit(), y la regla
de derivacion de arriba dice que, SI sale del bucle por un break, se
cumple que edad.isdigit(). O sea, SI sale del bucle, edad es un numero.
--
Gabriel Genellina
---------------------------------------------------------------------
Para dar de baja la suscripcion, mande un mensaje a:
pyar-unsubscribe@???
Para obtener el resto de direcciones-comando, mande un mensaje a:
pyar-help@???
PyAr - Python Argentina - Sitio web:
http://www.python.com.ar/
(text/plain)