[M3devel] MODULEs in .M3IMPTAB

[Daniel Alejandro Benavides D.]

Hi all:
yes, I think I did mention it in a past message because about the ESC, it needes as it m3tk too, I didn't know it was a requirement of m3tk though. But because is just a module dependency analyzer I thought we could just create one in m3tk, sort of a chicken and egg problem it seems now. OK, I with an older cm3 we could use it to build it in a setting and then supply itself in m3tk, if that's the way to go, therefore I think this is really needed for ESC release.
Another thing if you allow me is about again the ESC itself, I think that one of the ways we could improve some of the ESC checks is to reuse some sort automatic program debugger I already mentioned about Juno which language has a subset of Simplify language so we could try to postprocess further errors to guarantee they are so and the more important it could be possible to think in analyzing checks for soundness so we may try to put closer Simplif0y to its (in results terms) goal of finding more errors it can catch. That said I would go for double checked proofs so me can arguably guarantee they are sound proved theoretically and passing through it Simplify again, all of this without modification to ESC per se. This is traditional approach for debuggers, so its not a new idea again, just that we need to be smarter in certain way to catch with the less computation effort the most bugs we can. Another thing I was thinking was to integrate this proofs in
 regular builds so for example a given all program proofs modified by the debugger should be presented as warnings of error and something that must be checked closely (supervised).
Ok, let mw now your thoughts on this points, thanks in advance

--- El sáb, 5/3/11, Mika Nystrom <mika at async.caltech.edu> escribió:

> De: Mika Nystrom <mika at async.caltech.edu>
> Asunto: Re: [M3devel] MODULEs in .M3IMPTAB
> Para: "Tony Hosking" <hosking at cs.purdue.edu>
> CC: m3devel at elegosoft.com
> Fecha: sábado, 5 de marzo, 2011 17:53
> 
> Tony, are you sure?  There don't seem to be any tools
> in CM3 that process
> implementations with m3tk, or have I been looking in the
> wrong places?
> stubgen doesn't, I don't think stablegen does, and m3pp and
> m3tohtml
> don't even use m3tk.  Also it doesn't seem to work on
> PM3-1.13.2.  Hmmmmm....
> 
>      Mika
> 
> Tony Hosking writes:
> >It used to work... :-(
> >
> >On Mar 5, 2011, at 3:06 PM, Mika Nystrom wrote:
> >
> >> Hi again m3devel,
> >> 
> >> Can anyone think of a reason that cm3 should *not*
> emit information
> >> about MODULEs that it compiles to .M3IMPTAB? 
> (It doesn't, today,
> >> which means that m3tk-based tools can't find
> implementations, only
> >> interfaces.)
> >> 
> >>    Mika
>