[m-dev.] Inductive goals

[Mark Brown]

On Thu, Jan 23, 2014 at 3:21 PM, Michael Richter <ttmrichter at gmail.com> wrote:
> On 23 January 2014 10:20, Peter Schachte <pschachte at gmail.com> wrote:
>>
>>     $X from $Start to $End by $Func
>>
>> which is equivalent to {$X,Func($X)} folds {$Start,$End}
>
>
> It's also equivalent to FOR X = 1 TO 100 STEP 3, just a bit more general.  I
> thought I'd left that behind me in the '70s.  It appears Dijkstra may have
> been right.

Are you referring to this:

    "No loop should be written down without providing a proof for termination
    nor without stating the relation whose invariance will not be destroyed by
    the execution of the repeatable statement." [0]

?

Cheers,
Mark.

[0] http://www.cs.utexas.edu/~EWD/transcriptions/EWD03xx/EWD340.html