Verificação Formal: Aula 1

Algoritmos vs Programas

Um algoritmo que calcula o valor absoluto de um inteiro n, colocando o resultado em r:

var r : integer = n;

if r < 0 then r := -r

Um programa em C que usa o algoritmo acima para imprimir o valor absoluto de um número introduzido pelo utilizador:

#include <stdio.h>
int main() {
    int n,r;
    scanf("%d",&n);
    r = n;
    if (r < 0) r = -r;
    printf("%d\n",r);
    return 0;
}

Um algoritmo que multiplica um inteiro não negativo a por b, colocando o resultado em r:

var 
  r : integer = 0;
  n : integer = 0;

while n < a do
begin
  n := n + 1;
  r := r + b
end

Um programa em C que usa o algoritmo acima para imprimir o produto de dois números introduzidos pelo utilizador:

#include <stdio.h>
int prod(int a, int b) {
  int r = 0;
  for (int n = 0; n < a; n++) r += b;
  return r;
}
int main() {
    int a,b;
    scanf("%d",&a);
    scanf("%d",&b);
    printf("%d\n",prod(a,b));
    return 0;
}

Um algoritmo concorrente com 2 processos que incrementam uma variável partilhada x:

var x : integer = 0

procedure increment;
begin
  x := x + 1
end;

increment || increment

O um programa em C que implementa este algoritmo:

#include <stdio.h>
#include <unistd.h>
#include <sys/wait.h>
#include <sys/mman.h>

int main() {
    int *x = (int *) mmap(NULL, sizeof(int), PROT_READ | PROT_WRITE, MAP_SHARED | MAP_ANONYMOUS, -1, 0);
    *x = 0;
    if (fork() == 0) {
        (*x)++;
        return 0;
    }
    if (fork() == 0) {
        (*x)++;
        return 0;
    }
    while (wait(NULL) > 0);
    printf("%d\n",*x);
    return 0;
}

Discussão:

• Que diferenças vê entre os algoritmos e os programas?
• O algoritmos estão corretos?
• Os programas em C estão corretos?

Para mais discussão sobre algoritmos vs programas veja os minutos iniciais deste vídeo.

Lógica de Hoare

Tipicamente algoritmos sequenciais são especificados e verificados de forma dedutiva com lógica de Hoare.

Por exemplo, o algoritmo para calcular o valor absoluto pode ser especificado com as seguintes pré- e pós-condições.

{ true }
var r : integer = n;

if r < 0 then r := -r
{ r = abs(n) }

Para o caso da multiplicação temos:

{ a >= 0 }
var 
  r : integer = 0;
  n : integer = 0;

while n < a do
begin
  n := n + 1;
  r := r + b
end
{ r = a * b }

Para verificar a correção parcial de algoritmos com ciclos precisamos de invariantes de ciclo. Para verificação a sua terminação precisamos de variantes de ciclo. No caso da multiplicação um possível invariante seria r = n * b /\ n <= a e um possível variante seria a - n.

Verificação dedutiva de algoritmos sequenciais com Why3

Os exemplos acima verificados com o Why3:

• Valor absoluto
• Multiplicação por somas sucessivas

Exercício: verifique os seguintes algoritmos com o Why3:

• Outra versão da multiplicação por somas sucessivas
• Uma versão da multiplicação mais eficiente
• Fibonacci eficiente

Verificação dedutiva de algoritmos reativos

Como verificar algoritmos reativos, que reagem continuamente a estímulos do ambiente ou utilizador?

Considere o seguinte puzzle da cadeira pesada: num mapa quadriculado temos uma cadeira pesada que ocupa uma quadrícula; o utilizador pode em cada momento escolher rodar a cadeira 90º para a esquerda ou para a direita sobre qualquer uma das 4 pernas. Queremos verificar que não é possível colocar a cadeira na quadrícula imediatamente ao lado direito com a mesma orientação que estava inicialmente.

Este puzzle pode ser descrito pelo seguinte algoritmo, onde usamos não determinismo para abstrair o comportamento do utilizador.

var 
  x : integer = 0;
  y : integer = 0;
  o : integer = 0;

while true do
begin
  if true then 
    o := mod (o+1) 4 
  or else 
    o := mod (o-1) 4;
  case random(0..3) of
    0: y := y - 1;
    1: x := x + 1;
    2: x := x - 1;
    3: y := y + 1;
  end
end

Neste tipo de algoritmos não faz sentido falar em pós-condições nem em terminação. No entanto a propriedade que queremos verificar é de facto um invariante do ciclo, nomeadamente not (x = 1 and y = 0 and o = 0), e podemos usar lógica de Hoare para a verificar. O problema é que este invariante não é indutivo e será necessário descobrir um invariante mais forte (i.e. que o implique) que seja indutivo.

Exercício: tente descobrir esse invariante mais forte e verificar este algoritmo usando o Why3.

Exercício: haverá alguma versão mais abstrata do algoritmo deste puzzle onde a propriedade desejada seja trivial de verificar?

Verificação dedutiva de algoritmos concorrentes

O algoritmo concorrente apresentado acima pode ser especificado da seguinte forma.

{ true }
var
  x : integer = 0;

procedure increment;
begin
  x := x + 1
end;

increment || increment
{ x = 2 }

Como verificar este algoritmo com lógica de Hoare? De facto podemos modelar este algoritmo concorrente por um algoritmo sequencial que em cada momento escolhe de forma não determinística qual o processo a executar. Para tal temos que saber em que ponto de execução se encontra cada um dos processos.

{ true }
var 
  x : integer = 0;
  pc0 : 0..1 = 0;
  pc1 : 0..1 = 0;

while not (pc0 = 1 and pc1 = 1) do
begin
  if pc0 = 0 and pc1 = 0 then
  begin
    if true then
    begin
      x := x + 1;
      pc0 = 1
    end 
    or else 
    begin
      x := x + 1;
      pc1 = 1
    end
  end
  else if pc1 = 1 then
  begin
    x := x + 1;
    pc0 = 1
  end
  else
  begin
    x := x + 1;
    pc1 = 1
  end
end;
{ x = 2 }

Exercício: tente descobrir o invariante e o variante que permitem provar a correção deste algoritmo usando o Why3.

Exercício: tente modelar com um algoritmo sequencial não-determinístico a seguinte variante do algoritmo acima, onde cada processo começa por fazer uma cópia local da variável partilhada x.

{ true }
var 
  x : integer = 0;

procedure increment;
var
  y : integer = 0;
begin
  y := x;
  x := y + 1
end;

increment || increment
{ x = 2 }

Exercício: consegue verificar a pós-condição usando o Why3? será que a pós-condição não é verdade? nesse caso, especifique a pós-condição mais forte que este algoritmo garante e verifique-a com o Why3.

Verificação de algoritmos reativos e concorrentes

Considere o seguinte algoritmo de exclusão mútua de Peterson.

var 
  turn : 0..1;
  want0 : boolean = false;
  want1 : boolean = false;

procedure process0;
begin
  while true do                           
  begin
    (* idle *) 
    want0 := true; 
    turn := 1;  
    repeat until (not want1 or turn = 0);
    (* critical *) 
    want0 := false 
end

procedure process1;
begin
  while true do                           
  begin
    (* idle *) 
    want1 := true; 
    turn := 0;  
    repeat until (not want0 or turn = 1);
    (* critical *) 
    want1 := false 
end

process0 || process1

Discussão: como especificar e verificar as propriedades fundamentais deste algoritmo?

• Os dois processos nunca estão na região critica ao mesmo tempo.
• Sempre que um processo pretende aceder à região crítica irá conseguir.
• Ausência de deadlock.