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

Comece por experimentar e solucionar os exemplos 12, 13 e 14 discutidos nos slides.

Resolva agora os seguintes exercícios.

Exercício 1 (maxsort_init.c)

Recorde os predicados Sorted e Swap definidos na aula e os contratos das funções maxarray e swap:

/*@ predicate Sorted{L}(int *t,integer i,integer j) =
      \forall integer k; i<=k<j ==> \at(t[k],L) <= \at(t[k+1],L);
*/

/*@ predicate Swap{L1,L2}(int *a, integer i,integer j) = 
       \at(a[i],L1) == \at(a[j],L2)
       && \at(a[i],L2) == \at(a[j],L1)
       && \forall integer k;  k!=i && k!=j ==> \at(a[k] ,L1) == \at(a[k] ,L2);
*/

/*@ requires 0 < size && \valid(u+ (0..size-1));
    ensures 0 <= \result < size;
    ensures \forall integer a; 0 <= a < size ==> u[a] <= u[\result];
    assigns \nothing;
*/
int maxarray(int u[], int size);

/*@ requires \valid(t+i) && \valid(t+j);
    ensures Swap{Old,Here}(t,i,j);
    assigns t[i], t[j];
*/
void swap(int t[],int i,int j);

Considere a seguinte função que ordena um array por ordem crescente.

void maxSort (int *a, int size) { 
   int i, j;
   
   for (i=size -1; i>0; i--) { 
      j = maxarray(a,i+1); 
      swap(a,i,j);
   } 
}

1. Escreva um contrato que garanta a segurança desta função e prove a correção da função face esse contrato.

2. Melhore agora o contrato da função de forma a garantir que o array produzido está ordenado por ordem crescente. Escreva os invariantes de ciclo que lhe permitem provar o novo contrato.

3. Recorde agora a definição do predicado indutivo Permut, apresentado na aula,

   /*@ inductive Permut{L1,L2}(int *a, integer l, integer h) {
       case Permut_refl{L}:  
              \forall int *a, integer l, h; Permut{L,L}(a, l, h) ; 
       case Permut_sym{L1,L2}: \forall int *a, integer l, h;  
              Permut{L1,L2}(a, l, h) ==> Permut{L2,L1}(a, l, h) ; 
       case Permut_trans{L1,L2,L3}:  
              \forall int *a, integer l, h; Permut{L1,L2}(a, l, h) && Permut{L2,L3}(a, l, h) 
                                      ==> Permut{L1,L3}(a, l, h) ; 
       case Permut_swap{L1,L2}:  
              \forall int *a, integer l, h, i, j;  
                   l <= i <= h && l <= j <= h && Swap{L1,L2}(a, i, j) ==> Permut{L1,L2}(a, l, h) ;
     }
   */
   

   e complete o contrato da função maxSort de forma a garantir que a função implementa um algoritmo de ordenação. Em seguida, complete a prova.

Exercício 2 (count_init.c)

A função numOccur calcula o número de ocurrências de val no arrray ` a de tamannho n`.

int numOccur(const int* a, int n, int val) {
  int counted = 0;
  
  for (int i = 0; i < n; ++i) {
    if (a[i] == val) {
      counted++; }
  }
  return counted;
}

Uma definição axiomática de uma função lógica Count que determina o número de ocorrências de um inteiro num array, pode ser feita do seguinte modo.

/*@ 
axiomatic CountAxiomatic {

logic integer Count(int* a, integer n, int v) ;
   
axiom CountEmpty: \forall int *a, v, integer n; n <= 0 ==> Count(a, n, v) == 0;
   
axiom CountOneHit: \forall int *a, v, integer n;
             a[n] == v ==> Count(a, n + 1, v) == Count(a, n, v) + 1;

axiom CountOneMiss: \forall int *a, v, integer n; 
             a[n] != v ==> Count(a, n + 1, v) == Count(a, n, v);
}
*/

Note que na definição axiomática a função não tem corpo. Seu comportamento é definido apenas pelos axiomas que declaramos sobre ele.

1. Escreva um contrato ACSL para a função numOccur.

2. Escreva os invariantes de ciclo que lhe permitem provar a correção da função numOccur face ao contrato que definiu.

Exercício 3 (reverse_init.c)

A função reverse inverte o array a de tamanho n.

void reverse (int A[], int n) {
  int i, x;

  for (i=0; i<n/2; i++) {
     x = A[i];
     A[i] = A[n-1-i];
     A[n-1-i] = x;
  }  
}

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

2. Escreva os invariantes de ciclo que lhe permitem provar a correção da função reverse face ao contrato que definiu.