Understanding Design By Contract (DbC)

Software development is a dynamic field, and as developers, we strive adapt to the changing environment and to push code to production seamlessly. However “seamless” often feels unattainable.  We like to create reliable, maintainable, and bug-free code but in reality this is almost never the case. One methodology that has gained prominence to achieving these goals is “Software Design by Contract.” In this blog, we will explore the fundamental concepts of Design by Contract, its significance in software development, and how it can elevate the quality of our code.

🚀 Join our DbC survey! 🌐 Share your insights, unlock exclusive access to results. Let's explore software development together! 💻✨ #DbCSurvey #TechInsights

What is Design by Contract?

Design by Contract (DbC) is a software design approach introduced by Bertrand Meyer¹ . DbC is influenced by the clear rules and responsibilities outlined in business contracts, similar to agreements between a client and a supplier. At its core, DbC involves defining a set of agreements, or contracts, between different parts of a software system. These contracts -comprising preconditions, postconditions, and invariants –  act as a formal agreement that each component must adhere to during runtime.

Preconditions and Postconditions in Detail

Understanding Preconditions: Preconditions define the conditions that must be true before a function or method is invoked. That is, what a function requires beforehand. What a function requires could be one of the following:

• Constraints on input parameters
• Constraint on state
• For example, a function calculating the square root should have a precondition (requires) that the input must be a non-negative number.

def calculate_square_root(x):

  """
  Calculate the square root of a non-negative number.
  		
  :param x: The non-negative number for which to calculate the square root.
  :requires: x >= 0  # The input must be a non-negative number.
  :ensures: result >= 0  # The result must be a non-negative number.
  :ensures: result * result == x  # The square of the result must equal the input.
   """
   result = x ** 0.5
   return result

Explanation of the DbC contract:

• :requires: x >= 0 : This specifies that the input x must be a non-negative number.
• :ensures: result >= 0 : This indicates that the result of the square root calculation must be a non-negative number.
• :ensures: result * result == x : This states that the square of the result should equal the original input x, ensuring that the calculated value is indeed the square root.

Understanding Postconditions: Postconditions specify the guarantees a function makes after successful execution. That is, what  a function guarantees (ensures) afterwards.  What a function guarantees could be one of the following:

• Constraints output parameters (including meaning) – “returns true only when successful, otherwise …”
• Constraint on state – “File is no longer open for write”
• Errors/Exception – “Throws “xxx” when …”
• Performance Limits – “Returns in 10ms or less”

If our square root function returns a result, the postcondition could state that the result squared equals the original input.

def calculate_square_root(x):

  """
  Calculate the square root of a non-negative number.
  :param x: The non-negative number for which to calculate the square root.
  :requires: x >= 0  # The input must be a non-negative number.
  :postconditions:
    - The output parameter 'result' is a non-negative number.
    - The output parameter 'result' squared equals the input parameter 'x'.
    - If an exception occurs during the calculation, the program state remains unchanged.
    - The function raises a ValueError if the input is negative, ensuring error handling.
    - The performance limit for the square root calculation is within acceptable bounds.	    
  """
  try:
    result = x ** 0.5
    return result
  except ValueError:
    # If the input is negative, raise a ValueError
    raise ValueError("Input must be a non-negative number")

Example Usage:

# Example usage:
try:
  result = calculate_square_root(9)
  print(f"Square root: {result}")
except ValueError as e:
  print(f"Error: {e}")

These contracts serve as documentation, making explicit the assumptions about the function’s input and the guarantees about its output. Developers can use this information to understand the function’s expected behaviour and make sure that the function adheres to these contracts during implementation.

1. Meyer, Bertrand. “Applying design by contract” Computer 25.10 (1992): 40-51 ↩︎