Thu, 20 Aug 2009 09:55:35 +0300

Related articles |
---|

Integrated theorem prover in compiler cdegouw@gmail.com (- -) (2009-08-19) |

Re: Integrated theorem prover in compiler bmd@cs.kuleuven.be (bart demoen) (2009-08-19) |

Re: Integrated theorem prover in compiler walter@bytecraft.com (Walter Banks) (2009-08-19) |

Re: Integrated theorem prover in compiler pertti.kellomaki@tut.fi (Pertti Kellomaki) (2009-08-20) |

Re: Integrated theorem prover in compiler torbenm@pc-003.diku.dk (2009-08-20) |

Re: Integrated theorem prover in compiler gneuner2@comcast.net (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 <pertti.kellomaki@tut.fi> |

Newsgroups: | comp.compilers |

Date: | Thu, 20 Aug 2009 09:55:35 +0300 |

Organization: | Compilers Central |

References: | 09-08-030 |

Keywords: | theory, optimize |

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

<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

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.