next up previous
Next: Summary Up: Design By Contract / Previous: Verification Implementation

Design By Contract 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 up previous
Next: Summary Up: Design By Contract / Previous: Verification Implementation
Michael L. Hall