3 ms·
AutoProof – A Program Verifier for Eiffel (2015)
- jweir 8y agoI posted this after reading the discussion "Why not program right?" https://news.ycombinator.com/item?id=17466277 https://news.ycombinator.com/item?id=17466277 I'm not familiar with Eiffel and this AutoProof give a clear example of of its syntax, and methodology. At first glance it seems a little bit silly - the old keyword. Why not use immutable values?
- detaro 8y agoHow would immutable values be better? Can you give an example for what you'd prefer? Note that "old" only is valid in the conditions/contracts, not the main function body.
- jweir 8y agoI am naive on the language and have not used it. At first I thought you could get around using `old` by assigning the new balance to a property `new_balance`, but that won't work since this is an object's property so of course it must be set. I see the value and purpose now.