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

[Edmond Begumisa]

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.

- Edmond -


On Thu, 04 Nov 2010 03:58:12 +1100, Edmond Begumisa  
<ebegumisa@REDACTED> wrote:

> Here's an example of what I mean. Here is a UBF(B) contract copied from  
> Joe's UBF page (http://www.sics.se/~joe/ubf/site/quick.html)...
>
> +NAME("file_server").
>
> +VSN("ubf1.0").
>
> +TYPES
>
> info()         = info;
> description()  = description;
> services()     = services;
> contract()     = contract;
>
> file()         = string();
> ls()           = ls;
> files()        = {files, [file()]};
> getFile()      = {get, file()};
> noSuchFile()   = noSuchFile.
>
>
> +STATE start
>         ls()      => files()     & start;
>         getFile() => binary()    & start
> 		 | noSuchFile() & stop.
>
>
> +ANYSTATE
> 	info()        => string();
> 	description() => string();
> 	contract()    => term().
>
> (you can find the corresponding state machine implementation is  
> http://www.sics.se/~joe/ubf/site/eserve.html)
>
> ... you could achieve the exact same thing with gen_fsm combined with  
> TypEr/Dialyzer (I was doing just that), but the advantage to using the  
> UBF(B) contract instead is this info is declared in one place, as you  
> design and code away, then verified at runtime by the UBF(C) contract  
> checker. I find this approach more declarative and self-documenting.  
> IMO, state machines written against a UBF contract are much easier to  
> write, maintain, debug, document and modify than those written with  
> gen_fsm.
>
> Of course, to make use of this, you have to migrate to UBF(A) encoding  
> for the actual messages between processes. This usually only makes sense  
> if you're crossing OS process boundaries, and probably too costly for  
> communication between Erlang processes in the same VM instance.
>
> 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.
>
> - Edmond -
>
>
> On Wed, 03 Nov 2010 20:35:13 +1100, Torben Hoffmann  
> <torben.lehoff@REDACTED> wrote:
>
>> Hi Edmond,
>>
>> I am a bit confused by your statements since my problem was about
>> documentation of an _existing_ gen_fsm.
>> It might be my ignorance about what UBF can offer that is causing this  
>> (read
>> Joe's payer a while ago).
>>
>> As I understand UBF it allows you to specify what a component does so  
>> that
>> others can interact with it in a sensible manner and you can figure out  
>> if a
>> given component implements a given contract - or am I missing the point
>> here?
>>
>> I actually thought about using UBF, but when I looked at it it seemed a  
>> bit
>> to immature for a mission critical system, maybe that have changed by  
>> now.
>>
>> Do not get me wrong, I firmly believe in specifying protocols and UBF  
>> seems
>> like a very interesting thing to use, but in a real life situation you
>> sometimes have code that you want to extract information about and this  
>> was
>> the problem I was faced with.
>>
>> If I understand you right you are no longer using gen_fsm, right?
>> How do you piece together your software then?
>> I use the OTP supervisor structure all the time due to the obvious  
>> benefits
>> of a battle tested framework, but I would not mind adding another tool  
>> to my
>> tool box!!
>>
>> Cheers,
>> Torben
>>
>> On Wed, Nov 3, 2010 at 10:20, Edmond Begumisa
>> <ebegumisa@REDACTED>wrote:
>>
>>> Hi,
>>>
>>> I don't know how immediately useful this is (perhaps something to keep  
>>> in
>>> mind), but one of the attractive understated things about UBF is that  
>>> you
>>> define all this information in one place for both easy
>>> configuration/protocol-definition and reading/self-documentation...
>>>
>>> http://www.sics.se/~joe/ubf/site/quick.html<http://www.sics.se/%7Ejoe/ubf/site/quick.html>
>>> https://github.com/norton/ubf
>>>
>>> So far, I haven't regretted switching from gen_fsm to UBF(C)
>>>
>>> - Edmond -
>>>
>>>
>>>
>>> On Mon, 01 Nov 2010 05:58:35 +1100, Tomas Abrahamsson <
>>> tomas.abrahamsson@REDACTED> wrote:
>>>
>>>  On Tue, Oct 12, 2010 at 09:00, Torben Hoffmann  
>>> <torben.lehoff@REDACTED>
>>>> wrote:
>>>>
>>>>> Hi,
>>>>>
>>>>> I want to extract the following information from a gen_fsm:
>>>>>
>>>>>  - all the states
>>>>>  - the incoming events
>>>>>  - possible next states
>>>>>
>>>>> but I want to do it per function clause and not only on the function
>>>>> level
>>>>> as TypEr and Dialyzer does it.
>>>>>
>>>>
>>>> One way to do that is to copy each function clause into a
>>>> separate function.  Then one can run TypEr on the expanded
>>>> code.  Attached is an escript that does such an expansion
>>>> of exported functions of arity 2 and 3, and also of
>>>> handle_event, handle_sync_event and handle_info. The script
>>>> accepts -I and -D options for include paths and macro
>>>> definitions, just like erlc,and prints the expanded program
>>>> on stdout.
>>>>
>>>> I've tried plotting state machines from the output of TypEr
>>>> when run on the expanded results, and it seems to do reasonably
>>>> well. I haven't done any thorough verification.
>>>>
>>>> It doesn't solve all of your problems: it doesn't find any
>>>> outgoing messages, and it has the same limitations you
>>>> already indicated when returning from a function clause in
>>>> different ways, so I guess the results are roughly what
>>>> you already seems to have, or what Vance's drawing tool
>>>> already produces.
>>>>
>>>> Somehow being able to make more use of TypEr's
>>>> knowledge about a file would be really interesting,
>>>> for example to be able to query it for type information
>>>> given various execution paths through the program,
>>>> if it would be possible.
>>>>
>>>> BRs
>>>> Tomas
>>>>
>>>
>>>
>>> --
>>> Using Opera's revolutionary e-mail client: http://www.opera.com/mail/
>>>
>>
>>
>>
>
>


-- 
Using Opera's revolutionary e-mail client: http://www.opera.com/mail/