Annotations Post/Précondictions et WSDL

Annotations Post/Précondictions et WSDL - Java - Programmation

Marsh Posté le 18-11-2010 à 18:25:01    

Bonjour,
 
Je voudrais utiliser des annotations sur les méthodes (ou autres) d'un Web Service pour donner une spécification formelle de la capacité du Web Service, en utilisant des préconditions (require) et postconditions (ensure). Bon un exemple simple de code source qu'on peut trouver sur Wikipedia est:
 

Code :
  1. public class CompteBancaireExemple {
  2.     private int solde;
  3.     private boolean isLocked = false;
  4.     //@ invariant solde >= 0 && solde <= 1000;  
  5.     //@ ensures solde == 0;
  6.     public CompteBancaireExemple() { ... }
  7.     //@ requires montant > 0;
  8.     //@ ensures solde == \old(solde) + montant;
  9.     public void crediter(int montant) { ... }
  10.     //@ requires montant > 0;
  11.     //@ ensures solde == \old(solde) - montant;
  12.     public void debiter(int montant) { ... }
  13.     //@ ensures isLocked == true;
  14.     public void lockCompte() { ... }
  15. }


 
Je voudrais ensuite que le consommateur du Web Service puisse avoir ces spécifications (annotations). Est ce que avec ces annotations, l'interface du Web Service (WSDL) que le consommateur aura, contiendra ces annotation ?
 
Merci.

Reply

Marsh Posté le 18-11-2010 à 18:25:01   

Reply

Marsh Posté le 19-11-2010 à 22:57:54    

up

Reply

Marsh Posté le 22-11-2010 à 22:06:35    

Ca peut peut être se documenter dans le WSDL/XSD mais à part ça t'attends pas à ce que ça impacte le code du langage qui viendra consommer ton service...


---------------
Réalisation amplis classe D / T      Topic .Net - C# @ Prog
Reply

Marsh Posté le 23-11-2010 à 00:30:53    

TotalRecall a écrit :

Ca peut peut être se documenter dans le WSDL/XSD mais à part ça t'attends pas à ce que ça impacte le code du langage qui viendra consommer ton service...


Quel est selon vous le moyen approprié pour que le consommateur du Web Service ait ces spécifications formelles (conditions pré et poste représentés comme des assertions logiques) ?
 
Le but c'est qu'en ayant ces assertions en place, le consommateur peut utiliser des techniques de raisonnement automatique pour prouver les propriétés du service, et l'utiliser dans une implémentation tout en ayant la possibilité de prouver qu'il est formellement correcte.
 
Merci.

Reply

Sujets relatifs:

Leave a Replay

Make sure you enter the(*)required information where indicate.HTML code is not allowed