SmallLang

Lenguaje similar a C++.

• Un programa es una instrucción
  1. Asignación: x := E
  2. Nada: skip
• Estructuras de control
  1. Secuencia: S1; S2 es una programa si S1 y S2 son dos programas.
  2. Condicional: if B then S1 else S2 endif
  3. Ciclo: while B do S endwhile

Transformación de estados

Llamamos estado de un programa a los valores de todas sus variables en un punto de su ejecución.

Podemos considerar la ejecución de un programa como una sucesión de estados.

La asignación es la instrucción que permite pasar de un estado al siguiente en esta sucesión de estados.

Las estructuras de control se limitan a especificar el flujo de ejecución.

Corrección de un programa

• Definición:

  Decimos que un programa $S$ es correcto respecto de una especificación dada por una precondición $P$ y una postcondición $Q$, si siempre que el programa comienza en un estado que cumple $P$ el programa termina su ejecución y en el estado final se cumple $Q$.

• Notación: $\{P\} S \{Q\}$ si y solo si $S$ es correcto (tripla de Hoare).

Correción de alternativas

Cuando tenemos un condicional tenemos que considerar las dos alternativas por separado.

Ciclos

while (guarda B) {
	cuerpo del ciclo S
}

• El cuerpo del ciclo $S$ se repite mientras la guarda $B$ se cumpla. A cada repetición la llamamos iteración.
• La ejecución del ciclo termina si no se cumple la guarda al comienzo de la ejecución o bien luego de una de las iteraciones.
• Cuando el ciclo termina el estado resultante es el estado posterior a la última instrucción del cuerpo del ciclo.