Questions and discussion on UBF

Hello,
As I am working on using contracts on component (or service, if one 
prefer) oriented specifications, I'm looking at UBF.


I'm asking myself why allowing any type for messages in the contracts. I 
know that this is linked with the fact that in Erlang a message may be 
of any type. But:
  - a programming rule specifies that all messages should be tagged.
  - as a "universal" format, it should conform to other language
    culture too.
Indeed, in a more abstract view (than erlang usual one), it would be 
"better" to name (give a tag) messages (from a specification point of 
view). Combined with some (yet to completly implement) type system, it 
would perhaps be possible to ensure that a server respect its contracts...

My second question is why just allowing named type in the automaton 
description.
More precisely why not having something like:
+STATE start
       ls            => files()     & start;
       {get, file()} => binary()    & start
                     | noSuchFile() & stop.
Is there any technical (or philosophical) limitation that I haven't 
thougth of? I think it would save type definitions and help reading the 
automaton (without always shifting to type definitions to remember what 
are the message types). I know that the current syntax is similar in 
this point to the message definition in WSDL, but I don't see WSDL as a 
panacea of XML encoding of interfaces.

Next, to go back to my point on universality. Why not having:
+STATE start
       ls()                 => files()     & start;
       get(file : string()) => binary()    & start
                            | noSuchFile() & stop.
My point here is that I would like to add to the contract some pre and 
post conditions and to do this usually we have to refer to some 
arguments of the message. Furthermore, to do this, I would like to add 
some state variables to the state.
For exemple, a bank account contract could be:
+STATE start
  open() => ok() & created.
+STATE created
  deposit(sum : int()) => ok() & credit(sum).
+STATE credit(balance : int())
  deposit(sum : int())  => if (sum > 0) ok() & credit(balance + sum);
  withdraw(sum : int()) => if (sum <= balance) ok() & credit(balance - 
sum);
  balance()             => {ok, sum} with sum = balance & credit(balance).

I don't advocate that this is a great example of the interest of pre 
and post conditions. But, I think it is sufficiently interesting to 
illustrates what I was thinking of.

It is clear that this way of thinking contracts embed a lot more 
(behavioral) semantics that the current UBF. Indeed, it shift some part 
of the server state to the "contract checker". But, it could gave some 
interesting property like the fact that the "contract checker" could use 
several servers giving them the needed state with the message (we would 
get some fault tolerance or some load balancing capacity).

Finally, why not allowing a return state in the ANYSTATE declaration. 
Suppose, I would like to have a stop message available in all states 
that brings the server in a stopped state. For example,

+STATE stopped
  start() => ok() & s1.
+STATE s1
  ...
+STATE s2
  ...
+ANYSTATE
  stop() => ok() & stopped.

Thanks in advance for any answer, opinion, criticism...

Fabien
--
Fabien Dagnat -- Maître de Conférences
 Mel : Fabien.Dagnat@xxxxxxxxxxxxxxxx
 Web : perso-info.enst-bretagne.fr/~fdagnat/index.php
 Tel : (0|33) 2 29 00 14 09
 Fax : (0|33) 2 29 00 12 82
 Adr : Ecole Nationale Superieure des Télécommunication de Bretagne
       Departement Informatique
       Technopôle Brest Iroise
       BP 832
       29285 Brest Cedex