Especificação de Programas

$$\text{while}G\text{{}C\text{}}[[a]]\text{P}[[b]]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{array}{rl}E\to & N\\ & |V\\ & |\text{-}E\\ & |E\text{+}E\\ & |E\text{-}E\\ & |E\text{*}E\\ B\to & \text{true}\\ & |\text{false}\\ & |\text{not}B\\ & |B\text{or}B\\ & |B\text{and}B\\ & |E\text{==}E\\ & |E\text{!=}E\\ & |E\text{<}E\\ & |E\text{<=}E\\ C\to & V\text{=}E\\ & |\text{if}B\text{{}P\text{}}\text{else}\text{{}P\text{}}\\ & |\text{while}B\text{{}P\text{}}\\ P\to & \lambda \\ & |C\text{;}P\end{array}$$ 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 ,\perp ,\neg ,\vee ,\wedge$ e com as relações numéricas ${=}_2,/{=}_2,{<}_2,{\le }_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{x\text{=}n}$. O lado esquerdo, $x$, é uma variável e o lado direito, $n$, uma expressão numérica.
  • Condição $\boxed{\text{if}b\text{{}p\text{}}\text{else}\text{{}n\text{}}}$. 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{\text{while}b\text{{}c\text{}}}$. 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{c\text{;}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 $\text{P}$ um programa com instruções $c=\left(c_1;\dots ;c_K\right)$ e variáveis $x=\left(x_1,\dots ,x_N\right)$.

Estado: Um estado, ou configuração, de $\text{P}$ é um par $e=\left(a,v\right)$ em que:

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

Valoração: Um estado $e=\left(a,v\right)$ de um programa $\text{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\left(\alpha \right)$ é 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\left(\beta \right)$ é 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\left(\beta \right)$ for $\mathtt{v}$ 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 $\text{P}$ a partir do estado $e_0$ é uma sequência de estados $\left(e_0,e_1,\dots \right)$ em que $e_{i+1}$ resulta de $e_i$ em função da instrução activa de $\text{P}$.

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

• Estado seguinte: Seja $e=\left(a,v\right)$ um estado com instrução ativa (índice) $a$ e valores $v$. O estado seguinte, $e^{\prime }$, 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{x_k\text{=}y}$
    • $e^{\prime }=\left(a+1,u\right)$ em que $u_j=v_j$ em todas as posições exceto $u_k=v_e\left(y\right)$;
  • Condição $\boxed{\text{if}b\text{{}p\text{}}\text{else}\text{{}n\text{}}}$
    • Se $e\models b$ seja $f$ o estado que resulta da computação de $p$ (o ramo positivo) a partir do estado $g=\left(1,v\right)$ e $u$ os valores em $f$. Então $e^{\prime }=\left(a+1,u\right)$.
    • Caso contrário, se $e/\models b$, seja $f$ o estado que resulta da computação de $n$ (o ramo negativo) a partir do estado $g=\left(1,v\right)$ e $u$ os valores em $f$. Então $e^{\prime }=\left(a+1,u\right)$.
  • Repetição $\boxed{\text{while}b\text{{}c\text{}}}$
    • (continuação) Se $e/\models b$, então $e^{\prime }=\left(a+1,v\right)$.
    • 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=\left(1,v\right)$ e $u$ os valores em $f$:
      • (ciclo) Se $f\models b$ então $e^{\prime }=\left(a,u\right)$.
      • (continuação) Caso contrário, se $f/\models b$, então $e^{\prime }=\left(a+1,u\right)$.

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=\left(1,\left(0,0\right)\right)$ (assumindo $\text{x}=x=x_1$ e $\text{y}=y=x_2$) está ilustrada na seguinte tabela:

Exercícios:

1. Faça a computação para o estado inicial $e=\left(1,\left(2,0\right)\right)$.
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 $\text{T}$ que verifique se qualquer programa $\text{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 $\text{X}$ e estado inicial $e$ por um número, digamos $x$, e correr $\text{T}$ no estado inicial $e_x=\left(1,(x,y=0)\right)$.

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

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

Programas Totais e Parciais

Definição (Programa Total, Parcial)

Seja $P$ um programa e $e=\left(1,v\right)$ um estado.

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

Além disso,

• $P$ é total se termina qualquer que seja o estado inicial $e$ como acima: $\forall eP\left(e\right)\downarrow$. Nesse caso escreve-se $$P\downarrow .$$
• $P$ é parcial se não termina com alguns estados iniciais $e$ como acima: $\exists eP\left(e\right)\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\le 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

$$[[a]]\text{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, $[[a]]\text{P}[[b]]$)

Seja $\text{P}$ um programa, $a$ e $b$ fórmulas. Um triplo de Hoare é a expressão $$[[a]]\text{P}[[b]]$$ e significa que se o programa $\text{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 $\text{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 $\text{P}$ é representada da mesma forma em $a$ e $b$: $\text{x}$ é representada por $x$, $\text{cont}$ por $\text{cont}$, etc.
• As variáveis ligadas de $a$ e $b$ não ocorrem em $\text{P}$.

Notação. A representação usual dos triplos de Hoare é $\{a\}\text{P}\{b\}$. Aqui usa-se a forma $[[a]]\text{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\left\{x/y\right\}$ 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$: $$[[x>0]]\text{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\le 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 $$[[x\ge 0]]\text{Fac1}[[y=x!]]$$ especifica que, se $x\ge 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 $\text{x}$ e $y$ a $\text{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 $[[x>0]]\text{Fac2}[[y=x!]]$ não funciona porque $x$ é transformado pelo programa.

Este problema pode ser resolvido usando uma "variável lógica auxiliar": $$[[x_0>0\wedge x=x_0]]\text{Fac2}[[y=x_0!]]$$

• $x_0$ é uma variável lógica universalmente quantificada e que não ocorre em Fac2: Para qualquer $x_0$, $[[x_0>0\wedge x=x_0]]\text{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$.