18.3 Local and global variables
18.3.1 Global variables
You can declare a new global variable with the following command
Global Variable x : value_type.
where x may be a reference, an array or a function.
Example:
Parameter N : Z.
Global Variable x : Z ref.
Correctness foo { `x < N` } begin x := (Zmult 2 !x) end { `x < 2*N` }.
Each time you complete a correctness proof, the corresponding program is
added to the programs environment. You can list the current programs
environment with the command
Show Programs.
18.3.2 Local variables
Local variables are introduced with the following syntax
let x = ref e1
in e2
where the scope of x is exactly the program e2.
Notice that, as usual in ML, local variables must be
initialized (here with e1).
When specifying a program including local variables, you have to take
care about their scopes. Indeed, the following two programs are not
annotated in the same way:
-
let x = e1 in e2 { Q }
The post-condition Q applies to e2, and therefore x may
appear in Q;
- (let x = e1 in e2) { Q }
The post-condition Q applies to the whole program, and therefore
the local variable x may not appear in Q (it is beyond
its scope).