eCv specifications

General Notes

All expressions within eCv specification constructs must have NO have side effects. So the following are not permitted in specifications:

• assignment expressions
• operators ++ and -- (both prefix and postfix)
• assigning operators (e.g. +=)
• calls to functions that have side-effects, i.e. functions with explicit or implicit non-empty writes-clauses
• reading or writing volatile variables

Where a specification macro takes an expression list, the expressions must be separated by a semicolon, not by a comma. This is because macros in C90 and C++ must have a fixed number of arguments.

pre(n >= 0; n <= 10)       /* correct */
pre(n >= 0) pre (n <= 10)  /* correct */
pre(n >= 0, n <= 10)       /* incorrect */


Within specifications, you may use ghost functions and ghost members. For example, if myArray is a parameter of array type, then myArray.lwb gives the lowest valid index (usually 0), and myArray.upb gives the highest valid index (usually one less than the number of elements in the array).

Similarly, if s is a parameter of type char * array, then isNullTerminated(s) expresses the condition that there is a valid non-negative index into s such that the corresponding element of s is the null character. See the list of ghost members and predefined ghost functions later in this document.

Type constraints

You can declare a constrained type by using an invariant clause within a typedef declaration. Here is an example:

typedef int invariant(value in 0..100) percent;

The argument of invariant is an expression that constrains on the values of this type, using the keyword value to refer to any such value. The constraint may refer to constants but not to variables.

The semantics of constrained types are as follows, in which the term underlying type refers to the type that precedes the invariant clause:

• A value of a constrained type can be converted implicitly to the underlying type. In particular, this conversion occurs whenever a value of a constrained type is subject to the "usual arithmetic conversions".
• A value of the underlying type can be converted implicitly to the constrained type. However, eCv generates a verification condition to ensure that the value is permitted by the constraint.
• If a static variable or a field or element of a static variable has a constrained type, it must either have an initializer or the constraint must allow the default static-initialized value of the underlying type.
• A pointer to a constrained type may not be cast to or from any other type, other than another type that is a synonym for it. In the above example, a percent* may not be cast to or from a int*. However, if we also declare:
  
  typedef percent percent2;
  
  then percent2 is a synonym for percent and we may convert between percent* and percent2* in either direction, explicitly or implicitly. If instead we declare:
  
  typedef int invariant(value in 0..100) percent2;
  
  then percent2 and percent are treated as different types, and there is no conversion from percent* to percent2* or vice versa. Likewise if we declare:
  
  typedef percent invariant true percent3;
  
  then percent3 is not a synonym for percent and there is no conversion between percent* and percent3*.

Function contracts

Function contracts are placed after the function parameter list, but before the opening brace "{" of the body if it is a function definition, or before the terminating semicolon if it is a function prototype.

You may declare any or all of writes-clauses, preconditions, recursion variants, returns-expressions and postconditions, but they must be declared in that order. The syntax of these is:

• writes(writes-expression-list)
• pre(expression-list)
• decrease(expression-list)
• returns(expression)
• post(expression-list)

You may declare more than one writes-clause, precondition, postcondition or variant, which is equivalent to declaring a single, longer list. For example:

pre(n >= 0)
pre(n <= 10)

pre(n >= 0; n <= 10)

Keep the arguments of each instance of a specification on a single line as far as possible, to avoid getting misleading line numbers in error and warning messages.

writes(writes-expression-list)

The writes-clause specifies what nonlocal variables the function writes. A writes-clause may contain the following elements, separated by semicolon:

• Normal lvalue expressions of non-volatile types, indicating that those expressions may be written to.
• Expressions of the form some(type-name), indicating that any nonlocal values of the designated type may be written. This form should only be used when the expressions that are written cannot be individually enumerated. For example, a function that iterates through a list updating every node in the list would specify writes(some(node_t)) where node_t is the type of the list node. [Note: the semantics of some are not fully implemented in the initial release of eCv, therefore programs using some may not be completely verifiable.]
• The special form volatile, indicating that the function writes and/or reads unspecified volatile variables. It is not necessary to list the variables individually.

If you don't provide a writes-clause, then a default one is constructed. The default will be such that for any parameter declaration of the form T *p or T * array p where T is not qualified by const or volatile, the function is assumed to write to *p. If your function writes to any other nonlocal variables (for example, static variables), then you must declare all the nonlocal variables it writes to in a writes-clause.

If you have a function with a parameter of the form T *p that doesn't write to *p, then if the function is under your control, we recommend you add the const qualifier. If this is not possible (for example, it is a third-party library function that you cannot change), use an explicit writes-clause to prevent eCv from assuming that the function writes to *p. You can use the form writes() to indicate that a function writes no nonlocal variables at all.

pre(expression-list)

Preconditions describe the constraints that the caller must satisfy when calling the function. eCv requires that all function preconditions be declared explicitly.

decrease(expression-list)

Recursion variants are only used in recursive function specifications, and allow eCv to prove that the recursion terminates. See Perfect Developer Language Reference Manual for details. Note that a function may have a recursive specification even if its implementation is not recursive.

returns(expression)

Returns-specifications describe the value that a function returns. They are not allowed when the function return type is void). The specification returns(e) is equivalent to post(result == e) with the important exception that the expression inside returns(...) is permitted to make recursive calls to the function being specified, whereas expressions inside post(...) are not. This allows you to write a recursive specification for the return value of a function, even when the return value is computed by iteration instead of recursion.

post(expression-list)

Postconditions describe conditions that the function guarantees hold when it returns. In postconditions, you may use the keyword result to refer to the value returned by the function. A non-void function may have both a returns-specification and a postcondition - for example, the postcondition might assert additional properties of the function result and/or describe side-effects of the function.

Where to put function contracts

If a function has extern linkage (i.e. it is not declared static), then you will normally define the function in a .c file and provide a prototype for it in a .h file. You should do the following:

• Declare the writes-clause (if applicable) and any preconditions and postconditions for the function in the prototype. This means that when you verify another .c file that #includes the file containing the prototype, the specifications are available.
• #include the .h file in the .c file (this is normal practice anyway, so that the prototype gets checked against the definition). If you don't do this, then the preconditions and postconditions will not be available when the function itself is verified.
• If the specification is recursive (i.e. the returns-specification calls the function recursively), you must declare a variant in the prototype. If only the function body is recursive, you may declare a variant in either the prototype or the definition, but not in both.

eCv will give an error message if, when processing a .c file and all the other files that it #includes, it finds a function definition with specifications and there is a prototype for that function in a different file.

If you need to provide specifications for functions declared in a third-party header file, but you do not wish to add specifications or the array or null keywords to that header file, you can declare prototypes for the same functions with added specifications, array and null keywords in your own header file. Each such function declaration should be prefixed with the spec keyword to tell eCv that this overrides the other one. eCv will nevertheless check that each pair of declarations is compatible, ignoring the missing array and null keywords in the third-party file.

eCv provides a number of header files corresponding to the standard C header files for this purpose. For example, file ecv_string.h provides specifications for functions in the standard header file string.h. So if your program includes string.h, you must also include ecv_string.h. Note that including ecv_string.h alone is not sufficient to make the declarations in string.h available. This is to ensure that your compiler sees its own versions of the declarations. You do not need to make the inclusion of ecv_string.h and similar files conditional on #ifdef __ECV__ because this is already done inside the file.

If a function is local to a single file (i.e. static linkage), then you must declare the specifications in the prototype, if it has one. If the function has no prototype, then declare the specifications in the function definition.

Specifications for C++ class member functions whose implementation is defined outside the class declaration must be attached to the declaration of the member function declaration within the class declaration.

Loop specifications

Loop specifications must be placed between the loop header and the loop body, like this:

for (...)
loop-specifications
{
    statements
}

while (...)
loop-specifications
{
    statements
}

do
loop-specifications
{
    statements
} while (...)


You may declare any or all of writes-clauses, loop invariants, and loop variants, but they must be declared in that order. The syntax of these is:

• writes(writes-expression-list)
• keep(expression-list)
• decrease(expression-list)

You may declare more than one writes-clause, loop invariant, or loop variant, which is equivalent to declaring a single, longer list. For example:

keep(n >= 0)
keep(n <= 10)

keep(n >= 0; n <= 10)

Keep the arguments of each instance of a specification keyword on a single line as far as possible, to avoid getting misleading line numbers in error and warning messages.

Loop writes clause

eCv needs to know what variables a loop modifies. If a loop modifies only the local variables of the function it occurs in, and modifies them directly rather than via a pointer, then eCv can generally work this out for itself. However, if a loop modifies anything else, or anything via a pointer or array pointer, then a writes-clause for the loop must be given explicitly. For example, consider the following:

void setArray(int * array a, size_t size, int k)
{ size_t i;
  for (i = 0; i != size; ++i) {
    a[i] = k;
  }
}

The loop modifies elements of the array a which is not a local variable, therefore a writes-clause is needed. The loop modifies all elements of the array, therefore the appropriate expression is a.all:

void setArray(int * array a, size_t size, int k)
{ size_t i;
  for (i = 0; i != size; ++i)
  writes(a.all)
  {
    a[i] = k;
  }
}


Note: if a loop modifies any elements of a local array, and no writes-clause is given, then it will be assumed that the loop modifies all elements of the array. You can use a loop invariant to describe elements of the array that do not change.

Loop invariant

eCv requires you to write a loop invariant for every loop. A loop invariant is a Boolean expression that depends on all the variables modified by the loop, and is true when the loop is first entered, at the start and end of each iteration of the loop, and when the loop terminates. Typically, it comprises two parts.

The most important part of the loop invariant is a generalization of the state that the loop is intended to achieve. It needs to be written so that it is easy to establish this part of the invariant before the loop starts, by suitable initialization of variables; yet it becomes exactly the desired state when the loop terminates. We’ll refer to the desired state when the loop terminates as the loop postcondition.

For example, suppose we have an array a of integers, and we want to set every element in that array to k. Here’s a function to do that:

void setArray(int * array a, size_t size, int k)
pre(a.lwb == 0)
pre(a.lim == size)
post(forall j in 0..(size - 1):- a[j] == k)
{ size_t i;
  for (i = 0; i != size; ++i)
  writes(a.all)
  {
    a[i] = k;
  }
}

The first precondition says that a is a regular pointer to the start of an array. The second one says that the number of elements is given by size.

The postcondition says that when the function returns, for all indices j in the range 0 to (size – 1), a[j] is equal to k.

In this case, the loop comprises the entire body of the function, so the loop postcondition is the same as the function postcondition. In fact, loop postconditions are very frequently forall expressions, especially for loops that iterate over an array.

We need to generalize the forall expression in the postcondition here so that it is true at the start of every iteration of the loop. The state when we are about to commence the i^th iteration will be that we’ve already set all elements from zero to i-1 (inclusive) to k, but not the elements from i onwards. We can express this with a slight modification to the forall expression, like this:

forall j in 0..(i - 1) :- a[j] == k)


The upper bound of the forall has been changed from (size – 1) in the postcondition to (i – 1) here. This gives us exactly what we need for the loop invariant:

• The loop initialization sets i to zero, so the initial bounds of the forall are 0 .. -1 (that is, from zero up to minus one). This is an empty range (because -1 is less than 0), and a forall over an empty range is true. So the loop invariant is established at the start of the first iteration.
• During each iteration, we set the ith element to k and we increment i. So the invariant is preserved. For example, after the first iteration, the forall has range 0..0 so it just tells us that a[0] == k, which is exactly right. After the second iteration, the range is 0..1 so it says that a[0] and a[1] have value k, which again is exactly right.
• The loop terminates when i == size, because we wrote the while-condition as i != size. If we replace i by size in the invariant, we get exactly the desired postcondition.

eCv expects the loop invariant to be written between the loop header and the body, like this:

void setArray(int * array a, size_t size, int k)
pre(a.lwb == 0)
pre(a.lim == size)
post(forall j in 0..(i - 1) :- a[j] == k)
{ size_t i;
  for (i = 0; i != size; ++i)
  writes(a.all)
  keep(forall j in 0..(i - 1) :- a[j] == k)
  { a[i] = k;
  }
}


eCv uses the keyword keep to introduce the invariant, because we’re keeping the invariant true.

Unfortunately, this is not yet enough to allow eCv to verify the loop. Using the above, eCv reports that it is unable to prove that a[j] is in-bounds in the loop invariant, or that a[i] is in-bounds in the loop body.

So, we need another component of the loop invariant, to ensure that these accesses are always in bounds. To make sure that a[i] is in bounds, we need to constrain i to be in the range 0..(size - 1) at that point. But we can’t constrain i to this range in the invariant, since when the loop terminates, i ends up with the value size, which is just outside this range. Instead, we constrain i to the range 0..size. The body is not executed when i == size, so that constraint is sufficient to guarantee that a[i] is in bounds in the body. The code then looks like this:

void setArray(int * array a, size_t size, int k)
pre(a.lwb == 0)
pre(a.lim == size)
post(forall j in 0..(i - 1) :- a[j] == k)
{ size_t i;
  for (i = 0; i != size; ++i)
  writes(a.all)
  keep(i in 0..size)
  keep(forall j in 0..(i - 1) :- a[j] == k)
  { a[i] = k;
  }
}

Previously, eCv reported that it was unable to prove that a[j] was in bounds in the original keep clause. Putting the new keep clause before the original one allows eCv to assume that i is in 0..size in the second keep clause. That is enough for it to prove that a[j] is in bounds, because j takes values from 0 to i – 1.

With the above loop specifications, eCv is able to prove that this function meets its specification, if the loop terminates. To prove that it terminates, we’ll need to provide a loop variant.

Note: if the while-part of a for-loop or while-loop has side effects, then the loop invariant refers to the state before those side-effects take place.

Proving loop termination

The easiest way to prove that a loop that is designed to terminate actually does terminate is to use a loop variant. A loop variant in its simplest form is a single expression that depends on variables changed by the loop. It has the following properties:

• Its type has a defined lower bound, a finite number of values, and a total ordering on those values;
• Its value decreases on every iteration of the loop.

If we can define such a variant, then we know that the loop terminates, because from any starting value the lower bound must be reached after a finite number of iterations – after which it can’t decrease any more.

To ensure that the first of these properties is met, eCv only allows loop variant expressions to have integer, Boolean, or enumeration type. For integer variants, eCv assumes a lower bound of zero and will need to prove that such a variant is never negative. For Boolean expressions, the lower bound is false, and true is taken to be greater than false. For expressions of an enumeration type, the lower bound is the lowest enumeration constant defined for that type.

In order to show that our example loop terminates, we need to add a loop variant in the form of a decrease clause. In this case, it is simple to insert a loop variant based on the loop counter:

void setArray(int * array a, size_t size, int k)
pre(a.lwb == 0)
pre(a.lim == size)
post(forall j in 0..(i - 1) :- a[j] == k)
{ size_t i;
  for (i = 0; i != size; ++i)
  writes(a.all)
  keep(i in 0..size)
  keep(forall j in 0..(i - 1) :- a[j] == k)
  decrease(size - i)
  { a[i] = k;
  }
}


The expression size – i meets the needs of a loop variant in eCv because:

• It has one of the allowed types (i.e. integer);
• It is always >= 0 inside the loop body (actually, it is >= 0 immedately after the loop terminates too, although eCv doesn’t require that);
• It decreases on every iteration (because i increases while size remains constant).

eCv will try to prove that size – i is never negative, and that size – i decreases from one iteration to the next. The first of these is easily proven from the invariant i in 0..size. The second is easily proved because the loop increments i at the end of each iteration but leaves size alone.

For a for-loop whose header increments a loop counter from a starting value to a final value, we can always use a loop variant of the form final_value – loop_counter, provided the loop body doesn’t change loop_counter or final_value.

For some loops, each iteration may make progress towards termination in one of several ways. For example, you could write a single loop that iterates over the elements of a two-dimensional array. Each iteration might move on to the next element in the current row, or advance to the next row if it has finished with the current one. In cases like this, defining a single variant expression for the loop can be awkward. So eCv allows you to provide a list of variant expressions. Each iteration of the loop must decrease at least one of its elements in the list, and may not increase an element unless an element earlier in the list decreases. So it must either decrease the first element, or keep the first element the same and decrease the second element, or keep the first two elements the same and decrease the third; and so on.

Note: if the while-part of a for-loop or while-loop has side effects, then the loop variant is computed after those side-effects take place.

Ghost declarations

Sometimes it is easier to write a specification if you declare additional constants, variables and function prototypes (with associated contracts) that are referred to only in specifications. Such a declaration is called a ghost declaration. To tell eCv that a declaration is ghost, and to avoid your compiler generating code for ghost declarations, such a declaration is enclosed in the ghost(...) macro. Here are some example ghost declarations:

ghost(
  int max3(int a, int b, int c)
  post(result >= a && result >= b && result >= c && (result == a || result == b || result == c));
)

ghost(const int maxReading = 1000;)

There are some special rules for ghost declarations, as follows:

• A ghost function declaration may not have a body. It must be a prototype, and to be useful it must have a contract specification.
• Ghost declarations may use the predefined ghost type integer, which is an integral type with no bounds; and the predefined ghost collection types _ecv_set<T>, _ecv_bag<T> and _ecv_map<T1, T2> (see the Library Reference section of the Perfect Developer Language Reference Manual for details of these collection types)
• Ghost functions may have array return types, for example int[ ]

You may refer to ghost declarations in specification contexts and in other ghost declarations, but not in code. The final semicolon at the end of the ghost declaration (before the closing parenthesis that completes the ghost macro invocation) is optional.

Sometimes, for specification purposes it is useful to pass additional ghost parameters to non-ghost functions or constructors. This can be done by declaring a ghost parameter list immediately after the main parameter list, like this:

When such a function is called, actual ghost parameters must be provided using a similar syntax:

   TOC

eCv Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.