Invariants can also be specified on compound data types (C structs and unions). In VCC, instances of such compound types are called objects; each object has a Boolean ghost field \closed that indicates that it is in a "valid" state; the invariants on a type are expected to hold for an instance of the type whenever the instance is closed.

For example, here is a simple example of a data structure that maintains a small set of ints as a sorted array (without duplicates):

#include <vcc.h>

#define SIZE 10

typedef struct Set {
  unsigned int len;
  int data[SIZE];
  
  _(invariant len < SIZE)
  _(invariant \forall unsigned int i, j; i < j && j < len ==> data[i] < data[j])
} Set;

Last edited Jan 19, 2012 at 2:15 PM by MarkHillebrand, version 7

Comments

No comments yet.