[Practico 5] Ej 7

[Practico 5] Ej 7

de Pablo Daniel Martinez Arevalo -
Número de respuestas: 1

Cuando tengo que definir el xWhile lo puedo hace así

| xWhileTrue : forall (c : BoolExpr) (m m1 m2 : Memory) (p : Instr),

      BEeval c m true -> Execute p m m1 -> Execute (IWhile c p) m1 m2 -> Execute (IWhile c p) m m2

o así

| xWhileTrue : forall (c : BoolExpr) (m m1 m2 : Memory) (p : Instr),

      BEeval c m true -> Execute p m m1 -> Execute (IWhile c p) m1 m2 

las dos opciones son correctas?

En respuesta a Pablo Daniel Martinez Arevalo

Re: [Practico 5] Ej 7

de Carlos Luna -

Hola.

La opción correcta (que se corresponde con la semántica dada para el while cuando es true) es la primera. Notar que en la segunda opción m2 no tendría relación con lo que pasa antes (en la ejecución de un paso).

Saludos, Carlos