David Crocker's Verification Blog

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…