Cálculo de Hoare

Para cada um dos programas P seguintes verifique, recorrendo ao cálculo de Hoare, que estão parcialmente correctos face às condições iniciais (C1) e objectivo (C2) indicadas.

Nos exercícios que se seguem as variáveis N, X e Y denotam inteiros, a variável W uma lista de inteiros e a variável M uma matriz.

Programas sobre inteiros

Cálculo do factorial

P:=Module[{i},i=N;
r=1;
While[i>0,
r=r i;
i=i-1
]
];

C1=N≥0;

C2=(r==(∏_(K=1)^N)K).

Exponenciação

P:=If[y<0,
Null,
z=1;
w=y;
While[y≠0,
y=y-1;
z=z x
];
y=w
];

C1=(x==X∧y==Y∧Y≥0);

C2=(z==(X^Y)∧w==Y∧y==Y).

Programas sobre listas

Comprimento duma lista

P:=Module[{aux},
aux=W;
r=0;
While[aux≠{},
r=r+1;
aux=Rest[aux]
];
];

C1=True;

C2=(r==Length[W]).

Soma duma lista

P:=Module[{aux},
aux=W;
r=0;
While[aux≠{},
r=r+First[aux];
aux=Rest[aux]
]
];

C1=True;

C2=(r==(∑_(K=1)^(Length[W]))W[[K]]).

Soma dos elementos em posições pares

P:=Module[{i},
i=1;
r=0;
While[i≤Length[W],
If[EvenQ[i],
r=r+W[[i]],
Null];
i=i+1
];
];

C1=True;

C2=(r==(∑_(K=1)^(⌊((Length[W])/2)⌋))W[[2K]]).

Soma dos elementos pares duma lista

P:=Module[{i},
i=1;
r=0;
While[i≤Length[W],
If[EvenQ[W[[i]]],
r=r+W[[i]],
Null];
i=i+1
];
];

C1=True;

C2=(r==(∑_(K=1)^(Length[W]))If[EvenQ[W[[K]]],W[[K]],0]).

Inversão duma lista

P:=Module[{i},
i=1;
r={};
While[i≤ Length[W],
r=Prepend[r,W[[i]]];
i=i+1
]
];

C1=True;

C2=(r==(Underoverscript[∧, (K=1), (Length[W])])r[[Length[W]-K+1]]==W[[K]]).

Máximo duma lista

P:=Module[{i},
i=2;
r=W[[1]];
While[i≤ Length[W],
If[r<W[[j]],
r=W[[j]],
Null];
i=i+1
]
];

C1=W≠{};

C2=(((Underoverscript[∧, (K=1), (Length[W])])r≥W[[K]])∧((Underoverscript[∨, (K=1), (Length[W])])r==W[[K]])).

Supremo duma lista

P:=Module[{aux},
aux=W;
r=-Infinity;
While[aux≠{},
If[r<First[aux],
r=First[aux],
Null];
aux=Rest[aux]
]
];

C1=True;

C2=(r==sup[W]);

onde a função sup retorna o supremo da lista argumento.

Procura numa lista

P:=Module[{aux},
aux=W;
r=False;
While[aux≠{},
r=r∨(x==First[aux]);
aux=Rest[aux]
]
];

C1=True;

C2=(r==(Underoverscript[∨, (K=1), (Length[W])])x==W[[K]]).

Procura dum primo numa lista

P:=Module[{aux},
aux=W;
r=False;
While[aux≠{},
If[PrimeQ[First[aux]],
r=True,
Null];
aux=Rest[aux]
]
];

C1=True;

C2=(r==(Underoverscript[∨, (K=1), (Length[W])])PrimeQ[W[[K]]]).

Média dos elementos duma lista

P:=Module[{i},
i=2;
r=W[[1]];
While[i≤Length[W],
r=r+W[[i]];
i=i+1
];
r=r/Length[W]
];

C1=W≠{};

C2=(r==(((∑_(K=1)^(Length[W]))W[[K]])/(Length[W]))).

Programas sobre matrizes

Traço duma matriz

P:=Module[{i},
i=1;
r=0;
While[i≤Length[M],
r=M[[i,i]];
i=i+1
];
];

C1=sqmQ[M];

C2=(r==(∑_(K=1)^(Length[M]))M[[K,K]]);

onde o predicado sqmQ indica se uma matriz é quadrada.

Exercícios de exame

Exame-tipo (2001/2002)

P:=Module[{i},
i=1;
r=0;
While[i≤N,
r=r+i;
i=i+1
]
];

C1=N≥0;

C2=(r==(∑_(K=1)^N)K).

Exame A, 21/01/2002

P:=Module[{i},
i=1;
r=0;
While[i≠Length[W]+1,
r=r+W[[i]];
i=i+1
]
];

C1=W≠{};

C2=(r==(∑_(K=1)^(Length[W]))W[[K]]).

Exame B, 21/01/2002

P:=Module[{i},
i=1;
r=1;
While[i≠Length[W]+1,
r=r*W[[i]];
i=i+1
]
];

C1=W≠{};

C2=(r==(∏_(K=1)^(Length[W]))W[[K]]).

Exame A, 06/02/2002

P:=Module[{i},
i=1;
r=False;
While[i≤ Length[W],
r=r∨(x==W[[i]]);
i=i+1
]
];

C1=W≠{};

C2=(r==(Underoverscript[∨, (K=1), (Length[W])])x==W[[K]]).

Exame B, 06/02/2002

P:=Module[{i},
i=0;
r=True;
While[i< Length[W],
i=i+1;
r=r∧(x==W[[i]])
]
];

C1=W≠{};

C2=(r==(Underoverscript[∧, (K=1), (Length[W])])x==W[[K]]).