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