ENIGMA SOBRE C . Terminación de programas

[dijsktra]

Hola!

En una facultad de Madrid me he encontrado pinchado en el panel este original reto...
Está en inglés, pero creo que se entiende...

• El primer problema pide demostrar que el programa dado acaba
• El segundo dice que cuando acabe, el sistema sacará la llamada correspondiente al assert.  

Alguna propuesta ?

[MAFUS]

El segundo ejemplo no debería parar y el assert(1) no debería fallar.

[EdePC]

Saludos,

- El FOR requiere de ( Sentencia; Condicion; Sentencia ), tengo entendido de que las Sentencias pueden quedar vacías, lo he visto mucho en javascript.

-- En el primer caso es un bucle que no se cumple, la condición es 0 o FALSE

-- En el segundo caso el bucle en infinito y nunca llega a ejecutarse el assert(1)

- Entonces pienso que el libro se refiere a un problema de compilación, pero mi compilador MinGW no me ha dado ningún problema. Algo así como decir que se está importando tal cosa y no se está usando, o se ha detectado un bucle infinito, o se ha detectado una sentencia de código ( assert(1) ) que nunca se ejecutará debido x razón, etc.

---

- También me parece sospechoso ese ; al final del FOR, supongo que dependiendo del tema del libro, podría estar explicando que el ; da por finalizado el Bucle en esa misma línea y no ejecuta nada más, es decir, ese FOR no tiene cuerpo a ejecutar:

Código (c) [Seleccionar] Expandir

for ( sentencia, condicion, sentencia ) ;

for ( sentencia, condicion, sentencia )
  cuerpo a ejecutar

for ( sentencia, condicion, sentencia ) {
  cuerpo a ejecutar
}

for ( sentencia, condicion, sentencia ) ;
  esta sentencia no pertenece al FOR y es independiente

for ( sentencia, condicion, sentencia ) ; {
  esta sentencia no pertenece al FOR y es independiente
}


[K-YreX]

Al primer ejemplo no le veo mucha complicación, un <for> se ejecuta mientras la condición (segundo campo del <for>) sea verdadera (1). Los campos de inicialización (primer campo) y actualización (tercer campo) pueden quedarse vacíos como es el caso aunque siempre se ha comentado que no es una buena práctica ya que en otros lenguajes no está permitido este uso.
Se ejecuta el <for> y como la condición es falsa (0) termina y sale.

En cambio, en el segundo ejemplo es todo lo contrario, el <for> no termina nunca ya que la condición es siempre verdadera (1) y como ya ha comentado EdePC, como el <for> acaba en punto y coma ( la instrucción del <assert(1)> no se ejecutará nunca ya que no pertenece al cuerpo del <for> y este genera un bucle infinito.

[Loretz]

El primer caso a mí me parece lo mismo; para el segundo lo único que se me ocurre es que alguien ha estado jugando con <assert>, así que si yo también...

Código (c) [Seleccionar] Expandir

#include <stdio.h>
#include <string.h>

#define __FILENAME__ (strrchr(__FILE__, '\\') ? strrchr(__FILE__, '\\') + 1 : __FILE__)

#define assert(expression) (void)((!(expression)) || (mostrar(#expression, __FILENAME__, (unsigned)(__LINE__), __func__), 0))

#define for(a) while(0)

void mostrar(const char* message, const char* file, int line, const char* function)
{
    printf("%s: %s:%i: %s: Assertion \'%s\' failed\n", function, file, line, function, message);
}

int main()
{
    for( ;1; );

    assert(1);
}

[dijsktra]

Chicos, gracias por vuestras repuestas.
 Loretz, muy buena tu exhibición, pero el ejercicio que propones no cumple lo que dice, porque YA es otro fichero fuente del que se propone...

Creo que hay que hacerlo sobre el mismo contenido del original y lo que me choca más... se supone que no vale argûir "Alguien ha jugado con el assert, pues yo también...", porque el sistema ha de ser compatible ANSI-C/ISO-C, o sea, el assert tiene que hacer lo que se espera de él...

Os digo mis progresos:

• Es un absurdo esperar a que acabe un programa que no acaba. Todo el mundo está de acuerdo en que el bucle es infinito.
• Es un absurdo esperar que assert falle cuando el parámetro sea 1, ya que sólo falla cuando vale 0, según el ANSI-C/ISO-C

No hay manera de relacionar estos absurdos entre sí? Me huelo que "por aquí va la tostada", rollo lógica....

En cuanto tenga algo os lo paso...

El primer caso a mí me parece lo mismo; para el segundo lo único que se me ocurre es que alguien ha estado jugando con <assert>, así que si yo también...

Código (c) [Seleccionar] Expandir

#include <stdio.h>
#include <string.h>

#define __FILENAME__ (strrchr(__FILE__, '\\') ? strrchr(__FILE__, '\\') + 1 : __FILE__)

#define assert(expression) (void)((!(expression)) || (mostrar(#expression, __FILENAME__, (unsigned)(__LINE__), __func__), 0))

#define for(a) while(0)
...


[Serapis]

Esto son temas de sobra conocidos en teoría de compiladores.

El primer tema a considerar: Los bucles infinitos versa que si el incremento es 0 y el valor inicial es igual al valor final, no es un bucle infitio, en otro caso si:
       bucle infinito = ((inc = 0) and (inicio <> final))
...y si el cuerpo está vacío (como es el caso), o no existe dentro una sentencia de escape del bucle (si existe, deberá examinarse también). Lógicamente en tiempo de compilación...
       Por eso no se cumple en el primer caso y sí en el segundo.

Los bucles infinitos de este modo, en realidad pueden ser tomados como bucles incondicionales (tipo do...loop) y han sido la solución para lenguajes en los que no existen otro tipo de bucles que no sean condicionados por una expresión aritmética pero que si admiten una sentencia de salida del mismo controlados por algún 'if then else'.

El segundo tema a considerar: En teoría de compiladores se trata en la optimización de código, para eliminar código redundante o código inaccesible. Código inaccesible es aquel que nunca se va a ejecutar, caso por ejemplo como:

Código [Seleccionar] Expandir


int x = 20
si x = 0
   ...
fin si
El compilador detectará que si a x se el asigna la constante 20, no puede tener de inmediato la contante 0, luego todo el código dentro del condicional incluído el condicional, puede ser omitido.
Piénsese que los condicionales 'if then', a efectos prácticos pueden considerarse bucles de 0 ó 1 ciclos.

Desde el momento en que entras en un bucle infinito, el código que venga detrás se vuelve inaccesible, que es lo que pasa en el segundo ejemplo.

[dijsktra]

Hola NEBIRE

...

El primer tema a considerar: Los bucles infinitos versa que si el incremento es 0 y el valor inicial es igual al valor final, no es un bucle infitio, en otro caso si:
      bucle infinito = ((inc = 0) and (inicio <> final))
...y si el cuerpo está vacío (como es el caso), o no existe dentro una sentencia de escape del bucle (si existe, deberá examinarse también). Lógicamente en tiempo de compilación...
      Por eso no se cumple en el primer caso y sí en el segundo.
...

Esta propuesta no vale. Estás describiendo un caso muy partícular de bucles "for", los que se parecen /ajustan al patrón de Pascal

Código [Seleccionar] Expandir


for < variable-name > := < initial_value > to [down to] < final_value > do
  S;


Pero en el caso de C que se da, que variables hay?, cual es el valor inicial y/o final?
En C, el bucle for es tan versátil/expresivo como el while.

EScrito de otro modo, en el primer caso hay que explicar por qué el bucle C, acaba:

Código (c) [Seleccionar] Expandir

while (0) ;

Aqui no hay duda de que no hay valores iniciales, ni finales.... Solo constantes.

[MAFUS]

Yo lo veo una proposición más filosófica que práctica.
Ya de por sí la premisa, sobre el segundo fuentes, es falsa porque ese bucle no terminan nunca, al tener en la condición un 1 y por tanto siempre será cierta. Pero en ese mismo fuente se podría considerar que 1 es falso ya que ese valor detiene el bucle y, además, hace saltar al assert. Y ya que el 1 del for y el 1 del assert son diferentes por ser dos objetos diferentes pero con el mismo símbolo (es decir, no son una posición de memoria que por alguna razón ajena al programa ha cambiado, sino que realmente es 1) entonces 1 es 0.
En ese supuesto, imposible por otra parte, sí que se llegaría a la solución propuesta.

[dijsktra]

Exacto MAFUS! Lo has clavado!

Yo lo veo una proposición más filosófica que práctica.
Ya de por sí la premisa, sobre el segundo fuentes, es falsa porque ese bucle no terminan nunca, al tener en la condición un 1 y por tanto siempre será cierta. Pero en ese mismo fuente se podría considerar que 1 es falso ya que ese valor detiene el bucle y, además, hace saltar al assert. ...
En ese supuesto, imposible por otra parte, sí que se llegaría a la solución propuesta.

Bueno, creo que ya lo tengo, chicos. Me han ayudado un poco por ahí... Y cuando lo entiendes, es una pura broma....

La cuestión tiene que ver no tanto con C, como con dos aspectos de la algoritmia:

• la terminación de un programa
• la corrección parcial, que nos dice que si acaba, (notese la cursiva) entonces el programa computa lo que se espera de él.  

Las dos cuestiones son ciertas. Empiezo por la más extraña, la segunda, la del bucle infinito.

• Según el estandar ANSI-C, asssert solo falla cuando la evaluación del parámetro da 0 (false). En nuestro caso, assert(1), cuando 1==0, lo que es un absurdo  
• Según el estandar ANSI-C, el bucle acaba cuando la parte del discriminante da 0 (false) . En nuestro for( ; 1; ), caso, cuando 1==0 , (en terminos prácticos, nunca)  
• O sea, que cuando el bucle acabe, (no dice que acabe, dice que cuando acabe, esto es importante!) se cumplirá   1==0, lo que es la condición para que assert(1) falle.  

Esta bien el enigma... A nadie engaña por decir que esperando lo suficiente, el assert(1) fallará... Eso sí, tiene que esperar lo suficiente, por los siglos de los siglos...

Formalmente, pura lógica...

Código [Seleccionar] Expandir



(Short proof)
    1=0 |= 1=0  q.e.d  

(Full proof)

Let Post Q:1=0 .

Then we have to proof that

 { I } for( ; 1 ; ) { Q } (Partial correctness, no matter I)

 1. { I } skip {I}  SKIP
 2. I and 1=1 -> I (Logic, stronger antecedent )
 3. { I and 1=1 } skip { I } STREN(1,2)
 4. I and 1=0 -> 1=0 (Logic, false (or stronger) antecedent)
 5. { I } for( ; 1 ; ) { 1=0 }  WHILE(3,4)

 q.e.d

Remark: ANSI-C states
    * assert(1) call does fail when 1=0 ("never")
    * loop for( ;1;) does end when 1=0 ("never" ;-D)
    * empty loop's body is skip.

El primer problema, que todos veíamos que acababa, también es parecido...pero ahora si nos interesa demostrar que efectivamente acaba, y nos da igual lo que pase al acabar.

En los libros de algoritmia se dice que para que un bucle acabe (terminación) tenemos que idear una quota definida positiva en el punto antes de evaluar la condición de salida  (un invariante). Como no hay variables, escogemos como quota C(n)=0... Esta quota tiene que disminuir cada vuelta, es decir 0 < 0, lo que es un absurdo.
Como va a disminuir cada vuelta, si nunca entra? Bueno, seg'un el estandar ANSI entra cuando la evualuación de la guarda es  distinta de 0, nuestro caso for( ; 0 ; ) , cuando 0!=0 (o sea nunca).

El resultado es que cuando 0!=0 entonces ocurrirá que 0 < 0. No dice que 0!=0, sino que cuando 0!=0, absurdo, entonces 0<0 (otro absurdo). Genial!  Pura lógica.

Código [Seleccionar] Expandir



(Short proof)

  0!=0 |= 0 < 0   q.e.d.

(Full proof)

Let C()=0 >= 0 positively defined, i.e.

     I -> 0 >= 0  (no matter I)
     
Then we have to proof

    { I and 0!=0 and 0=0 } skip { 0 < 0} (Quota indeed decreases)

   1. { 0 < 0 } skip { 0 < 0 } (SKIP)
   2. I and 0!=0 and 0=0 -> 0 < 0  (Logic, false antecedent)
   3. { I and 0!=0 and 0=0 } skip { 0 < 0 } (STRENG(2,1))

   q.e.d

Remark :   * ANSI-C states the loop is entered
          when 0!=0, i.e. "never" ;-D
  * empty loop's body is "skip"