[bitc-dev] Abstract Interpretation primer

[Valerio Bellizzomi]

On 02/08/2005, at 10.54, Dominique Quatravaux wrote:

>C Y wrote:
>
>>Is it possible to prove at least some properties for non-terminating
>>programs? 
>>
>It's of course not possible to prove them in an algorithmic fashion (all
>the time, in bounded time, no false positives/negatives): deciding most
>interesting properties of a program is a superset of the well-known
>Turing halting problem. But the halting problem catch-22 does not
>theoretically rule out sort-of expert systems that can answer "yes",
>"no" or "I don't know" to questions such as "does this program
>terminate", "does it violate memory policy so-and-so", "does it throw
>exceptions", and so on.

I am trying very hard to see what kind of "certitude" this expert system
can give us, but really I don't see any unless the expert system is
verified not to violate itself the same rules it tries to
catch...apparently like a chicken and egg issue, very recursive and nested,
but only apparently.

This reminds the "comma 22" story: "a faulty program can request to be
terminated, but no program that requests to be terminated is considered
faulty."

:-)

val