Re: Questions and discussion on UBF

I think the answer to most of these questions has to do with complexity.

  At the outset  I wanted things to be *as simple  as possible* - that
why things  are as they are. If  you want more complexity  I think you
should layer them on top of the existing infratructure.

  /Joe



On Mon, 28 Apr 2003, 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...
> 
> 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
>