18.2 Syntax of annotated programs

18.2.1 Programs

The syntax of programs is given in figure 18.1. Basically, the programming language is a purely functional kernel with an addition of references and arrays on purely functional values. If you do not consider the logical assertions, the syntax coincide with Objective Caml syntax, except for elements of arrays which are written t[i]. In particular, the dereference of a mutable variable x is written !x and assignment is written := (for instance, the increment of the variable x will be written x := !x + 1). Actually, that syntax does not really matters, since it would be extracted later to real concrete syntax, in different programming languages.

prog ::= {   predicate   } *   statement   [ {   predicate   } ]
     
statement ::= expression
  | identifier   :=   prog
  | identifier   [   expression   ]   :=   prog
  | let   identifier   =   ref   prog   in   prog
  | if   prog   then   prog   [ else   prog ]
  | while   prog   do   loop_annot   block   done
  | begin   block   end
  | let   identifier   =   prog   in   prog
  | fun   binders   ->   prog
  | let   rec   identifier   binder   :   value_type
       {   variant   wf_arg   }   =   prog   [ in   prog ]
  | (   prog    prog   )
     
expression ::= identifier
  | !   identifier
  | identifier   [   expression   ]
  | integer
  | (   expression+ )
     
block ::= block_statement   [   ;   block   ]
     
block_statement ::= prog
  | label   identifier
  | assert   {   predicate   }
     
binders ::= (   identifier,...,identifier   :   value_type   ) +
     
loop_annot ::= {   invariant   predicate   variant   wf_arg   }
     
wf_arg ::= cic_term   [ for   cic_term ]
     
predicate ::= cci_term   [ as   identifier ]

Figure 18.1:
Syntactic sugar.
Restrictions.
You can notice some restrictions with respect to real ML programs:
  1. Binders in functions (recursive or not) are explicitly typed, and the type of the result of a recursive function is also given. This is due to the lack of type inference.

  2. Full expressions are not allowed on left-hand side of assignment, but only variables. Therefore, you can not write 
        (if b then x else y) := 0
    But, in most cases, you can rewrite them into acceptable programs. For instance, the previous program may be rewritten into the following one: 
        if b then x := 0 else y := 0

18.2.2 Typing

The types of annotated programs are split into two kinds: the types of values and the types of computations. Those two types families are recursively mutually defined with the following concrete syntax:
value_type ::= cic_term
  | cic_term   ref
  | array   cic_term   of   cic_term
  | fun   (   x : value_type   )+   computation_type
     
computation_type ::= returns   identifier : value_type
    [reads   identifier,...,identifier]   [writes   identifier,...,identifier]
    [pre   predicate]   [post   predicate]
    end
     
predicate ::= cic_term
     

The typing is mostly the one of ML, without polymorphism. The user should notice that:

18.2.3 Specification

The specification part of programs is made of different kind of annotations, which are terms of sort Prop in the Calculus of Inductive Constructions.

Those annotations can refer to the values of the variables directly by their names. There is no dereference operator ``!'' in annotations. Annotations are read with the Coq parser, so you can use all the Coq syntax to write annotations. For instance, if x and y are references over integers (in type Z), you can write the following annotation
{ `0 < x <= x+y` }
In a post-condition, if necessary, you can refer to the value of the variable x before the evaluation with the notation x@. Actually, it is possible to refer to the value of a variable at any moment of the evaluation with the notation x@l, provided that l is a label previously inserted in your program (see below the paragraph about labels).

You have the possibility to give some names to the annotations, with the syntax
{ annotation as identifier }
and then the annotation will be given this name in the proof obligations. Otherwise, fresh names are given automatically, of the kind Post3, Pre12, Test4, etc. You are encouraged to give explicit names, in order not to have to modify your proof script when your proof obligations change (for instance, if you modify a part of the program).

Pre- and post-conditions

Each program, and each of its sub-programs, may be annotated by a pre-condition and/or a post-condition. The pre-condition is an annotation about the values of variables before the evaluation, and the post-condition is an annotation about the values of variables before and after the evaluation. Example:
{ `0 < x` } x := (Zplus !x !x) { `x@ < x` }
Moreover, you can assert some properties of the result of the evaluation in the post-condition, by referring to it through the name result. Example:
(Zs (Zplus !x !x)) { (Zodd result) }

Loops invariants and variants

Loop invariants and variants are introduced just after the do keyword, with the following syntax:
while   B   do
    {   invariant   I     variant   f   for   R   }
    block
done

The invariant I is an annotation about the values of variables when the loop is entered, since B has no side effects (B is a purely functional expression). Of course, I may refer to values of variables at any moment before the entering of the loop.

The variant f must be given in order to establish the termination of the loop. The relation R must be a term of type A® A®Prop, where f is of type A. When R is not specified, then f is assumed to be of type Z and the usual order relation on natural number is used.

Recursive functions

The termination of a recursive function is justified in the same way as loops, using a variant. This variant is introduced with the following syntax
let   rec   f   (x1:V1)...(xn:Vn) : V   {   variant   f   for   R   } = prog
and is interpreted as for loops. Of course, the variant may refer to the bound variables xi. The specification of a recursive function is the one of its body, prog. Example:
let   rec   fact   (x:Z) : Z   {   variant   x } = {   x³0   }   ...   {   result=x!   }

Assertions inside blocks

Assertions may be inserted inside blocks, with the following syntax
begin   block_statements ...;   assert   {   P   };   block_statements ...   end
The annotation P may refer to the values of variables at any labels known at this moment of evaluation.

Inserting labels in your program

In order to refer to the values of variables at any moment of evaluation of the program, you may put some labels inside your programs. Actually, it is only necessary to insert them inside blocks, since this is the only place where side effects can appear. The syntax to insert a label is the following:
begin   block_statements ...;   label   L;   block_statements ...   end
Then it is possible to refer to the value of the variable x at step L with the notation x@L.

There is a special label 0 which is automatically inserted at the beginning of the program. Therefore, x@0 will always refer to the initial value of the variable x.
Notice that this mechanism allows the user to get rid of the so-called auxiliary variables, which are usually widely used in traditional frameworks to refer to previous values of variables.

Boolean expressions

As explained above, boolean expressions appearing in if and while tests are arbitrary programs of type bool. Actually, there is a little restriction: a test can not do some side effects. Usually, a test if annotated in such a way:
B   { if   result  then   T   else   F }
(The if then else construction in the annotation is the one of Coq !) Here T and F are the two propositions you want to get in the two branches of the test. If you do not annotate a test, then T and F automatically become B=true and B=false, which is the usual annotation in Floyd-Hoare logic.

But you should take advantages of the fact that T and F may be arbitrary propositions, or you can even annotate B with any other kind of proposition (usually depending on result).

As explained in the paragraph about the syntax of boolean expression, some syntactic sugar is provided for usual order relations over type Z. When you write if   x<y   ... in your program, it is only a shortcut for if   (Z_lt_ge_bool x y)   ..., where Z_lt_ge_bool is the proof of " x,y:Z. $ b:bool. (if   b  then   x<y   else   x³ y) i.e. of a program returning a boolean with the expected post-condition. But you can use any other functional expression of such a type. In particular, the Programs standard library comes with a bunch of decidability theorems on type nat:
zerop_bool : " n:nat.$ b:bool. if   b  then   n=0   else   0<n
nat_eq_bool : " n,m:nat.$ b:bool. if   b  then   n=m   else   n¹m
le_lt_bool : " n,m:nat.$ b:bool. if   b  then   n£ m   else   m<n
lt_le_bool : " n,m:nat.$ b:bool. if   b  then   n<m   else   m£ n
which you can combine with the logical connectives.

It is often the case that you have a decidability theorem over some type, as for instance a theorem of decidability of equality over some type S:
S_dec : (x,y:S){x=y}+{¬ x=y}
Then you can build a test function corresponding to S_dec using the operator bool_of_sumbool provided with the Prorgams module, in such a way:
Definition   S_bool   := [x,y:S](bool_of_sumbool   ?   ?   (S_dec   x   y))
Then you can use the test function S_bool in your programs, and you will get the hypothesis x=y and ¬ x=y in the corresponding branches. Of course, you can do the same for any function returning some result in the constructive sum {A}+{B}.