Questions and discussion on UBF

[Erik Pearson]

Hi Fabien,

Quite a lot to chew on -- I'll bite off just one piece!

On Monday, April 28, 2003, at 07:16 AM, Fabien Dagnat wrote:

> 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...

I think I see what you mean here, but please correct me if not. This 
would basically be extending the UBF(C) from

   Msg$  => {Reply, NextState}$

to

   {SendTag, Msg}$ => {ReplyTag, Reply, NextState}$

In short, I think this would start breaking down the simplicity of UBF. 
Can't you get that just by always using types which are structures, and 
having the first element be a constant which serves as your tag?



>
> 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@REDACTED
>  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
>
>
>
Erik Pearson
Adaptations
desk +1 510 527 5437
cell +1 510 517 3122