Archive

Posts Tagged ‘formal verification’

Verifying the Liskov Substitution Principle in C++ code: Part 1

March 25, 2015 Comments off

When RTCA released DO-178C – the long-awaited update to the DO-178B standard for airborne software – they added a number of supplements to cover specific software development techniques. One of those techniques is object-oriented software development, covered by supplement DO-332. This supplement mentions the Liskov Substitution principle (hereafter abbreviated LSP) in FAQ #14 “Why is the Liskov Substitution Principle (LSP) important?” and gives more detail in FAQ #15 and #16. So, what is the LSP, and how can we make sure that a software design adheres to it? Read more…

Verifying pointer arithmetic

July 16, 2010 4 comments

Today I’ll look at whether code that uses pointer arithmetic is any harder to verify than equivalent code that does not use pointer arithmetic.

Consider this function for copying an array (or part of an array) into another array (or part of another array):

void arrayCopy(const int* src, int* dst, size_t num) {
  size_t i;
  for (i = 0; i < num; ++i) {
    dst[i] = src[i];
  }
}

Read more…

Aliasing and how to control it

June 22, 2010 4 comments

Today I’ll start by writing a simple function that determines the maximum and minimum of two integers. We want to return two values, and C doesn’t make that easy unless we declare a struct to hold them. So I’ll pass two pointers to where I want the results stored instead. Here goes:

#include "arc.h"
 void minMax(int a, int b, out int *min, out int *max)
post(*min <= a; *min <= b; *min == a || *min == b) post(*max >= a; *max >= b; *max == a || *max == b)
{ *min = a < b ? a : b;
  *max = a > b ? a : b;
}

I’ve highlighted the ArC annotations in green. Read more…

Verifying absence of integer overflow

June 7, 2010 2 comments

One class of errors we need to guard against when writing critical software is arithmetic overflow. Before I go into detail, I invite you to consider the following program and decide what it prints:

#include <stdio.h>
int main(int argc, char *argv[]) {
unsigned int x = 42;
long y = -10;
printf("%s\n", (x > y ? "Hello, normal world!" : "Hello, strange world!"));
return 0;
}

Read more…

Verifying a binary search, part 2

May 6, 2010 2 comments

In my last entry I showed how to use a correct-by-construction approach to develop a binary search function. We got as far as specifying the function and the loop, but we left the loop body undefined. The function declaration looked like this: Read more…

Verifying a binary search

May 5, 2010 Comments off

In the last post, I covered some different levels of formal verification that you may be interested in, and showed how to add minimum annotation to the linearization example to allow ArC to prove predictable execution. The example provided a prototype for the binary search function it called, to which we added a minimal postcondition, so that it looked like this:

size_t bSearch(const LinEntry* array table, size_t nElems, uint16_t key)
 post(result <= nElems);

Read more…

What are you trying to prove?

April 27, 2010 9 comments

If you’re thinking of using formal verification to increase the quality and reliability of your software, one of the first decisions you need to make is what you want to prove. Roughly speaking, you have three levels to choose from: Read more…