Next: Summary
Up: Design By Contract /
Previous: Verification Implementation
Design by Contract does nothing more than specify
where and what to verify. For example:
subroutine Quadratic_Roots (a, b, c, root1, root2)
! Input variables.
type(real), intent(in) :: a, b, c ! Equation coefficients.
! Output variables.
type(real), intent(out) :: root1, root2 ! Roots of the equation.
! Internal variable.
type(real) :: determ ! Determinant of the equation.
! Verify requirements.
VERIFY(Valid_State(a),1) ! The equation coefficients can
VERIFY(Valid_State(b),1) ! take on any real value, but
VERIFY(Valid_State(c),1) ! we can check for NaNs & Infs.
! Calculate roots.
determ = b**2 - 4.d0*a*c
VERIFY(determ>=0.d0,1)
determ = sqrt(determ)
root1 = (-b + determ)/(2.*a)
root2 = (-b - determ)/(2.*a)
! Verify guarantees.
VERIFY(Valid_State(root1),1) ! The roots can take on any real
VERIFY(Valid_State(root2),1) ! value, so only test Valid_State.
return
end subroutine Quadratic_Roots
Aside: type(real) is a gm4 macro for the F90 intrinsic real type.
Next: Summary
Up: Design By Contract /
Previous: Verification Implementation
Michael L. Hall