TOC
The following additional types of declaration are available. They may not appear inside functions, and their scope is the file in which they are declared.
In the following, a spec-expression-list is a list of one or more spec-expressions separated by semicolons. A spec-expression is any expression that has no side effects. A spec-expression may refer to ghost declarations.
The first form causes eCv to generate verification conditions that all the expressions in the spec-expression-list are true. Whether proven or not, each expression in the list will be assumed true when attempting to prove that the following expressions are true, and when proving subsequent verification conditions in the same scope.
In the second form, the parameter list must not be empty and all the parameters must be named. The prover generates verification conditions that all the expressions in the spec-expression-list are true for all possible values of the parameters.
You can also use assert as a statement (see below).
Note: if you wish to #include "assert.h" in your source file so that you can do run-time checking of assertions in a debug build, then we suggest you introduce any global assertions with the keyword _ecv_assert instead of assert, otherwise your compiler will report a syntax error. Alternatively, enclose them within #ifdef __ECV__ ... #endif.
The first form causes the prover to assume that each expression in the spec-expression is true, without generating a verification condition. Useful when you want to provide information that eCv has no way of finding out for itself. Here is an example:
struct Foo {
int x;
double y;
}
assume(sizeof(struct Foo) <= 2 * min_sizeof(struct Foo))
Although eCv can calculate a minimum value for the size of a structure, it cannot calculate a maximum value
because the amount of padding inserted by the compiler is unknown. This means that eCv is
normally unable to prove that calculations involving the size of a structure do not overflow. In this example, we use an assume
declaration to put an upper limit on sizeof(struct Foo), thereby avoiding this problem.
The second form causes the prover to assume that each expression in the spec-expression is true, for all possible values of the parameters.
You can also use assume as a statement (see below).
Causes eCv to generate a verification condition that each spec-expression is true at that point, and then to assume it is true when proving subsequent verification conditions.
Note: if you wish to #include "assert.h" in your source file so that you can do run-time checking of assertions in a debug build, then we suggest the following:
The main use of assume is as described above; however assume can also be used within a statement list, in a similar way to assert. When assume is used in this way, each expression in spec-expression-list is assumed true without generating a verification condition.
This is useful when you want to provide information that eCv has no way of finding out for itself.
Used to introduce a statement that is invisible to the compiler, typically for the purpose of changing the value of a ghost variable. A ghost statement may not change the value of any non-ghost variables.
A "do nothing" statement,which can be useful when, for instance, you want to provide an empty loop body.
In specifications and within the declarations of ghost functions, you can use some special
eCv expression types as well as side-effect-free expressions from the
C language. The not-null
expression (which can be used in normal code as well) may be useful, too.
Builds a sequence (i.e. an array) of values comprising cast-expression_1, cast-expression_1+1, cast-expression_1+2 and so on up to cast-expression_2. If cast-expression_1 > cast-expression_2, the sequence is empty. The expressions must both be of integral type (in which case they are promoted to integer, which is the type of unbounded integers), or of type char, or of type wchar_t, or of the same enumeration type.
We suggest using a space before and after the ".." operator to avoid the possibility that the C preprocessor treats the whole construct as a preprocessing number. In particular, if cast-expression_1 is an integer literal, cast-expression_2 starts with a macro name (for example, result), and there are no spaces, then the preprocessor will not recognize the macro.
The => operator means implication, so that a => b means "a implies b". This is equivalent to (!a || b) but is easier to read in some specification contexts, such as preconditions.
The precedence of => is lower than ||, so any && or || operators in the operands are evaluated before the implication is evaluated.
Returns true if and only if the left operand occurs in the right operand. The right operand must be an array, set or bag whose element type is the same as the type of the left operand. Or the right operand can be a map whose domain type is the same as the type of the left operand.
idiv is a version of the integer division operator / that always rounds down (i.e. towards minus infinity).
imod is a version of the integer modulus operator % that always returns a non-negative result.
Both of these have the precondition that the second operand is greater than zero.
_ecv_pow is an operator that raises the left-hand operand to the power of the right-hand operand, equivalent to the ^ operator in Perfect. The types of the operands may be (integer, integer), (real, real) or (real, integer).
This is the compound literal expression from C99. When eCv
is run in C90 or C++ mode, it can be used in specifications and other
ghost contexts. It constructs a value of type from the values in initializer-list.
For example, the expression (int[3]){45, 32, 12} yields an array of three integer values. Don't be
misled by the word "literal", the expressions in initializer-list
do not need to be constant-expressions. You may not declare new structs, unions or enums inside type.
Yields true if the storage associated with each expression in the argument list does not overlap with the storage associated with any other expression in the list. Each expression may be an lvalue or an expression of the form "some(type-name)" (see also writes-clauses in function specifications). To be meaningful, at least one of the expression must be of the form *p where p is a pointer, or a[i] or a.all where a is an array pointer. Used mostly in function preconditions and structure invariants, to state that some parameters or fields of pointer type don't alias the same memory, or don't point into certain static variables, or never point into structures of certain types.
This yields true if expression was last assigned a value through member-name. The type of expression must be a union, and member-name must be one of the members of that union.
Within a postcondition, any mention of a variable or other object normally refers to the value of that variable or object when the function returns. [Exception: any mention of a function parameter in a postcondition always refers to the initial value of that parameter, because changes to the values of parameters are not visible to the caller of the function.] However, it is often useful to refer to initial values in a postcondition as well, so that the postcondition can describe how final values relate to initial values. You can do this by applying the old operator to the expression whose initial value you are interested in.
Here is an example:
static unsigned int count;
void updateCount(unsigned int *p)
writes(count; *p)
pre(p != &count)
pre(count + *p <= maxof(unsigned int))
post(count == old count + old(*p))
post(*p == 0)
{
count += *p;
*p = 0;
}
You can also use the old operator in a loop invariant or loop variant, to refer to the value of an expression just before the loop was entered for the first time.
This allows you to construct an expression by first naming a subexpression and then using that name as many times as you wish, thereby avoiding the need to write out the subexpression in full each time. For example, to compute the fourth power of x in a ghost context we could use:
( let square = x * x; square * square )
The scope of each name is the remainder of the parenthesised expression in which it is declared.
Yields the value of the type when it has default initialization, for example the initial value of a static variable that was declared without an initializer. For integral types this is also the value corresponding to a bit pattern of all zeros. This is not necessarily true for pointer types and floating-point types.
Yields the maximum value of the specified type, which must be an enumeration or unconstrained integral type, or an alias for such a type.
Yields the minimum value of the specified type, which must be an enumeration or unconstrained integral type, or an alias for such a type.
Yields the lower limit of sizeof(type-name). If sizeof(type-name) is known exactly by eCv, then min_sizeof(type-name) is equal to sizeof(type-name). For a structure, min_sizeof(struct S) is the sum of the sizes of all the fields of S, that is, the size that a struct S would be have if there is no padding.
Yields the value of type-name corresponding to zero initialization. Same as default(type-name) for integral and character types; undefined (i.e. platform-dependent) for other types.
Yields true if, for every value of identifier in type, bool-expression is true.
Yields true if, for every value of identifier in the array or collection expression, bool-expression is true.
Yields true if, for some value of identifier in type, bool-expression is true.
Yields true if, for some value of identifier in the array or collection expression, bool-expression is true.
Yields the single element in collection-expression for which bool-expression is true. There must be exactly one such element.
Selects those elements in collection-expression for which bool-expression is true, yielding a new collection containing those elements. If the collection is an array, then the elements in the result appear in the same order as they did in the original.
For example, the following expression:
those x in
arr :- x >= 0yields an array comprising the non-negative elements of arr.
Yields a new collection obtained by mapping the elements of collection-expression using expression. The original collection is unchanged. If the collection is an array, then the elements in the result appear in the same order as the elements they were derived from appeared in the original.
For example, if arr has type int[ ] then the expression:
for x in arr yield x + 1
yields an array of type integer[ ] with
the same number of elements as the original, in which each element is
one greater than the corresponding element in arr.
Yields a new collection obtained by selecting those elements of collection-expression for which bool-expression is true and mapping them using expression. The original collection is unchanged. If the collection is an array, then the elements in the result appear in the same order as the elements they were derived from appeared in the original.
For example, if arr has type int[ ] then the expression:
for those x in arr :- x >= 0 yield x + 1
first selects the non-negative elements of arr and
then adds 1 to them, yielding an array of type integer[ ].
Applies the specified binary operator sequentially over the
elements of the collection, starting from the element at index 0. For
example, the expression + over arr where arr
has type int[ ] yields the
sum of the elements. If the sequence has only one element, then the
result is the value of that element. If the operator is known to eCv
and has a left-identity value declared, then it is permissible for the
sequence to be empty, in which case the value is the left identity.
Otherwise, this construct has the precondition that the sequence is not
empty. Operators + and * over integral types and floating types all
have a left identity element known to eCv.
eCv Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.