Robustness and Contextual Code Verification:

Part 2: Contextual Verification

In part one of this two-part series, we discussed robustness code verification, a method in which you verify your unit of code in isolation from the rest of the code base. We outlined a few examples, and we discussed the pros and cons of using this approach.

In this post, we will discuss contextual code verification, in which you verify your unit of code in context of the code base where the unit will be integrated. This post will walk you through the concepts behind contextual code verification using the same examples as in the last post, and it will then outline the best practices for using both types of code verification (robustness and contextual).

In contextual code verification, there is some initial setup involved - you have to provide some context for the code you are verifying. For example, you have to provide:

  • A reasonable range for input variables.
  • Manual stubs to represent undefined functions.
  • The order in which functions are called by the main function, so that some are called before others. (This is necessary in case you do not provide an actual main function.)

But fear not. Although it sounds like a lot of work up front, this is a one-time setup for your unit. What do you get in return? You have fewer potential errors to review. Let us take the same examples as from the robustness code verification post. This time, before verifying, we use available options in Polyspace® products to provide context to the verification.

Providing Context to Inputs

Suppose you know that num1 and num2 cannot be equal. Neither can their difference exceed the range of a 32-bit integer. You can specify this information to the verification software. Polyspace products allow you to do this through a Data Range Specification interface where you can specify exact ranges of inputs.

Here is the result of the same verification. This time, it has been specified that num1 and num2 are in the ranges [100…200] and [0…10] respectively. As expected, both the division by zero and overflow errors do not appear. The code appears green in the Polyspace user interface, indicating that the software has proven the absence of these errors.

Robustness and contextual code verification

Result of the verification.

Providing Context to Undefined Functions

Suppose you know that checkDenominator does what its name suggests: It checks the value of the denominator but does not change it. Polyspace products allow you to specify this information through a Data Range Specification interface.

Here is the result of the same verification. This time, it has been specified that checkDenominator does not change the value stored in the address &den. As expected, a division by zero error is not shown. A tooltip on den during the division tells that den is still in the range [1...3] as it was during initialization.

Data range specification interface

Data range specification interface.

Yes, sometimes you have to make your best guess about input ranges. But if your inputs represent quantities in the real world, you or your client will have a solid idea about their ranges. And once you have verified your code for those ranges, you can always document them as safe ranges for your unit. If someone uses your unit with inputs outside those ranges, he or she is doing so entirely at his or her own risk.

Keep in mind: With contextual verification, there are always those ‘what if’s’ lurking in the back of your (or your manager’s) mind. You could be asking:

  • What if the context changes?
  • What if you do not know about all the contexts in which your unit might be reused? After all, we are asking you to verify your code as early as possible.
  • What if certification requirements ask you to have certain units verified against all possibilities? You might have to present a report illustrating that you did your due diligence.

Best Practices for Choosing Between Robustness or Contextual Code Verification

Before you start specifying contexts for your verification, a best practice might be to take a step back and ask the following questions:

  • How critical is your application?

If your code is intended for use in critical applications, you and users of your code will sleep better at night if you can ensure robustness of your unit. It might be better to perform robustness verification on your code.

Otherwise, even if you document all the safe ranges for your unit, you are still leaving room for another person to not read or follow your instructions. Robustness verification is a way to safeguard your code against any circumstance.

Also, sooner or later, you might have to meet certification requirements. You are one step ahead of the game if you are performing robustness verification on your unit and fixing or justifying all errors.

  • Do you know the entire set of requirements from your unit?

Can you write down a detailed specification of every other unit with which your unit will interact? Do you know the complete range of inputs that your unit will receive? If not, you would be better off verifying your code against all possibilities using contextual code verification.

You can also adopt a mix of robustness and contextual verification, where you provide ranges for some variables and not for others.

  • How likely is it that your code will be reused?

Are you writing a library function that can be called in many contexts? Are you writing the definition for a class that will be inherited from later? If so, you should ideally perform robustness verification on your code.

The more robust your code, the easier it is for you to reuse it in the future. If you verify your code in a narrow context, you severely limit its reusability. If someone intends to reuse your code outside that narrow context, he has to run the verification on your code all over again.

Once you have answered these questions, you can devise a verification strategy that suits your needs. At the end of the day, your strategy will be a compromise between absolute safety and making the best use of your time. Polyspace products can help you identify the weaknesses of your code, and it is up to you to decide how much context to provide.