[M3devel] ESC

[Daniel Alejandro Benavides D.]

Hi all:
in fact there was another ESC written exclusively for the purpose of finding the time complexity (from source) of multi-threaded programs, but this would be another approach to find whether ESC system and its proof machine (Simplify) will perform OK using it in normal basis, at the average case scenario (but Simplify has unsoundnesses and program-dependent checker coming from ESC front end), at least in a programming environment like Modula-3 to have the class of complexity of a programming model is something I want. 
However there is proof of such an environment used for big SW development at IBM, which targeted Modula-3, was not good without formal software analysis (in both fronts, development and performance)
Thing is I don't how many studies of Software developers given by a systematic analysis are aside  of IBM 80's and some more for Modula-3 theres later.
So based in experience I can infer it's good, but in the real world I don't know how many will buy the idea not backed by some real good experience and with some real proof. Anyone else :)  
Thanks in advance

Thanks in advance

--- El mar, 19/6/12, Hendrik Boom <hendrik at topoi.pooq.com> escribió:

De: Hendrik Boom <hendrik at topoi.pooq.com>
Asunto: [M3devel] ESC
Para: "m3devel" <m3devel at elegosoft.com>
Fecha: martes, 19 de junio, 2012 12:00

On Tue, Jun 19, 2012 at 05:28:33PM +0100, Daniel Alejandro Benavides D. wrote:
> Hi all:
> I don't think is so much a waste of time, if compiler has done well, you don't need to make a debugger, but instead if it hasn't done it well, don't waste more time use a different compiler (optimized).
> ESC had a X postfix for every package name that has been verified so you could have a different verified and compiled version and as a reference for program behavior and then use an experimental debug able version.
> That was the idea with a Module system with separate compilation and version stamps, IMHO, to really have a fast to execute and easy to debug around cycle and you need that lately as compiler versions are getting faster or harder to debug.
> The interesting stuff is whether you could use the same infrastructure to verify in less time or not, that will proof ESC is worth of anything which I'm sure no body uses for that reasoning broken -not Dragisha's nor Hendrick- but most people do ahead of time.
> Thanks in advance
> 
> --- El mar, 19/6/12, Dragiša Durić <dragisha at m3w.org> escribió:

Yes, I agree. It would be worthwhile to track down the ESC source code.  
Or rewrite it.

But until that's been done I'll probably need a debugger.  And maybe 
occasinoally afterward, for the things that ESC doesn't catch.

-- hendrik
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://m3lists.elegosoft.com/pipermail/m3devel/attachments/20120619/291507ce/attachment-0002.html>