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

[Joseph Wayne Norton]

Edmond -

FYI.  There is a new UBF user's guide currently being drafted on github.

   http://norton.github.com/ubf/ubf-user-guide.en.html

There are still (well mostly all) quite a few empty sections that haven't  
been started yet.  Nevertheless, an ABNF definition of UBF(A), UBF(B), and  
UBF(C) is in the appendix.   The ABNF definition is complete and accurate  
with the github repository.

thanks,


On Thu, 04 Nov 2010 01:58:12 +0900, 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/
>>>
>>
>>
>>
>
>


-- 
norton@REDACTED