Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] exit_behavior pour la prochaine réunion

  • Subject: [Frama-c-discuss] exit_behavior pour la prochaine réunion
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Mon, 14 Sep 2009 16:17:43 +0200
Claude, (mais les autres peuvent ?galement jouer le jeu...)

Lors de la prochaine r?union, il faudrait que nous avancions ?galement 
sur la clause "exit_behavior".
Afin de gagner du temps et que personne ne soit pris au d?pourvu, voici 
quelques ?l?ments.

Tout d'abord, je pense qu'en ACSL, la fonction exit se sp?cifie ainsi :

/*@ terminates \true ; // Elle ne boucle jamais ind?finiment,
  @ requires \true ;   // et ne requiert rien de particulier.
  @ behavior no_return :
  @   assumes case1:\true ;            // Dans tous les cas,
  @   requires pre1:\true ;            // sans ne rien requ?rir d'autre,
  @   ensures post1:\false ;           // elle n'effectue aucun "return",
  @ exit_behavior may_exit:            // et par cons?quent,
  @   assumes case2:\true ;            // dans chacun de ces cas,
  @   requires pre2:\true ;            // sans ne rien requ?rir d'autre,
  @   assigns modif2:\nothing ;        // elle ne modifie rien
  @   ensures post2:\result == status ;// et sort en "exit" du "main" 
avec la valeur "status".
  @*/
int exit(int status);

J'ai comment? chacunes des clauses afin de mettre en ?vidence ce 
qu'elles v?rifient.
Ainsi on voit mieux les impl?mentations qui pourraient ne pas satisfaire 
ce contrat. 

Maintenant, prenons la fonction identity.
Cela donne :
/*@ terminates \true ; // Elle ne boucle jamais ind?finiment,
  @ requires \true ;   // et ne requiert rien de particulier.
  @ behavior may_return :
  @   assumes case1:\true ;           // Dans tous les cas,
  @   requires pre1:\true ;           // sans ne rien requ?rir d'autre,
  @   assigns modif1:\nothing ;       // elle ne modifie rien,
  @   ensures post1:\result == val ;  // renvoie l'argument pass?
  @ exit_behavior never_exit:         // et,
  @   assumes case2:\true ;           // dans chacun de ces cas,
  @   requires pre2:\true ;           // sans ne rien requ?rir d'autre,
  @   ensures post2:\false ;          // elle ne sort jamais en "exit" 
du "main".
  @*/
int identity (int val);

Cela signifirait qu'en absence de clause "exit_behavior",
il existerait une clause par d?faut :
/*@ exit_behavior never_exit:
  @   assumes \true ;
  @   requires \true ;
  @   ensures \false ;
  @*/

Es-tu d'accord avec tout cela ?
Que penses-tu des preuves li?es aux diff?rentes clauses "ensures \false ;" ?

Patrick.

-- 
Patrick Baudin,
CEA, LIST, SOL, F-91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072