déclaration avec retour dans JML

Question

i besoin de mettre en place une postcondition qui assure à retourner null si size_ est 0. Basé sur

if(size_ == 0) 
    return null; 

comment puis-je faire en JML? des idées? A la suite ne fonctionne pas:

//@ ensures size_ == null ==> \return true; 

merci à l'avance

Answer 1

Essayez

//@ ensures size_ == null ==> \result == true; 

Exemple:

//@ ensures size_ == null ==> \result == true; 
public boolean sizeUndefined() { 
    if (size_ == null) 
     return true; 

    return size_.length() > 0; 
} 

Vous pouvez aussi tout simplement l'écrire comme ceci:

//@ ensures size_ == null ==> \result; 

Voici the documentation for \result:

3.2.14 \result
Dans un postcondition normal ou une cible de modification d'une méthode non-vide, le résultat identificateur spécial \ est une expression de spécification dont le type est le retour type de la méthode. Il indique la valeur renvoyée par la méthode. \ result n'est autorisé que dans un pragma Ensure, also_ensures, modify, ou aussi_modifies qui modifie la déclaration d'une méthode non-void.

Answer 2

tout d'abord: quel type est size_, Object ou primitive(int)?

Deuxièmement, quel est le type de retour de la méthode? Object ou primitive(boolean)?

Vous ne pouvez pas comparer un type primitif à null ou renvoyer null où un type primitif est censé être renvoyé. Si nous supposons size_ est int et le retour est boolean alors la post-condition serait

//@ ensures size_ == 0 ==> \result;