Verifcação dedutiva de programas C com plugin WP do Frama-C - sessão laboratorial 1

Comece por experimentar e solucionar os 11 primeiros exemplos discutidos nos slides.

Resolva agora os seguintes exercícios.

Exercício 1

Considere o seguinte código (disponivel no ficheiro change_init.c)

void change(int *a, int *b) { 
  int tmp = *a;
  *a = *b;
  *b = tmp;
}

1. Escreva em ACSL um contrato para esta função.

2. Prove a segurança da função e sua correção face ao contrato que definiu. Use para isso os plugins WP e RTE do Frama-C.

3. Escreva uma função main que chame esta função e verifique-a.

Exercício 2

A função negs testa se um array tem valores negativos, devolvendo 0 caso tenha.

int negs(int A[], int N);

1. Defina um contrato ACSL que descreva de forma precisa o comportamento desta função.

2. Escreva a definição da função e comprove sua segurança e correção funcional face ao contrato que definiu.

3. Escreva a seguinte função main anotada e verifique-a. Analize os resultados obtidos e acrescente as anotações necessárias para completar a prova com sucesso.

void main(void){
  int a[10];
  int b[5] = {3,4,8,3,7};
  int c[5] = {2,4,-28,3,-17};
  int i;

  i = negs(b,5);
  //@ assert i!=0;
  //@ assert i==1;     

  i = negs(c,5);
  //@ assert i==0;


  for(i=0; i<10; i++)
    a[i] = i*3;

  i = negs(a,10);
  //@ assert i!=0;
}

Exercício 3

A função minarray devolve o índice em que está o menor valor do array.

int minarray(int A[], int N);

1. Defina um contrato ACSL que descreva de forma precisa o comportamento desta função.

2. Escreva a definição da função e comprove sua segurança e correção funcional face ao contrato que definiu.

3. Escreva uma função main que invoque esta função e verifique-a.

Exercício 4

A função equal_seg testa se o segmento [a..b] de dois arrays são iguais.

int equal_seg(int A[], int B[], int a, int b, int N);

1. Defina um contrato ACSL que descreva de forma precisa o comportamento desta função.

2. Escreva a definição da função e comprove sua segurança e correção funcional face ao contrato que definiu.

3. Escreva uma função main que invoque esta função e verifique-a.

Exercício 5

A função where retorna uma posição do array onde o valor guardado é x. Caso o array não contenhas nenhum valor x retorna -1.

int where(int A[], int N, int x);

1. Comece por definir em ACSL o predicado belongs(x,A,n) que testa se o inteiro x pretence ao array A de tamanho n.

2. Usando o mecanismo de behaviors do ACSL defina um contrato que descreva de forma precisa o comportamento da função where.

3. Implemente a função e comprove sua segurança e correção funcional face ao contrato que definiu.

4. Escreva uma função main que invoque esta função e verifique-a.