Integrated theorem prover in compiler
- -
In Eiffel it is possible to specify a function precondition,
postcondition and loop invariants, but these are not statically
checked by the compiler (at compile-time), but instead run-time. An
exception is thrown if any assertion is violated, but of course this
only shows that for _that particular execution_ no assertion was
violated. I could not find any compiler that proofs correctness of a
given function at compile-time.
I have seen stand-alone tools that do statically verify correctness of
a function (for example: ESC/Java does (attempt to) verify correctness
of java code statically) but never integrated within a compiler
itself.
Integration of a theorem prover in a compiler has numerous advantages:
1) Users of the functions that have been verified only have to look at
the specification of the function, and not at the implementation for
an accurate description of what the function does
2) There is no need to check the assertions in a program at run-time
anymore if they already have been checked statically
3) There are many more opportunities to optimize code, since
assertions can be used to find out properties of the code the compiler
could otherwise never have found out (a simple example would be that
if the compiler knows an integer is always bounded between 0 and 255,
it just has to allocate 1 byte)
My question is: is there any compiler (for Eiffel, Java or any other
language) that statically checks assertions, and if so, does it
exploit any of the three advantages listed above?
[I'd be surprised. Theorem provers are slow, so for it to be at all
practical the compiler would have to cache its results so it could
skip the proofs it's already tried, and the proofs that are practical
tend to be trivial. I've always thought that the whole idea of
program proofs was backward--if you can describe the program's
behavior in the assertion language, skip the program and compile the
assertions. Also see
http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf -John]
bart demoen
> My question is: is there any compiler (for Eiffel, Java or any other
> language) that statically checks assertions, and if so, does it exploit
> any of the three advantages listed above?
Have a look at CIAO Prolog http://clip.dia.fi.upm.es/Software/Ciao/
It has assertions that are checked at compile time - maybe not what you
are after, but worth checking out.
AFAIK, the assertion language is extensible and so are the checkers.
Get in touch with Manuel Hermenegildo and/or Manuel Carro.
Cheers
Bart Demoen
Walter Banks
> 2) There is no need to check the assertions in a program at run-time
> anymore if they already have been checked statically
On this one small point we had support for user defined assertions in
a compiler that were checked statically when they could and left as
part of the source level debugging for the the emulation or simulation
environment to check. We found it to be a bad idea for several
reasons.
1) The developers were distracted for the the application algorithms
and tended to make more implementation errors.
2) As the application evolved some of the initial assumptions changed
and later in the development process the false failures were seen as
errors in the changes. Rather than analyse the application code the
assertions were treated as independent "correct" information.
Regards,
Walter..
--
Walter Banks
Byte Craft Limited
http://www.bytecraft.com
Pertti Kellomaki
> My question is: is there any compiler (for Eiffel, Java or any other
> language) that statically checks assertions, and if so, does it
> exploit any of the three advantages listed above?
There is at least SPARK Ada <http://www.praxis-his.com/sparkada/>,
and the toolsets associated with the B-method
<http://en.wikipedia.org/wiki/B-Method>.
You might also want to take a look at PVS <http://pvs.csl.sri.com/>
which kind of does it the other way around. There is a subset
of the theorem prover language that can be used as a functional
programming language, and mapped to Common Lisp. Not exactly
what you are asking for, but quite related. I just love the
predicate subtype mechanism in the language.
There is also Coq and other theorem provers where it is possible
to derive programs from proofs, but that is (at least to me)
quite a bit hairier.
--
Pertti
Torben Ægidius Mogensen
> My question is: is there any compiler (for Eiffel, Java or any other
> language) that statically checks assertions, and if so, does it
> exploit any of the three advantages listed above?
There is Spec#, a C# variant that statically checks assertions and for
null pointers etc. See
http://research.microsoft.com/en-us/projects/specsharp/
> Integration of a theorem prover in a compiler has numerous advantages:
> 1) Users of the functions that have been verified only have to look at
> the specification of the function, and not at the implementation for
> an accurate description of what the function does
The assertions are not full specifications, so this is not fully
exploited. The assertions do provide the necessary preconditions for
using a function, though, so you can see this from the specification.
> 2) There is no need to check the assertions in a program at run-time
> anymore if they already have been checked statically
It can certainly eliminate certain runtime checks such as null pointer
checks and range checks, but this is hindered by compiling to .NET,
which enforces such checks at runtime. Eiffel-style runtime checking of
assertions is avoided, though.
> 3) There are many more opportunities to optimize code, since
> assertions can be used to find out properties of the code the compiler
> could otherwise never have found out (a simple example would be that
> if the compiler knows an integer is always bounded between 0 and 255,
> it just has to allocate 1 byte)
Apart from (potentially) eliminating null-pointer checks and range
checks, I'm not sure to which extent this is exploited, but I can
imagine exploiting assertions in data flow analyses by, essentially,
using the assertions to filter the sets of values during analysis.
Torben
George Neuner
wrote:
>In Eiffel it is possible to specify a function precondition,
>postcondition and loop invariants, but these are not statically
>checked by the compiler (at compile-time), but instead run-time. An
>exception is thrown if any assertion is violated, but of course this
>only shows that for _that particular execution_ no assertion was
>violated. I could not find any compiler that proofs correctness of a
>given function at compile-time.
That's because, in general, only pure functions can be effectively
proved. You can make certain assertions about imperative code, but
not nearly as many as pure functional or declarative code. Introducing
side effects such as persistent data structures and general I/O
further complicate proofs because the proof becomes dynamically
context dependent.
>I have seen stand-alone tools that do statically verify correctness of
>a function (for example: ESC/Java does (attempt to) verify correctness
>of java code statically) but never integrated within a compiler
>itself.
ESC/Java does not verify correctness as doing so requires knowledge of
the intended algorithm being implemented. Instead ESC/Java looks for
evidence of commonly made coding mistakes that are known to lead to
runtime errors.
>Integration of a theorem prover in a compiler has numerous advantages:
>1) Users of the functions that have been verified only have to look at
>the specification of the function, and not at the implementation for
>an accurate description of what the function does
Assuming the code conforms to the specification ... which, for most
commonly used languages, is not a condition that can be automatically
verified.
>2) There is no need to check the assertions in a program at run-time
>anymore if they already have been checked statically
Assertions that depend on runtime values can't be checked statically.
>3) There are many more opportunities to optimize code, since
>assertions can be used to find out properties of the code the compiler
>could otherwise never have found out (a simple example would be that
>if the compiler knows an integer is always bounded between 0 and 255,
>it just has to allocate 1 byte)
You're forgetting that the assertion, being written separately from
the code, may be outdated, ill-fitted, or just plain wrong. This is
the equivalent of the compiler reading comments.
A better solution is to use a data type - either explicitly specified
or inferred by the compiler - that is restricted to the proper set of
values.
As for your example: using 1 byte for a 0..255 value could be much
slower than using a full sized machine word. Except in cases where
the size really matters - such as device register programming - it is
generally sufficient to define the value range or set and leave the
compiler to enforce the restriction however it pleases.
>My question is: is there any compiler (for Eiffel, Java or any other
>language) that statically checks assertions, and if so, does it
>exploit any of the three advantages listed above?
>[I'd be surprised. Theorem provers are slow, so for it to be at all
>practical the compiler would have to cache its results so it could
>skip the proofs it's already tried, and the proofs that are practical
>tend to be trivial. I've always thought that the whole idea of
>program proofs was backward--if you can describe the program's
>behavior in the assertion language, skip the program and compile the
>assertions. Also see
>http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf -John]
I'm not aware of any involving explicit theorem provers or assertions
as such, but the class of declarative languages - Prolog, Mercury, Oz,
etc. - have the property (to varying degrees) that the specification
of the problem solution is executable code. So, in essence, all you
ever write are assertions.
George
Robert A Duff
> I have seen stand-alone tools that do statically verify correctness of
> a function (for example: ESC/Java does (attempt to) verify correctness
> of java code statically) but never integrated within a compiler
> itself.
Other tools are SPARK (from Praxis) and Inspector (from SofCheck).
> Integration of a theorem prover in a compiler has numerous advantages:
0) It's more convenient than running a separate tool.
> 1) Users of the functions that have been verified only have to look at
> the specification of the function, and not at the implementation for
> an accurate description of what the function does
I don't see that. This seems the same, whether the proofs are done by a
separate tool, or integrated with the compiler.
> 2) There is no need to check the assertions in a program at run-time
> anymore if they already have been checked statically
Yes.
One possibility is to use something like SPARK to prove that assertions
are true, and then tell the compiler to suppress the run-time checks.
Anyway, many compilers do some small amount of this already. For
example, there's an implicit assertion that pointers are not null when
you dereference them:
while X /= null then
X := X.Next;
...
Many compilers can prove that X is not null in the loop,
and avoid a check.
As I said, "small amount".
> 3) There are many more opportunities to optimize code, since
> assertions can be used to find out properties of the code the compiler
> could otherwise never have found out...
Yes, but this seems essentially the same as point (2). If the compiler
can prove that such-and-such is true, then it can optimize based on that
fact.
>... (a simple example would be that
> if the compiler knows an integer is always bounded between 0 and 255,
> it just has to allocate 1 byte)
Well, this particular example is easy. For example, in Ada, if you say:
type T is range 0..255;
X : T := 100;
then the compiler can easily know that X can be allocated 1 byte.
No fancy proofs necessary. Fancy proofs might be necessary to prove
that "X := X + 1;" doesn't cause trouble.
> My question is: is there any compiler (for Eiffel, Java or any other
> language) that statically checks assertions, and if so, does it
> exploit any of the three advantages listed above?
> [I'd be surprised. Theorem provers are slow, so for it to be at all
> practical the compiler would have to cache its results so it could
> skip the proofs it's already tried, and the proofs that are practical
> tend to be trivial. I've always thought that the whole idea of
> program proofs was backward--if you can describe the program's
> behavior in the assertion language, skip the program and compile the
> assertions.
I don't buy that argument. In many cases, it's easier to check the
assertions (either at run time or statically) than to "compile" those
assertions into code that implements them. For example, consider a
square-root function. The requirement is that the result squared is
equal to the argument (plus-or-minus some epsilon). That's easy to
check, but hard to compile. The actual algorithm might be some
complicated loop that iterates toward the correct answer.
In other words, "Assert (Result*Result = Argument);" gives no hint to a
compiler how to efficiently produce Result, given Argument. "Just
compile the assertions" won't work in this case.
>... Also see
> http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf -John]
Yes, thanks for the link, that's worth reading.
- Bob
Murali Sitaraman
interested in this topic might be interested in RESOLVE. RESOLVE is
an integrated specification and implementation language that lets you
specify, develop, compile and verify the kinds of generic components
you may write in Java, C#, or C++. It is in some sense a response to
Tony Hoare's grand challenge; see his article in October CACM for a
short summary.
RESOLVE is a sourceforge project. Please see
www.cs.clemson.edu/~resolve for a current version of RESOLVE verifier
and compiler (actually, a translator to Java). I expect that a web
version will be posted at the site for trying out the
compiler/verifier within the next week.
RESOLVE is very much a research effort involving Clemson, Ohio State,
and several other institutions. While the group has made decent
progress, plenty of research questions remain (including specification
and analysis of memory usage constraints). The technical reports at
the site have details. See the ones on Push-button Verification and
Verification Vision, for example.
Thanks for any feedback.
Three points wrt follow-up messages to the original posting:
Any mathematical theorem used by the RESOLVE verifier must have a
mechanically-derived or mechanically-checkable proof (in other words,
theorems are not accepted based on "social processes.")
A verifier merely proves that code is correct wrt stated
specifications, so as was rightly pointed out in a follow-up, there is
still the separate task of checking that the specifications do indeed
capture requirements. Also, testing will be necessary to validate
code against customer requirements.
RESOLVE language and verifier are designed to verify software one
component at a time in a modular fashion.
Murali
------
> In Eiffel it is possible to specify a function precondition,
> postcondition and loop invariants, but these are not statically
> checked by the compiler (at compile-time), but instead run-time. An
> exception is thrown if any assertion is violated, but of course this
> only shows that for _that particular execution_ no assertion was
> violated. I could not find any compiler that proofs correctness of a
> given function at compile-time. ...