James J. Horning: Verification of Euclid Programs. Program Construction 1978: 164-173