Resolução da 8ª Aula Prática

Resoluções

1.a) a 1.c) Ver ex1abc.C.

0 - Começa por se escrever o esqueleto da função:

/** Indica se o argumento é um número natural primo.   @pre ?.   @post ?.*/ bool ePrimo(int const n) {     assert(?);

    bool e_primo = ?;

    ...

    return e_primo; }
1 - Definição da pré-condição e da condição objectivo da função:

A pré-condição, como indicado no enunciado, é que

PC: 1 <= n.

A condição objectivo, também de acordo com o enunciado, é

CO: ePrimo = (2 <= n e (Q j : 2 <= j < n : n ÷ j <> 0)).

Pode-se simplificar a resolução do problema resolvendo o caso de n < 2 à parte, recorrendo a uma instrução condicional:

/** Indica se o argumento é um número natural primo.   @pre 1 <= n.   @post ePrimo = (2 <= n e (Q j : 2 <= j < n : n ÷ j <> 0)).*/ bool ePrimo(int const n) {     assert(1 <= n);

    if(n < 2)         return false;

    // PC: ?.    bool e_primo = ?;

    ...

    // CO: ?.    return e_primo; }

Neste momento a atenção pode-se centrar na parte restante do código, antes da instrução de retorno. Nesse caso, é evidente que:

PC: 2 <= n.

CO: e_primo = (Q j : 2 <= j < n : n ÷ j <> 0).

É ainda possível simplificar esta condição objectivo. Se um determinado j for divisor de n, então existe um k inteiro tal que j × k = n. Suponha-se que j é tal que n < j × j, ou seja, n^½ < j. Então, como k = n / j, tem-se que k < n / n^½, ou seja, k < n^½. Portanto, se existir um n^½ < j tal que n ÷ j = 0, então também existe um k < n^½ tal que n ÷ k = 0. Isto significa que, para que 2 <= n seja primo, basta que não seja divisível por nenhum inteiro 2 <= j <= n^½, não sendo necessário verificar os inteiros entre n^½ exclusive e n exclusive. Ou seja, a condição objectivo pode ser reescrita como

CO: e_primo = (Q j : 2 <= j <= n^½ : n ÷ j <> 0),

que é equivalente a

CO: e_primo = (Q j : 2 <= j < n^½ + 1 : n ÷ j <> 0).

dado que j só pode tomar valores inteiros.
2 - É necessário um ciclo? Problema interessante!
3 e 4 - Determinação da condição invariante e da guarda do ciclo:

Pode ser feita substituindo uma constante por uma variável. Como n é constante, n^½ + 1 também o é, e por isso pode-se substitui por uma variável:

CI: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i <= n^½ + 1.

A guarda deve ser escolhida por forma a que CI e ¬G implica CO. Neste caso a escolha é não simples, pois n^½ + 1 pode tomar valores não inteiros. O que se pretende, na realidade, é que i termine o ciclo com um valor tal que j < i seja o mesmo que j < n^½ + 1. Mas isso é o mesmo que dizer que n^½ + 1 <= i < n^½ + 2, que é o mesmo que n^½ < i <= n^½ + 1. Assim, a escolha da negação da guarda torna-se evidente:

¬G: n^½ < i, ou seja,
G: i <= n^½, ou seja,
G: i × i <= n.

O corpo da função é então:

/** Indica se o argumento é um número natural primo.   @pre 1 <= n.   @post ePrimo = (2 <= n e (Q j : 2 <= j < n : n ÷ j <> 0)).*/ bool ePrimo(int const n) {     assert(0 <= n);

    if(n < 2)         return false;

    // PC: 2 <= n.    bool e_primo = ?;     int i = ?;

    while(i * i <= n) {

        ...

    }

    // CO: e_primo = (Q j : 2 <= j <= n^½ : n ÷ j <> 0).    return e_primo; }
5 - Escolha da inicialização:

A inicialização é muito simples: basta inicializar i com 2 e e_primo com V:

    bool e_primo = true;     int i = 2;

Nesse caso tem-se:

CI: V = (Q j : 2 <= j < 2 : n ÷ j <> 0) e 2 <= 2 <= n^½ + 1, ou seja,
CI: V = V e 1 <= n^½, ou seja,
CI: 1 <= n, ou seja,
CI: V, pela pré-condição.

O corpo da função fica:

/** Indica se o argumento é um número natural primo.   @pre 1 <= n.   @post ePrimo = (2 <= n e (Q j : 2 <= j < n : n ÷ j <> 0)).*/ bool ePrimo(int const n) {     assert(1 <= n);

    if(n < 2)         return false;

    // PC: 2 <= n.    bool e_primo = true;     int i = 2;

    while(i * i <= n) {

        ...

    }

    // CO: e_primo = (Q j : 2 <= j <= n^½ : n ÷ j <> 0).    return e_primo; }
6- Determinação do progresso:

O progresso deve ser escolhido de forma a garantir que o ciclo termina. É evidente que a simples incrementação de i é suficiente para o garantir.
7 - Determinação da acção:

A acção deve ser escolhida de modo a garantir que a condição invariante se mantém verdadeiro no final do passo, apesar do progresso. Ou seja, pretende-se que:

// CI e G: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i <= n^½ + 1 e i <= n^½, ou seja,
// CI e G: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i < n^½ + 1.
acção
++i;// CI: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i <= n^½ + 1.

Determinando a pré-condição mais fraca do progresso

// e_primo = (Q j : 2 <= j < i + 1 : n ÷ j <> 0) e 2 <= i + 1 <= n^½ + 1, ou seja,//e_primo = (Q j : 2 <= j < i + 1 : n ÷ j <> 0) e 1 <= i < n^½ + 1.++i;// CI: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i <= n^½ + 1,

conclui-se que é necessário escolher uma acção tal que

// CI e G: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i < n^½ + 1.
acção
// e_primo = (Q j : 2 <= j < i + 1 : n ÷ j <> 0) e 1 <= i < n^½ + 1.

É evidente então que a acção deve ser

e_primo = e_primo and n % i != 0;

pois determinando a pré-condição mais fraca

// e_primo e n ÷ i <> 0 = (Q j : 2 <= j < i + 1 : n ÷ j <> 0) e 1 <= i < n^½ + 1.e_primo = e_primo and n % i != 0; //e_primo = (Q j : 2 <= j < i + 1 : n ÷ j <> 0) e 1 <= i < n^½ + 1.

conclui-se que

CI e G: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i < n^½ + 1,
implica
e_primo e n ÷ i <> 0 = (Q j : 2 <= j < i + 1 : n ÷ j <> 0) e 1 <= i < n^½ + 1.

ou seja, conclui-se que

// CI e G: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i < n^½ + 1.
e_primo = e_primo and n % i != 0; //e_primo = (Q j : 2 <= j < i + 1 : n ÷ j <> 0) e 1 <= i < n^½ + 1.++i; //CI: e_primo = (Q j : 2 <= j < i : n ÷ j <> 0) e 2 <= i <= n^½ + 1.

Assim, a função completa é:

/** Indica se o argumento é um número natural primo.   @pre 1 <= n.   @post ePrimo = (2 <= n e (Q j : 2 <= j < n : n ÷ j <> 0)).*/ bool ePrimo(int const n) {     assert(0 <= n);

    if(n < 2)         return false;

    bool e_primo = true;     int i = 2;

    while(i * i <= n) {         e_primo = e_primo and n % i != 0;         ++i;     }

    return e_primo; }

1.d) Há muitas outras formas! Ver folhas teóricas! Há métodos recentes ainda mais eficientes e usados em criptografia...

2. Ver ex2.C.

O primeiro passo é escrever o esqueleto do programa incluindo a pré-condição e a condição objectivo. Para simplificar a escrita da condição objectivo, convencionou-se que se representavam os valores lidos to teclado através da notação cin_j, com j = 0, ..., n - 1. Por exemplo, cin₂ significa o terceiro inteiro lido.

#include <iostream>

using namespace std;

int main()
{     cout << "Quantos números vai introduzir? ";     int n;     cin >> n;

    if(n < 1) {         cout << "Tem de introduzir pelo menos um inteiro!" << endl;         return 1;     }

    cout << "Introduza " << n << " números." << endl;

    // PC: 1 <= n e o canal de entrada cin está em bom estado e contém n números inteiros.

    int maximo = ?;

    ...

    // CO: (E j : 0 <= j < n : cin_j = maximo) e (Q j : 0 <= j < n : cin_j <= maximo).

    cout << "O máximo é " << maximo << '.' << endl; }

Em seguida enfraquece-se a condição objectivo de modo a obter a condição invariante. Neste caso pode-se simplesmente substituir o limite superior do quantificador (constante n) por uma nova variável C++ i introduzida para o efeito e deixá-la variar numa gama apropriada:

CI: (E j : 0 <= j < i : cin_j = maximo) e (Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i <= n.

(Na realidade existe uma outra condição que se assume ser sempre verdadeira: o número de valores já lidos de cin é exactamente igual a i. Não se inclui essa condição na condição invariante para aliviar um pouco a notação.)

Esta condição invariante afirma simplesmente que maximo é o maior dos valores lidos até ao momento.

Como guarda, escolhe-se simplesmente i <> n, de modo que CI e ¬G implica CO.

O passo seguinte é escolher a inicialização do ciclo. Como não existe máximo de um conjunto vazio (porque o quantificador "existe um" é falso se o número de termos for zero), a forma mais simples de garantir a veracidade da condição invariante é fazendo:

int maximo; cin >> maximo; //depois desta instrução maximo = cin₀.
int i = 1;

Analisando os termos da condição invariante um a um, verifica-se que:

0 <= i <= n, é uma afirmação verdadeira, dada a pré-condição;
(Q j : 0 <= j < 1 : cin_j <= maximo) é o mesmo que cin₀ <= maximo, e portanto verdadeira, dado que maximo = cin₀; e
(E j : 0 <= j < i : cin_j = maximo) é o mesmo que cin₀ = maximo, e portanto verdadeira, dado que maximo = cin₀.

Em seguida há que escolher o progresso. Neste caso pode-se optar pela simples incrementação de i:

++i;

pois garante a terminação do ciclo.

Falta escolher uma acção que garanta a invariância da condição invariante apesar do progresso. O passo pode-se escrever:

// Aqui assume-se que CI e G, ou seja,
// (E j : 0 <= j < i : cin_j = maximo) e (Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i <= n e i <> n, ou ainda,
// (E j : 0 <= j < i : cin_j = maximo) e (Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i < n.
acção
++i;
// Aqui pretende-se que
// CI: (E j : 0 <= j < i : cin_j = maximo) e (Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i <= n.

Partindo dos objectivos, podemos obter a condição mais fraca a impor antes do progresso para que depois dele a condição invariante seja verdadeira. Para isso substitui-se i por i + 1, pois ++i é equivalente a i = i + 1:

// (E j : 0 <= j < i + 1 : cin_j = maximo) e (Q j : 0 <= j < i + 1 : cin_j <= maximo) e 0 <= i + 1 <= n, ou seja,// (E j : 0 <= j < i + 1 : cin_j = maximo) e (Q j : 0 <= j < i + 1 : cin_j <= maximo) e -1 <= i < n.++i;
// (E j : 0 <= j < i : cin_j = maximo) e (Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i <= n.

É fácil verificar que

((E j : 0 <= j < i : cin_j = maximo) ou cin_i = maximo) e
(Q j : 0 <= j < i : cin_j <= maximo) e cin_i <= maximo e 0 <= i < n
implica
(E j : 0 <= j < i + 1 : cin_j = maximo) e (Q j : 0 <= j < i + 1 : cin_j <= maximo) e -1 <= i < n.

Agora há que escolher a acção de modo a que

// (E j : 0 <= j < i : cin_j = maximo) e (Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i < n.
acção
// implica ((E j : 0 <= j < i : cin_j = maximo) ou cin_i = maximo) e
// (Q j : 0 <= j < i : cin_j <= maximo) e cin_i <= maximo e 0 <= i < n.

É claro que o valor de i não necessita de ser afectado pela acção. Mas o de maximo sim. Como o fazer? Haverá alguma circunstância em que a variável maximo não necessite de ser alterada, isto é, em que a acção possa ser nula? Comparando termo a termo as asserções antes e depois da acção, conclui-se que isso só acontece se cin_i <= maximo. Então a acção deverá consistir em duas instruções, uma que nos permita obter o valor de cin_i (e guardá-lo numa variável auxiliar) e numa instrução de selecção:

int v; cin >> v; //A partir de aqui v = cin_i. if(v <= maximo) ; else instrução₂

Resta saber que instrução deverá ser usada para o caso em que cin_i > maximo, ou seja, v > maximo. Essa instrução tem de levar a:

// (E j : 0 <= j < i : cin_j = maximo) e (Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i < n e cin_i > maximo.
instrução₂
// implica ((E j : 0 <= j < i : cin_j = maximo) ou cin_i = maximo) e
// (Q j : 0 <= j < i : cin_j <= maximo) e cin_i <= maximo e 0 <= i < n.

Antes da instrução, maximo contém o maior dos valores que estava no canal de entrada. No entanto, o valor acabado de ler (cin_i) contém um valor superior ao que está em maximo. Assim, maximo deverá tomar o valor de cin_i de modo a continuar a ter o maior dos valores lidos do canal de entrada até ao momento. A instrução a usar é portanto:

maximo = v;

Tem de se verificar se esta acção é correcta. Para isso calcula-se a pré-condição mais fraca que conduz à asserção final pretendida:

// ((E j : 0 <= j < i : cin_j = cin_i) ou cin_i = cin_i) e
// (Q j : 0 <= j < i : cin_j <= cin_i) e cin_i <= cin_i e 0 <= i < n, ou seja,
// ((E j : 0 <= j < i : cin_j = cin_i) ou V) e (Q j : 0 <= j < i : cin_j <= cin_i) e V e 0 <= i < n, ou seja,
// (Q j : 0 <= j < i : cin_j <= cin_i) e 0 <= i < n.
maximo = v; // e v = cin_i.
// implica ( (E j : 0 <= j < i : cin_j = maximo) ou cin_i = maximo) e
// (Q j : 0 <= j < i : cin_j <= maximo) e cin_i <= maximo e 0 <= i < n.

Como

(E j : 0 <= j < i : cin_j = maximo) e (Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i < n e cin_i > maximo
implica
(Q j : 0 <= j < i : cin_j <= maximo) e 0 <= i < n e cin_i > maximo
implica
(Q j : 0 <= j < i : cin_j < cin_i) e 0 <= i < n
implica
(Q j : 0 <= j < i : cin_j <= cin_i) e 0 <= i < n,

a invariância fica demonstrada.

Finalmente a demonstração de que o ciclo termina, i.e., que o ciclo está não só parcialmente correcto mas totalmente correcto, pode ser feita notando que i começa em 1 e é incrementado a cada passo, e portanto atingirá n ao fim de um número finito de passos (exactamente n - 1, recorde-se que a pré-condição garante que 1 <= n).

O programa completo fica então:

#include <iostream> using namespace std; int main()
{     cout << "Quantos números vai introduzir? ";     int n;     cin >> n;
    if(n < 1) {         cout << "Tem de introduzir pelo menos um inteiro!" << endl;         return 1;     }
    cout << "Introduza " << n << " números." << endl;
    int maximo;     cin >> maximo;
    int i = 1;     while(i != n) {         int v;         cin >> v;         if(v > maximo)             maximo = v;         ++i;     }     cout << "O maximo é " << maximo << '.' << endl; }

4.a) Ver ex4a.C.

O primeiro passo é escrever o esqueleto da função incluindo a PC e a CO.

/** Indica se existe um múltiplo de k entre m e n inclusive.
    @pre 0 < k e 0 <= m <= n.
    @post haMultiploEntre = (E j : m <= j <= n : j ÷ k = 0). */
bool haMultiploEntre(int const k, int const m, int const n)
{     assert(0 < k and 0 <= m and m <= n);
    bool ha = ?;
    ...

    // CO: ha = (E j : m <= j <= n : j ÷ k = 0).
    return ha;
}

Nota: Usa-se um nome incompleto (ha) para simplificar as expressões abaixo.

O passo seguinte passa por identificar a necessidade de um ciclo. Neste caso assume-se que um ciclo é necessário (mas ver próxima resposta).

Em seguida enfraquece-se a condição objectivo do ciclo de modo a obter a condição invariante. Neste caso pode-se simplesmente substituir o limite superior do quantificador (constante n) por uma nova variável C++ i introduzida para o efeito:

CI: ha = (E j : m <= j <= i : j ÷ k = 0) e m <= i <= n.

Como guarda escolhe-se simplesmente i <> n, de modo a que CI e ¬G implica CO.

O passo seguinte é escolher a inicialização do ciclo. A forma mais simples de tornar verdadeira a condição invariante é fazendo:

ha = false;
i = m - 1;

pois dessa forma o quantificador tem zero termos e portanto valor F.

Em seguida há que escolher o progresso. Neste caso pode-se optar pela simples incrementação de i:

++i;

Falta escolher uma acção que garanta a invariância da condição invariante apesar do progresso. O passo pode-se escrever:

// Aqui assume-se que CI e G, ou seja,
// ha = (E j : m <= j <= i : j ÷ k = 0) e m <= i <= n ei <> n ou ainda,
// ha = (E j : m <= j <= i : j ÷ k = 0) e m <= i < n.
acção
++i;
// Aqui pretende-se que CI seja verdadeira, ou seja,
// ha = (E j : m <= j <= i : j ÷ k = 0) e m <= i <= n.

Partindo dos objectivos, pode-se obter a condição mais fraca a impor antes do progresso para que depois dele a condição invariante seja verdadeira:

// ha = (E j : m <= j <= i + 1 : j ÷ k = 0) e m <= i + 1 <= n, ou seja,
// ha = (E j : m <= j <= i + 1 : j ÷ k = 0) e m - 1 <= i < n.
++i;
// ha = (Ej : m <= j <= i : j ÷ k = 0) e m <= i <= n.

Agora há que escolher a acção de modo a que

// ha = (E j : m <= j <= i : j ÷ k = 0) e m <= i < n
acção
// implica ha = (E j : m <= j <= i + 1 : j ÷ k = 0) e m - 1 <= i < n.

É claro que o valor de i não necessita de ser afectado pela acção. Mas o de ha precisa. Em particular a variável ha tem de passar a conter o valor que tinha antes da acção disjunto com (i + 1) ÷ k = 0. Ou seja, a acção será:

ha = ha or (i + 1) % k == 0;

Pode-se verificar que é uma boa escolha obtendo a condição mais fraca a impor antes da acção:

//(ha ou (i + 1) ÷ k = 0) = (E j : m <= j <= i + 1 : j ÷ k = 0) e m - 1 <= i < n.
ha = ha or (i + 1) % k == 0;
// implica ha = (E j : m <= j <= i + 1 : j ÷ k = 0) e m - 1 <= i < n.

Como

ha = (E j : m <= j <= i : j ÷ k = 0) e m <= i < n
implica
(ha ou (i + 1) ÷ k = 0) = (E j : m <= j <= i + 1 : j ÷ k = 0) e m - 1 <= i < n.

a invariância fica demonstrada.

Finalmente a demonstração de que o ciclo termina, i.e., que o ciclo está não só parcialmente correcto mas totalmente correcto, pode ser feita notando que i começa em m - 1 e é incrementado a cada passo, e portanto atingirá n ao fim de um número finito de passos (exactamente n - m + 1, recorde-se que a pré-condição garante que n >= m).

A função completa fica então:

/** Indica se existe um múltiplo de k entre m e n inclusive.
    @pre 0 < k e 0 <= m <= n.
    @post haMultiploEntre = (E j : m <= j <= n : j ÷ k = 0). */
bool haMultiploEntre(int const k, int const m, int const n)
{     assert(0 < k and 0 <= m and m <= n);
    bool ha = false;

    for(int i = m - 1; i != n; ++i)
        ha = ha or (i + 1) % k == 0;

    return ha;
}

Uma simples mudança de variável permite-nos atrasar o valor de i de uma unidade:

/** Indica se existe um múltiplo de k entre m e n inclusive.
    @pre 0 < k e 0 <= m <= n.
    @post haMultiploEntre = (E j : m <= j <= n : j ÷ k = 0). */
bool haMultiploEntre(int const k, int const m, int const n)
{     assert(0 < k and 0 <= m and m <= n);
    bool ha = false;

    for(int i = m; i != n + 1; ++i)
        ha = ha or i % k == 0;

    return ha;
}

É óbvio que, se alguma vez o valor de ha se tornar V, nunca mais o deixará de ser, pelo que o ciclo pode ser abreviado, reforçando a guarda (a demonstração formal de que o ciclo continua correcto deixa-se a cargo do aluno). Ou seja:

/** Indica se existe um múltiplo de k entre m e n inclusive.
    @pre 0 < k e 0 <= m <= n.
    @post haMultiploEntre = (E j : m <= j <= n : j ÷ k = 0). */
bool haMultiploEntre(int const k, int const m, int const n)
{     assert(0 < k and 0 <= m and m <= n);
    bool ha = false;

    for(int i = m; not ha and i != n + 1; ++i)
        ha = ha or i % k == 0;

    return ha;
}

Esta versão pode ser simplificada observando que no início do passo, com esta guarda reforçada, a variável ha toma sempre o valor F, pelo que a acção pode ser simplificada:

/** Indica se existe um múltiplo de k entre m e n inclusive.
    @pre 0 < k e 0 <= m <= n.
    @post haMultiploEntre = (E j : m <= j <= n : j ÷ k = 0). */
bool haMultiploEntre(int const k, int const m, int const n)
{     assert(0 < k and 0 <= m and m <= n);
    bool ha = false;

    for(int i = m; not ha and i != n + 1; ++i)
        ha = i % k == 0;

    return ha;
}

Finalmente, uma solução alternativa passa pelo terminar abrupto da função se se encontrar um múltiplo:

/** Indica se existe um múltiplo de k entre m e n inclusive.
    @pre 0 < k e 0 <= m <= n.
    @post haMultiploEntre = (E j : m <= j <= n : j ÷ k = 0). */
bool haMultiploEntre(int const k, int const m, int const n)
{     assert(0 < k and 0 <= m and m <= n);     for(int i = m; i != n + 1; ++i)
        if(i % k == 0)
            return true;

    return false;
}

Esta última versão é pouco recomendável, pois o ciclo fica com duas possíveis saídas.

4.b) Sim! A condição objectivo é equivalente a CO': m ÷ k = 0 ou m / k <> n / k (divisão inteira!). Ou seja, há um múltiplo de k entre m e n (inclusive), se e só se m for múltiplo de k ou o quociente de m por k for diferente do quociente de n por k. Ver ex4b.C.

Para demonstrar que CO' equivale a CO demonstra-se primeiro que CO' implica CO (suficiência) e depois que ¬CO' implica ¬CO (necessidade).

Suponha-se que m ÷ k = 0 ou m / k = g <> n / k = h. Se o primeiro termo for verdadeiro, é óbvio que existe um múltiplo: o próprio m. Partindo apenas do segundo termo, m / k = g <> n / k = h, conclui-se que g k <= m < (g + 1) k e h k <= n < (h + 1) k. Sabe-se ainda que g < h, o que é o mesmo que g + 1 <= h, que por sua vez implica que (g + 1) k <= h k. Assim, conclui-se que g k <= m < (g + 1) k <= h k <= n < (h + 1) k. Ou seja, há de certeza múltiplos de k entre m e n: pelo menos (g + 1) k e h k (que podem ser iguais).

Suponha-se agora que m ÷ k <> 0 e m / k = n / k = h. Do segundo termo é óbvio que h k <= m < (h + 1) k e que h k <= n < (h + 1) k. Por outro lado supôs-se que m ÷ k <> 0, ou seja, h k < m < (h + 1) k e h k <= n < (h + 1) k. Como se sabe que m <= n, conclui-se que h k < m <= n < (h + 1) k. É evidente então que não há múltiplos de k entre m e n nestas circunstâncias.

A função pode portanto ser escrita como:

/** Indica se existe um múltiplo de k entre m e n inclusive.
    @pre 0 < k e 0 <= m <= n.
    @post haMultiploEntre = (E j : m <= j <= n : j ÷ k = 0). */
bool haMultiploEntre(int const k, int const m, int const n)
{     assert(0 < k and 0 <= m and m <= n);     return m % k == 0 or m / k != n / k;
}

Desafio ao aluno: Consegue simplificar adicionalmente esta função?