 |
|
| Computers Forum Index » Computer Compilers » Integrated theorem prover in compiler... |
|
Page 1 of 1 |
|
| Author |
Message |
| bart demoen... |
 Posted: Wed Aug 19, 2009 4:13 pm |
|
|
|
Guest
|
On Wed, 19 Aug 2009 01:57:57 -0700, - - wrote:
Quote: 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 |
|
|
| Back to top |
|
|
|
| bart demoen... |
| Posted: Wed Aug 19, 2009 4:13 pm |
|
|
|
Guest
|
On Wed, 19 Aug 2009 01:57:57 -0700, - - wrote:
Quote: 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 |
|
|
| Back to top |
|
|
|
| Pertti Kellomaki... |
| Posted: Thu Aug 20, 2009 10:55 am |
|
|
|
Guest
|
- - wrote:
Quote: 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 |
|
|
| Back to top |
|
|
|
| Murali Sitaraman... |
| Posted: Sat Oct 17, 2009 12:55 am |
|
|
|
Guest
|
One of my colleagues brought this message to my attention. Those
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
------
Quote: 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. ... |
|
|
| Back to top |
|
|
|
|
|
All times are GMT
The time now is Sat Nov 28, 2009 10:43 pm
|
|