Questions and discussion on UBF

classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Questions and discussion on UBF

Fabien Dagnat-2
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
  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




Reply | Threaded
Open this post in threaded view
|

Questions and discussion on UBF

Erik Pearson-2
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
>  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



Reply | Threaded
Open this post in threaded view
|

Questions and discussion on UBF

Joe Williams-2
In reply to this post by Fabien Dagnat-2

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
>



Reply | Threaded
Open this post in threaded view
|

Questions and discussion on UBF

Fabien Dagnat-2
Hi,

Erik Pearson wrote:
 > Hi Fabien,
 >

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


Joe Armstrong wrote:
> 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
>
I agree with both of these answers, but I think they don't go against my
point of view.
Fact 1: if everyone is following the rule that every message must be
tagged, why not imposing it? Perhaps my proposal was to much different
from erlang and the solution would be to impose either Tag or {Tag,...}.
Fact 2: The interest of contracts (IMHO) is impose some rules to get
some guaranties.
Fact 3: In all my proposal the increment of complexity will only be:
   - on the contract checker that will have to include some state
management and basic boolean expression evaluation
   - on the contract compiler
I don't think they add complexity to all the machinery of types and
conversion and to the programs people (client) would have to write
(except from the contract).

Thanks
Fabien
--
Fabien Dagnat -- Ma?tre de Conf?rences
  Mel : Fabien.Dagnat
  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