Especificação de Programas

$$ \Huge \ploop{G}{C} \qquad \ho{a}{P}{b} \qquad e \models a $$

O processo de verificação formal de um programa começa por uma definição formal da sintaxe dos programas, continua com a respetivas semântica, isto é, as computação e a especificação dos “comportamentos”: condições sobre as entradas e os respetivos resultados.

As condições das entradas e resultados são fórmulas de uma lógica de primeira ordem adequada e a verificação é uma prova com regras adequadas à sintaxe do programa.

Programas Sequenciais Transformacionais

O primeiro passo consiste em definir uma linguagem de programação adequada que, essencialmente, é um sub-conjunto das linguagens imperativas comuns (C, Python, Rust).

A formalização de uma linguagem (de programação ou outro uso) é assunto de outra disciplina, não tratado aqui. Resumindo, uma linguagem de programação pode ser definida usando uma gramática independente do contexto.

Definição (Expressão, Instrução, Programa)

Dada a gramática

$$ \begin{aligned} E \to & \quad N \cr & | \quad V \cr & | \quad \pneg{E} \cr & | \quad \padd{E}{E} \cr & | \quad \psub{E}{E} \cr & | \quad \pmul{E}{E} \cr B \to & \quad \ptrue \cr & | \quad \pfalse \cr & | \quad \pnot{B} \cr & | \quad \por{B}{B} \cr & | \quad \pand{B}{B} \cr & | \quad \peq{E}{E} \cr & | \quad \pne{E}{E} \cr & | \quad \plt{E}{E} \cr & | \quad \ple{E}{E} \cr C \to & \quad \pcp{V}{E} \cr & | \quad \pcond{B}{P}{P} \cr & | \quad \ploop{B}{P} \cr P \to & \quad \lambda \cr & | \quad \pseq{C}{P} \cr \end{aligned} $$

onde $N$ representa os números inteiros e $V$ as variáveis.

Então:

• Expressão numérica: Uma expressão numérica resulta da variável $E$. As expressões numéricas usam números, variáveis e as funções aritméticas $-_1, +_2, -_2, \times_2$; São termos na LPO.
• Expressão booleana: Uma expressão booleana resulta da variável $B$. As expressões booleanas podem ser construídas com os conectivos lógicos $\top, \bot, \neg, \lor, \land$ e com as relações numéricas $=_2, \not=_2, <_2, \leq_2$; São fórmulas sem quantificadores na LPO.
• Instrução: Uma instrução resulta da variável $C$. Há três tipos de instruções:
  • Cópia $\boxed{\pcp{x}{n}}$. O lado esquerdo, $x$, é uma variável e o lado direito, $n$, uma expressão numérica.
  • Condição $\boxed{\pcond{b}{p}{n}}$. A guarda $b$ é uma expressão booleana e $p, n$ são (sub-)programas, o ramo positivo e o ramo negativo respetivamente.
  • Repetição ou Ciclo $\boxed{\ploop{b}{c}}$. A guarda $b$ é uma expressão booleana e o corpo $c$ um (sub-)programa.
• Programa: Um programa resulta da variável $P$. - O caso $\boxed{\lambda}$ é o programa vazio, sem instruções. - O caso $\boxed{\pseq{c}{p}}$ é uma sequência em que a a seguir à instrução $c$ estão as instruções de $p$. Nesta sequência não estão incluídas as instruções dos corpos das repetições nem dos ramos das condições.

Isto é, um programa é uma sequência de instruções, possivelmente vazia. Há três tipos de instruções: cópia, condição e repetição. As expressões numéricas e booleanas são parte dessas instruções.

Esta definição apenas cobre a sintaxe de um programa. Para definir a computação de um programa é necessário um estado que descreva a instrução atual e os valores das variáveis e como os diferentes tipos de instruções comandam a evolução do estado.

Definição (Estado, Valoração, Computação)

Seja $\kw{P}$ um programa com instruções $c = \del{c_1; \ldots; c_K}$ e variáveis $x = \del{x_1, \ldots, x_N}$.

Estado: Um estado, ou configuração, de $\kw{P}$ é um par $e = \del{a, v}$ em que:

• $a$ é o índice da instrução ativa, um número natural positivo.
• $v = \del{v_1, \ldots, v_N}$ é um vetor de números tal que o valor da variável $x_i$ é $v_i$.

Valoração: Um estado $e = \del{a, v}$ de um programa $\kw{P}$ define o valor das expressões desse programa da seguinte forma:

• Valor numérico: Seja $\alpha$ uma expressão numérica. Então $v_e\at{\alpha}$ é o valor de $\alpha$ em $e$ e resulta de:
  1. Substituir as variáveis de $\alpha$ pelos respetivos valores em $e$.
  2. Usar as regras usuais da aritmética para as operações.
• Valor booleano: Seja $\beta$ uma expressão booleana. Então $v_e\at{\beta}$ é o valor de $\beta$ em $e$ e resulta de:
  1. Calcular os valores numéricos em $\beta$.
  2. Usar as regras usuais das desigualdades e dos conectivos booleanos em $\beta$.
• Se $v_e\at{\beta}$ for $\ndT$ diz-se que $e$ satisfaz $\beta$ e escreve-se $v_e \models \beta$ ou simplesmente $e \models \beta$.

Computação: Uma computação do programa $\kw{P}$ a partir do estado $e_0$ é uma sequência de estados $\del{e_0, e_1, \ldots}$ em que $e_{i+1}$ resulta de $e_i$ em função da instrução activa de $\kw{P}$.

• Estado inicial: Em geral $e_0$ é dado. Caso contrário, assume-se que $e_0 = \del{1, \del{0, 0, \ldots, 0}}$, a instrução ativa é a primeira instrução de $\kw{P}$ e todas as variáveis têm valor $0$.

• Estado seguinte: Seja $e = \del{a, v}$ um estado com instrução ativa (índice) $a$ e valores $v$. O estado seguinte, $e’$, depende do tipo da instrução ativa:
  • Se não existe instrução ativa ($a > K$) o programa termina e $e$ é o estado final.
  • Cópia $\boxed{\pcp{x_k}{y}}$
    • $e’ = \del{a+ 1, u}$ em que $u_j = v_j$ em todas as posições exceto $u_k = v_e\at{y}$;
  • Condição $\boxed{\pcond{b}{p}{n}}$
    • Se $e \models b$ seja $f$ o estado que resulta da computação de $p$ (o ramo positivo) a partir do estado $g = \del{1, v}$ e $u$ os valores em $f$. Então $e’ = \del{a + 1, u}$.
    • Caso contrário, se $e \not\models b$, seja $f$ o estado que resulta da computação de $n$ (o ramo negativo) a partir do estado $g = \del{1, v}$ e $u$ os valores em $f$. Então $e’ = \del{a + 1, u}$.
  • Repetição $\boxed{\ploop{b}{c}}$
    • (continuação) Se $e \not\models b$, então $e’ = \del{a + 1, v}$.
    • Caso contrário, se $e \models b$ então seja $f$ o estado que resulta da computação de $c$ (o corpo) a partir do estado $g = \del{1, v}$ e $u$ os valores em $f$:
      • (ciclo) Se $f \models b$ então $e’ = \del{a, u}$.
      • (continuação) Caso contrário, se $f \not\models b$, então $e’ = \del{a + 1, u}$.

As definições acima formalizam objetivamente a computação que um programa executa dada uma entrada (o estado inicial) para produzir o respetivo resultado (o estado final).

Exemplo. Computação Copy.

Considere-se o programa Copy:

#![allow(unused)]
fn main() {
y = 1;
if x > y {
    while y < x {
        y = y + 1;
    }
} else {
    while x < y {
        x = x + 1;
    }
}
}

Exercícios:

1. Quantas instruções tem este programa? De que tipos?
2. Quantos sub-programas?

A computação deste programa no estado inicial $e = \del{1, \del{0, 0}}$ (assumindo $\kw{x} = x = x_1$ e $\kw{y} = y = x_2$) está ilustrada na seguinte tabela:

Exercícios:

1. Faça a computação para o estado inicial $e = \del{1, \del{2, 0}}$.
2. Será que definir o valor de $y$ no estado inicial tem algum efeito no estado final?
3. Será que este programa garante que o estado final $f \models x = y$ seja qual for o estado inicial?
4. Em que casos o valor de $x$ não é afetado pelo programa? E o valor de $y$?

Problema da Paragem

Pode acontecer que uma computação não termine. Por exemplo o programa

#![allow(unused)]
fn main() {
while true {}
}

não termina em qualquer estado inicial. Neste caso a computação é uma sequência infinita de estados e o estado final não está definido.

O Problema da Paragem, apresentado informalmente na secção Gödel e Turing da Consequência Semântica Proposicional, consiste em determinar se existe algum programa $\kw{T}$ que verifique se qualquer programa $\kw{X}$ termina ou não.

Agora, com uma definição formal de “programa”, este problema pode ser apresentado com mais rigor.

A ideia é representar cada programa $\kw{X}$ e estado inicial $e$ por um número, digamos $x$, e correr $\kw{T}$ no estado inicial $e_x = \del{1, (x, y = 0)}$.

Essa computação de $\kw{T}$ deve terminar e, no estado final, fica $y = 1$ se e só se o programa $\kw{X}$ com estado inicial $e$ termina.

O que Turing mostrou é que não existem programas como $\kw{T}$: nenhum programa resolve o problema da paragem.

Programas Totais e Parciais

Definição (Programa Total, Parcial)

Seja $P$ um programa e $e = \del{1, v}$ um estado.

• Se $P$ termina (ou converge) no estado $e$ como acima escreve-se $$P\at{e}\downarrow.$$
• Caso contrário, $P$ diverge no estado $e$ e escreve-se $$P\at{e}\uparrow.$$

Além disso,

• $P$ é total se termina qualquer que seja o estado inicial $e$ como acima: $\forall e~P\at{e}\downarrow$. Nesse caso escreve-se $$P\downarrow.$$
• $P$ é parcial se não termina com alguns estados iniciais $e$ como acima: $\exists e~P\at{e}\uparrow$. Nesse caso escreve-se $$P\uparrow.$$

Por exemplo o programa

#![allow(unused)]
fn main() {
while x != y {
    x = x + 1
}
}

termina quando $e \models x \leq y$ mas não termina se $e \models x > y$. Portanto é um programa parcial.

Com a definição de programa total e parcial, o problema da paragem pode ser enunciado da seguinte forma:

Problema da Paragem. Existe um programa que classifica corretamente cada programa como total ou parcial?

Nesta formulação estamos a assumir que a entrada dos programas é dada na forma de um número que “codifica” juntamente o programa e o estado inicial.

O problema que se está a tratar aqui é mais “simples”: É possível provar que um programa tem um determinado comportamento? Isto é, se a entrada verificar determinadas condições iniciais existe uma prova que o resultado do programa satisfaz as condições finais?

Exemplo. Satisfação de estados iniciais e finais.

Considere-se o seguinte programa e condições sobre os valores das variáveis antes do programa correr e quando termina.

#![allow(unused)]
fn main() {
y = 0;
z = 0;
while z != x {
    z = z + 1;
    y = y + z;
}
}

Seja $e$ o estado inicial e $f$ o estado final.

A ideia é caraterizar o “comportamento” de um programa pelos estados iniciais e finais.

Triplos de Hoare

$$\Large \ho{a}{P}{b}$$

Pretende-se relacionar uma condição inicial dada e uma condição final obtida por efeito da computação do programa.

Definição (Triplo de Hoare, $\ho{a}{P}{b}$)

Seja $\kw{P}$ um programa, $a$ e $b$ fórmulas. Um triplo de Hoare é a expressão

$$ \ho{a}{P}{b} $$

e significa que se o programa $\kw{P}$ corre num estado inicial $e$ que satisfaz $a$, $e \models a$, então, quando termina o estado final, $f$, satisfaz $b$, $f \models b$.

• A fórmula $a$ é a pré-condição do triplo.
• A fórmula $b$ é a pós-condição do triplo.
• O programa $\kw{P}$ é o programa do triplo.

As fórmulas $a$ e $b$ são fórmulas LPO no universo dos números inteiros, com as interpretações usuais dos símbolos $-_1, +_2, -_2, \times_2, <_2, =_2$.

Além disso:

• Cada variável de $\kw{P}$ é representada da mesma forma em $a$ e $b$: $\kw{x}$ é representada por $x$, $\kw{cont}$ por $\text{cont}$, etc.
• As variáveis ligadas de $a$ e $b$ não ocorrem em $\kw{P}$.

Notação. A representação usual dos triplos de Hoare é $\set{a} \kw{P} \set{b}$. Aqui usa-se a forma $\ho{a}{P}{b}$ para evitar confusão com a sintaxe dos programas, que usa {} para delimitar sub-programas, e com a substituição em fórmulas FOL, que usa $a\subst{x}{y}$ para substituir as ocorrências da variável $x$ pelo termo $y$ na fórmula $a$.

Especificação por Triplos de Hoare

Supondo que se pretende que um programa tenha o seguinte comportamento: quando $x$ é um número positivo, o programa define $y$ como um número cujo quadrado é menor do que $x$:

$$ \ho{x > 0}{P}{y^2 < x} $$

Isto é, se o programa correr num estado $e$ tal que $e \models x > 0$ quando termina, no estado que resulta, $f$, tem-se $f \models y^2 < x$.

Um programa que produza “lixo” quando $x \leq 0$ está de acordo com a especificação, desde que funcione como indicado quando $x > 0$.

Variáveis lógicas e do programa

Há uma associação entre as variáveis lógicas das condições e as variáveis que ocorrem nos programas. Esta associação é necessária mas requer algum cuidado.

Seja Fac1 o seguinte programa

y = 1;
z = 0;
while z != x {
    z = z + 1;
    y = y * z;
}

O triplo

$$ \ho{x \geq 0}{\kw{Fac1}}{y = x!} $$

especifica que, se $x \geq 0$ então Fac1 deve calcular o fatorial de $x$ e guardar o resultado em $y$. Neste caso a variável lógica $x$ está associada a $\kw{x}$ e $y$ a $\kw{y}$.

Mais adiante vai-se provar que este programa efetivamente calcula o fatorial de $x$.

Agora, seja Fac2 o programa

y = 1;
while x != 0 {
    y = y * x;
    x = x - 1;
}

Para Fac2 o triplo $\ho{x > 0}{\kw{Fac2}}{y = x!}$ não funciona porque $x$ é transformado pelo programa.

Este problema pode ser resolvido usando uma “variável lógica auxiliar”:

$$ \ho{x_0 > 0 \land x = x_0}{\kw{Fac2}}{y = x_0!} $$

• $x_0$ é uma variável lógica universalmente quantificada e que não ocorre em Fac2: Para qualquer $x_0$, $\ho{x_0 > 0 \land x = x_0}{\kw{Fac2}}{y = x_0!}$.
• Como $x_0$ não ocorre em Fac2 este triplo especifica o comportamento que se pretende: no fim $y$ é o fatorial de $x_0$.