Posts Tagged ‘formal verification’

Verifying loops: proving termination

March 31, 2010 6 comments

If you’ve stuck with me so far in this mini-series on verifying loops, give yourself a pat on the back  before reading further. When it comes to formal verification of single-threaded software, loops are the most challenging constructs to verify. Read more…

Verifying loops – part 2

March 29, 2010 2 comments

Last time I showed how it was possible to analyse a loop-free and recursion-free program or function to determine its semantics (i.e. its weakest precondition and its postcondition), but that this didn’t work when we have loops. To make it possible to analyze loops thoroughly, Read more…

Verifying loops in C and C++ (intro)

March 22, 2010 1 comment

When it comes to formal verification of single-threaded programs, one of the hardest constructs to verify is the humble loop. If a function contains no loops and no function calls, then a static analyser can trace through the function, looking for constructs (such as indexing an array, or dividing one number by another) that have an implied precondition Read more…

Using and Abusing Unions

March 12, 2010 4 comments

The C union type is one of those features that is generally frowned on by those who set programming standards for critical systems, yet is quite often used. MISRA C 2004 rule 18.4 bans them (“unions shall not be used”) on the grounds that there is a risk that the data may be misinterpreted. However, it goes on to say that deviations are acceptable for packing and unpacking of data, and for implementing variant records provided that the variants are differentiated by a common field. Read more…

Using constrained types in C

February 26, 2010 4 comments

When writing critical software, one of the advantages cited for using Ada rather than C is that Ada lets you define constrained types, like this:

type Percentage is Integer range 0 .. 100;

Read more…

Reasoning about null-terminated strings in C/C++

February 23, 2010 Comments off

In my last post I described how ArC supports reasoning about array access, by allowing you to refer to the bounds of an array in a specification. If the code itself needs to know the size of an array, then the size is provided by other means, for example by passing it as an extra parameter. However, when using arrays of characters, standard practice in C is not to pass the number of elements, but to use a null character to indicate the end. Read more…

The Taming of the Pointer – Part 2

February 22, 2010 6 comments

In last Wednesday’s post I mentioned three ways in which pointers are troublesome in C/C++, and I introduced the null ArC keyword to mitigate one of them. Now I’ll turn to the second issue: the fact that given (say) a variable or parameter of type int*, the type does not allow us to determine whether it refers to a single int, or to an array of ints – nor, if it refers to an array, can we find how many elements the array contains. Read more…