Considere o seguinte código para o cálculo de $x$ elevado a $y$.

              
                #include <stdio.h>

                int potencia(int x, int y) {
                    int resultado = 1;
                    for (int i = 0; i < y; i++) {
                      resultado *= x; 
                    }
                    return resultado;
                 }
               
                int main(void) {
                  printf("2 elevado a 8 : %d\n", potencia(2,8));
                  return 0;
                }
              
            

Como você prova que este código faz o cálculo deste produto?

Antes da formalização da lógica, antes de Leibnitz, Boole, Hilbert, Gödel, Church e Turing, uma prova era só, e somente só, um argumento convincente.

Convincentes são os argumentos que não deixam dúvidas no interlocutor. De fato, ainda hoje, uma prova é apenas um argumento convincente. O que mudou é que este convencimento deve ser atingido por meio da lógica.

Poderíamos definir uma prova como: uma sequência de fórmulas, na qual, cada fórmula ou é um axioma, ou é o resultado da inferência da fórmula anterior.

Geralmente, não precisamos de toda esta formalidade matemática para provar que um programa funciona. Contudo, esta formalidade garante que o programa funciona.

                
                 int potencia(int x, int y) {
                      int resultado = 1;
                      for (int i = 0; i < y; i++) {
                        resultado *= x;
                      }
                      return resultado;
                   }
                
            

A parte mais importante do código é a função $potencia$ e nesta função, a parte principal é o laço. Desta forma, precisamos provar que este laço faz o que desejamos. Começamos com definindo um loop invariant.

Loop Invariant: uma propriedade dos laços que será verdadeira, antes e depois de cada iteração. No caso, podemos começar com: $(y \ge i ) \wedge (resultado = x^i) = True$ e verificar se isto é verdade, ou não, antes das iterações, a cada interação e depois de todas as iterações Hoare Logic.

Funções Puras: produzem o mesmo resultado para a mesma entrada e não possuem nenhum efeito colateral.

Recursão: não usamos nenhum laço de repetição.

Funções de primeira-classe: podem ser passadas como parâmetro, devolvidas e armazenadas em estruturas de dado.

Variáveis imutáveis: você pode criar uma variável nova mas não pode mudar o valor de uma variável já criada.