Correción de programas

Expresar en el lenguaje de Dijkstra la ejecución de dos comandos en orden indeterminado. Analizar su wp.
Demostrar si el orden de ejecución altera el efecto de los siguientes pares de comandos:
1. A:=B; C:=D
2. A:=A+1; A:=A-1;
3. A:=B; B:=A;
A que commandos en el lenguaje de Dijkstra corresponden las siguientes construcciones. Justificar:
1. if fi
2. do od
Hallar una precondición para que: do A→ B:=B * 2; A:=False od
1. termine en un ciclo con B positivo.
2. Itere exactamente dos veces y B sea positivo
3. cicle más de una vez con B positivo
Hallar la precondición para que:
1. if X > 1 → X := X + 1 fi con poscondición X par
2. do X > 0 → X := X - 1 od termine, ciclando más de una vez
Verificar si los siguientes programas son correctos:
1. programa que halla el mayor entre dos nros
2. programa que halla el mayor entre tres nros
3. programa que ordena dos nros
Hallar la propiedad invariante y la función variante de los siguientes ciclos:
1. programa que halla el cociente entre A y B en función de la resta, donde A pertenece a los Naturales con el cero y B pertenece a los Naturales
2. programa que halla el producto de A y B en función de la suma, donde A pertenece a los Enteros y B pertenece a los Naturales con cero
3. programa que halla el máximo común divisor entre dos nros Naturales aplicando el algoritmo de Euclides