加藤＠ＯＤＮです．

In article <YAS.04Sep15033225@kirk.is.tsukuba.ac.jp>, Yasushi Shinjo wrote:
>新城＠筑波大学情報です。こんにちは。
>
>In article <chv1ld$151j@utogw.gssm.otsuka.tsukuba.ac.jp>
>    kuno@gssm.otsuka.tsukuba.ac.jp writes:
>> >     i            10
>> > s + Σ data[k] = Σ data[k]
>> 部分和の範囲が逆でした…ループ範囲も9まででした…
>>       9            9
>>  s + Σ data[k] = Σ data[k]
>>      i+1           0
>>                   しょうもないですね ^_^;          久野
>
>わりと、本質を付いているんじゃないですか。つまり、
>
>・Ｃ言語で総和のプログラムを書くより、ループ不変量を書く方が難しい

ある定理の証明を書くより，その証明が正しい事を示す方がずっと難しいん
だから，これは当たり前ではありませんか？　なんとなくですが，難しさの
順は，，，

　証明を書く < 実行可能な証明を書く << その証明を検証する

の様な気がします．
＃実行可能な証明はプログラムに対応（？)．
-- 
Hideki Kato <mailto:katoh@pop12.odn.ne.jp>