Home » forums » LtU Forum

A proof engine for Eiffel

The following paper describes a proof engine for the Eiffel language.

The proof engine allows the verification of the assertions of Eiffel
code. Some language extensions are introduced to express proofs of
assertions. Within the proofs the user can enter proof commands and the proof
engine can verify the correct use of the proof commands.

Modularization techniques are introduced to the keep the proofs small and
expressive.

The proof engine has some improved features to do the burdensome work for the
user. It is expected that the developer enters the key assertions and proves
them and the proof engine can verify the routines using the key assertions.

- In the first chapter the basic concepts are explained.

- The second chapter introduces the commands of the proof engine.

- The third chapter shows how basic properties of boolean expression can be
proved with the proof engine.

- The forth chapter applies the proof engine to assertions within the class
INTEGER

- The fifth chapter shows how routines can be proved.

Find the detailed paper at http://tecomp.sourceforge.net (manual navigation: http://tecomp.sourceforge.net -> white papers -> verification -> proof engine)

By hbrandl at 2010-07-07 18:38 | LtU Forum | previous forum topic | next forum topic | other blogs | 5863 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Imperative component

I have worked with Isabelle/HOL and the functional part of the paper seems to be similar to Isabelle/HOL (just in Eiffel syntax).

The interesting part is the chapter with applies the proof engine to imperative code. However that chapter is relatively compact. I would like to see more examples on imperative code.

By hlb at Wed, 2010-07-14 14:04 | login or register to post comments

As soon as I find more time,

As soon as I find more time, I will provide more examples for imperative code.

By hbrandl at Thu, 2010-07-15 12:59 | login or register to post comments

functional sublanguage

The sublanguage used in asssertions of Eiffel is functional in the sense that it is side effect free. It is interesting to see that the functional sublanguage must be powerful enough to be usable to prove the imperative routines.

Therefore I am quite impressed to see that the best of both worlds can be combined: The functional world for its expressiveness and the imperative world to get runtime efficiency.

By hlb at Mon, 2010-07-19 12:11 | login or register to post comments

This thread is beginning to

This thread is beginning to look suspicious. If there is no interest in the community, I suggest you stop posting to it.

By Ehud Lamm at Mon, 2010-07-19 16:36 | login or register to post comments

Interest from the community

Interest of the community in a thread is indicated by people posting to it. The 'paper' is on-topic for LtU. (More an issue is its organization, and the irritating ipligence 'feature'.)

By dmbarbour at Mon, 2010-07-19 20:06 | login or register to post comments

Check out the usernames of

Check out the usernames of the people posting.

By Jules Jacobs at Mon, 2010-07-19 20:26 | login or register to post comments

I dunno

Are you suggesting these accounts are the same person? Would someone who's making a fake account to answer his own question use his real initials?

By Matt M at Mon, 2010-07-19 21:07 | login or register to post comments

Bayesian Reasoning

Well, that's only one of (at least) two relevant questions. Another is the probability of a fake account versus the probability of two people with the same initials that are specifically interested in a proof engine for Eiffel. Peter Norvig explains the fallacy of confusing P(H|E) with P(E|H) quite nicely. ;-)

By Leon P Smith at Tue, 2010-07-20 05:02 | login or register to post comments

Fallacies

Don't forget that the only reason you're considering the probability of identical initials is because we have just observed such a thing.

By Matt M at Tue, 2010-07-20 16:16 | login or register to post comments

Sorry for the irritating

Sorry for the irritating `ipligence' feature. I will try to make it invisible. Can you give specific feedback on the `organization'.

Since it is work in process I am happy with any feedback to improve the paper to make it better readable and understandable.

By hbrandl at Mon, 2010-07-19 22:02 | login or register to post comments

Suggestions for Organization

  • Could you provide postscript or PDF? or an all-in-one-page option?
  • Navigational links. E.g. there should be a link to 'Next: Basic Concepts' from 'Introduction'
  • Also, add a direct link to your paper into the OP of the LtU node, rather than directions on how to navigate your page.
By dmbarbour at Mon, 2010-07-19 22:34 | login or register to post comments

Direct Linking

Add a direct link to your paper into the OP of the LtU node, rather than directions on how to navigate your page.

Indeed =)

By Leon P Smith at Tue, 2010-07-20 05:30 | login or register to post comments

done

done

By hbrandl at Sat, 2010-07-24 21:09 | login or register to post comments