[erlang-questions] Extracting detailed information from TypEr /Dialyzer

[French, Mike]

> On Thu, 04 Nov 2010 03:58:12 +1100, Edmond Begumisa  
> <ebegumisa@REDACTED> wrote:
> 
...
> > Actually, there's an idea: maybe someone should write a contract checker

> > for gen_fsm that uses ordinary Erlang-terms rather than UBF(A) encoding.

> > This could then be used in the same VM instance without much cost and  
> > make working with gen_fsm more dependable by allowing you to declare how

> > the state-machine is supposed to behave and cross check that against how

> > it's actually behaving -- a major frustration I've had when using  
> > gen_fsm.

> -----Original Message-----
> From: erlang-questions@REDACTED 
> [mailto:erlang-questions@REDACTED]On
> Behalf Of Edmond Begumisa
> Sent: 03 November 2010 19:55
> To: Torben Hoffmann
> Subject: Re: [erlang-questions] Extracting detailed information from
TypEr/Dialyzer
> 
> A better way of putting it...
> 
> While you can look at UBF(A) and UBF(C) as a formal approach to protocols,

> what's relevant here, is that from Erlang's perspective, you can look at  
> UBF(B) as a formal approach to state machines providing type checking and

> declarative state transitions. This can be very helpful at all levels of  
> development of a state machine from design right though to coding,  
> debugging and documentation.
> 
> That's more what I was trying to say.

A good point, nicely put.

It seems a pity to restrict UBF to external communication 
when we also need specification of internal messsaging.
Can we go further and say that UBF(B), or close variant,
could be incorporated into the Erlang type system, as a 
declarative signature for message protocol contracts on processes. 

We already have -type and -spec, 
maybe there are -send and -recv statements to be made
about what messages can be sent or received by a process.

Some -spec'ed methods are also process loops, 
with process state as their arguments.
In some cases, the continuous space of arguments 
could be pattern-matched into a finite set of states,
which might still be useful even if the mapping is partial
(rather than the total mapping built in to gen_fsm by design).
Perhaps there is are -proc statements based on UBF(B) 
that correlate the states and the send/recv specifications. 

Mike


Thales UK Ltd (Wells) DISCLAIMER: The information contained in this e-mail
is confidential. It may also be legally privileged. It is intended only for
the stated addressee(s) and access to it by any other person is
unauthorised. If you are not an addressee, you must not disclose, copy,
circulate or in any other way use or rely on the information contained in
this e-mail. Such unauthorised use may be unlawful. We may monitor all
e-mail communications through our networks. If you have received this e-mail
in error, please inform us immediately on sender's telephone number above
and delete it and all copies from your system. We accept no responsibility
for changes to any e-mail which occur after it has been sent.  Attachments
to this e-mail may contain software viruses which could damage your system.
We therefore recommend you virus-check all attachments before opening.
Thales UK Ltd. Registered Office: 2 Dashwood Lang Road, The Bourne Business
Park, Addlestone, Weybridge, Surrey KT15 2NX Registered in England No.
868273