Pourquoi ai-je eu une violation de précondition de valid_index dans Eiffel?

Question

Je viens de tester simplement une fonction push_at de la classe container (faite par array, fondamentalement). Je ne sais pas quelle partie de mon code déclenche cette violation.

push_at (i: INTEGER; s: STRING) 

    require 
     valid_index: i >= 1 
    do 
     container [i] := s 

    end 

Dans mon testeur

local 
     con: CONTAINER 

do 
      create {CONTAINER}con.make 
      con.push_at (1,"A") 
      con.push_at (2,"B") 

Result := con.get(1) ~ "A" and con.get(2) ~ "B" 
check Result end 
end 

Merci pour l'aide!

Answer 1

C'est le conteneur [i]. Lorsque vous créez con, il sera vide (probablement - vous ne nous avez pas montré votre code). Vous pré-condition doit refléter la condition préalable sur con []. Ce qui à son tour doit refléter la condition préalable sur {ARRAY} .put, que vous devez utiliser pour l'implémenter. Votre précondition actuelle ne le fait pas (c'est plutôt arbitraire).

Answer 2

La structure sous-jacente utilisée comme stockage pour les éléments n'alloue pas automatiquement la mémoire pour les nouveaux éléments. Certaines structures le font lorsque la commande d'assignation container [i] := s est exécutée. Mais ce n'est pas le cas dans le code que vous mentionnez. Par conséquent, l'index i utilisé dans cette commande n'est pas valide, d'où la violation de précondition. Si vous regardez la trace d'exception ou la pile d'appels, vous verrez que la violation de précondition ne se produit pas dans la fonctionnalité {CONTAINER}.puch_at, mais dans {ARRAY}.put ou similaire, qui - par coïncidence et convention de dénomination - utilise la même étiquette de précondition valid_index.

Il existe différentes façons de résoudre le problème:

1. Utilisez une structure différente pour le stockage (l'attribut container dans votre exemple), par exemple ce pourrait être HASH_TABLE [STRING, INTEGER]. Il devient alors possible de stocker des éléments à des index arbitraires.

2. Assurez-vous que le stockage est pré-alloué. Si vous connaissez la plage des index possibles, alors container peut être initialisé pour les utiliser tous depuis le début. Il peut être créé avec create container.make_filled ("", 1, N), où N est l'index maximum. (Je suppose que container est de type ARRAY [STRING].)

3. Ajouter les éléments un par un. Dans ce cas, la condition préalable de push_at doit vérifier si l'index fourni existe ou est adjacent au précédemment alloué une:

   require 
        valid_index: i >= 1 
        existing_or_adjacent_index: 
         container.valid_index (i) or else 
         container.valid_index (i - 1) 
   

   Le code de push_at doit être adapté pour utiliser la fonction qui va allouer un nouvel index si la un est fourni au-delà de la gamme d'indices attribués:

   container.force (s, i) 
   

Cosmetics: il n'y a pas besoin de répéter la déclaration de type dans l'instruction de création create {CONTAINER} con.make parce que le type de 012 variablesest CONTAINER. Donc, il suffit d'utiliser create con.make.