>>883
>>876にはプログラムの正当性や検証の話は全然出てこないのですが。