correctness proofs demonstrated with natural numbers

[Helmut]

I have written a paper to show how natural numbers without any
conceptual limitation (i.e. arbitrarily sized) can be implemented
and verified in Modern Eiffel. The fact that the implementation is
highly inefficient to execute is accepted. The implementation
shall serve as a model on how to implement inductively defined
data types in Modern Eiffel and on how to proof important
properties of the implemented functions.

Many correctness proof are given in full detail. Modern
Eiffel's proof engine can derive all these proofs
mechanically. The developer just has to state the properties.

The paper can be found at
http://tecomp.sourceforge.net/doc/paper/proof/math_nat.pdf

[Helmut]

Sorry, the link has been wrong!!!

correct link:
http://tecomp.sourceforge.net/index.php?file=doc/papers/proof/math_nat.pdf

[August Karlstrom]

The link seems to be broken.


August

--
The competent programmer is fully aware of the limited size of his own
skull. He therefore approaches his task with full humility, and avoids
clever tricks like the plague. --Edsger Dijkstra

[August Karlstrom]

On 2011-09-27 01:03, August Karlstrom wrote:
> On 2011-09-14 21:51, Helmut wrote:
>> The paper can be found at
>> http://tecomp.sourceforge.net/doc/paper/proof/math_nat.pdf
>
> The link seems to be broken.

OK, got it now. Seems like my newsreader didn't got your last post.

/August