[M3devel] gui problems? BadBricks? columns?

[Daniel Alejandro Benavides D.]

Hi all:
it makes and abstraction of the code in terms of Guarded commands of Dijkstra, then applies the static checking of the calculus of weakest preconditions type checking as a normal program too the code and then translates to first order logic formulae, if the annotated program can be satisfied then it will give no output, but if does prove that the program doesn't produce the anottated output, it will complain on where it fails, wherever it doesn't like the proof.
The important thing is that if the checker satisfies all of his conditions, it doesn't mean it does not break, i.e it could be that the checker will no complain but still can't prove absolutely that is not to crash, is a kind of liberal, perhaps because of its logic calculus.
There is also the case of possible false alarms, which could be triggered, but this is almost the case in any compiler and here too, even the M3 compiler (something called completeness, just very simple known type systems have), so we can't expect to type check in the semantic analyser it wrong and to accept it in the checker, but we could instead just to make that a unsound program, lets say unsafe, will not lock or crash because and specific error because of the non-completeness issue. However the ESC didn't accept some special kind of almost safe programs, recursive, partly I believe because of a problem exposed below, is perhaps that the program doesn't end, unlike a for loop. 
There is also the need of a efficient and smarter automatic theorem prover, Simplify is one of the best available for some time now, but still, the same problems arise on it, it could be that because of the first order logic, the program could not terminate but the prover believe it will and it apparently does it, but that its proofs will be not totally proved for all cases, if so, then we would need to take care of those by applying hand formal verification measures like below I explain a case.
Also Simplify could rise that he can't prove that something is not provable by itself, but turn that it is doable, just that it can't by its own, so we need to also verify those cases.
In the end, the best case our checks will end, but sometimes, the first order logic could be an endless proof or undefined, in those cases we would need a threshold given by the experience, so we might start sooner than later to make our own.
The best of this is that are many things that have room for improvement as Dr Greg Nelson told me some time ago, would be nice thing to have the TODO list from him.
My personal wish is to make Modula-3 totally verifiable, learning this by hand would be harder, but by the tools we could make it for using its internal logic, the most critical part, the Professor Greg Nelson did some work on that part of that I believe.
Then the important parts are the semantic checker which it self is built on its internal logic, e.g a biased logic (i.e an unsound one, the proofs could not end or be too large to finish and unable to realize that after it spends time on it) it could be that never ends a proof or check it badly as good, the most perfect it checks it would be less efficient at some point (perhaps this was the reason to not check the total correctness besides the effort needed) so might be easier to pass the checks but less profitable in the checking. I really would like the most inner parts to be self provable, like more functional style programming then, but those are not verifiable by the ESC checker, it just doesn't do that, similar to when I had a problem on the checker I used sasylf.org, it had unimplemented the mutual induction proving part by that time of a course back in 2008, this is a theorem proof technique you need to use in advanced type theory of type system
 soundness proofs, sasylf is a programming language by itself to proof it is sound, so it turns out that if we can trust on them more than in any part of the checker we could move on from there to more advanced techniques, also this is harder I believe based on my small experience of type systems proofing. 
ESC developers say, the most provable source of those mis-checkings is automatic theorem prover, not in checker, then it might be more valuable to start there than in the checker's logic by itself, being more practical, more pragmatic. I have some experience with the use of automatic theorem provers part use by hand with sasylf, writing the proofs and let it check for one (say I was the ESC checker and sasylf was the automatic theorem prover), and it turns out not to be so difficult to use after some work and time of use, still there are many challenges open in the checkers for now, so the room for improvements there is also too big (i.e we can check more things, say, the Modula-3 arithmetic over and/or under flow, recurrence, by improving the core logic calculus and later working on the "second pass" or backend first order logic prover).
A special feature was the Locking level notation developed by writing the Trestle library, as it was coded threaded, it is perhaps the most advanced part of it, more details than that I don't now, but more probably coming on the way. I just know its logic is more advanced from what I recall, it requires some clever reasoning and calculus too I guess.
So we can have a lot discussion, perhaps the first kick is given now. I also hope its not too much blah, ... sorry for the long message
Thanks in advance 

--- El mié, 29/12/10, Hendrik Boom <hendrik at topoi.pooq.com> escribió:

> De: Hendrik Boom <hendrik at topoi.pooq.com>
> Asunto: Re: [M3devel] gui problems? BadBricks? columns?
> Para: m3devel at elegosoft.com
> Fecha: miércoles, 29 de diciembre, 2010 22:26
> On Wed, Dec 29, 2010 at 08:23:12PM
> -0500, Coleburn, Randy wrote:
> > Daniel et al:
> > 
> > I tried a year or so ago to pursue getting the sources
> for the ESC.
> > I'd have to dig up my old emails, but my recollection
> is that I ran into a dead end getting the sources and the
> permission to put them in our repository.
> > I don't think the Modula-3 edition was kept up when
> the project moved on to other languages.
> 
> What does the ESC do that's relevant to threading?  I
> mean, not just an 
> answer like "deadlock and race detection", but what
> algorithms does it 
> use to accomplish it?  Does the Modula 3 compiler
> construct the proper 
> data structures that could provide the raw data those
> algorithms would 
> need?  How much work would it be to reimplement this
> from scratch?
> 
> -- hendrik
>