generated at
事前条件
サブルーチンの開始時に、これを呼ぶ側で保証すべき性質

事後条件と異なり、その関数の利用者側に要請される性質