|Integrated theorem prover in compiler firstname.lastname@example.org (- -) (2009-08-19)|
|Re: Integrated theorem prover in compiler email@example.com (bart demoen) (2009-08-19)|
|Re: Integrated theorem prover in compiler firstname.lastname@example.org (Walter Banks) (2009-08-19)|
|Re: Integrated theorem prover in compiler email@example.com (Pertti Kellomaki) (2009-08-20)|
|Re: Integrated theorem prover in compiler firstname.lastname@example.org (2009-08-20)|
|Re: Integrated theorem prover in compiler email@example.com (George Neuner) (2009-08-20)|
|Re: Integrated theorem prover in compiler bobduff@shell01.TheWorld.com (Robert A Duff) (2009-08-20)|
|Integrated theorem prover in compiler MSITARA@clemson.edu (Murali Sitaraman) (2009-10-16)|
|From:||Pertti Kellomaki <firstname.lastname@example.org>|
|Date:||Thu, 20 Aug 2009 09:55:35 +0300|
|Posted-Date:||20 Aug 2009 10:26:05 EDT|
- - wrote:
> 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
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.
Return to the
Search the comp.compilers archives again.