Completar de forma apropiada la lineas punteadas de la siguiente de dem de correctitud
problema maximo3(a,b,c:Z) == res : Bool {
asegura res == max(a,max(b,c));
}
int maximo·(int a, int b, int c)
{
int r;
//estado E1
if(a < b)
{
if(b < c) r = c;
else r = b;
}
else
{
if(a < c) r = c;
else r = a;
}
//vale r = = max(a,max(b,c))
return r;
//vale ...;
}
Estos son mis intentos de resolución
caso en el que la guarda de if(a < b) es True
//estado E1
//vale a < b
if(b<c)
r = c;
else
r = b;
//vale r == max(b,c)
//dado que a < b ^ r == max(b,c)
//implica r > a ^ r == max(b,c)
//implica r == max(a, max(b,c))
caso en el que la guarda de if(a < b) es False
//estado E1
//vale not(a < b)
if(a<c)
r = c;
else
r = a;
//vale r == max(a,c)
//dado que not(a<b) ^ r == max(a,c)
//implica a >= b ^ r == max(a,c)
//implica r >= b ^ r == max(a,c)
//implica r == max(b, max(a,c))
caso en el que la guarda de if(b<c) es True
//estado E1
//vale a < b
//vale b < c
r = c;
//vale r == c
//vale c == c@E1
//implica r == max(c,b)
//implica r == max(a, max(c,b))