doc/vcgen.rst

   1 .. _chap.vcgen:
   2
   3 The VC Generators
   4 =================
   5
   6 This chapter gives information about the various processes that generate
   7 the so-called verification conditions, VC for short, from WhyML code.
   8
   9
  10 VC generation for program functions
  11 -----------------------------------
  12
  13 For each program function of the form
  14
  15 .. parsed-literal::
  16
  17    let *f* (*x*:sub:`1`: *t*:sub:`1`) ... (*x*:sub:`n`: *t*:sub:`n`): *t*
  18      requires { *Pre* }
  19      ensures  { *Post* }
  20    = *body*
  21
  22 a new logic goal called ``f'VC`` is generated. Its shape is
  23
  24 .. math::
  25
  26    \forall x_1,\dots,x_n,\quad \mathit{Pre} \Rightarrow \mathit{WP}(\mathit{body},\mathit{Post})
  27
  28 where :math:`\mathit{WP}(e,Q)` is a formula computed automatically using
  29 rules defined recursively on :math:`e`.
  30
  31 TODO: Refer to `A Pragmatic Type System for Deductive Verification <https://hal.archives-ouvertes.fr/hal-01256434v3>`_
  32
  33
  34 Attributes: :why3:attribute:`[@vc:divergent]` disables generation of VC for termination
  35
  36 Other attributes: :why3:attribute:`[@vc:annotation]`, :why3:attribute:`[@vc:sp]`, :why3:attribute:`[@vc:wp]`, :why3:attribute:`[@vc:white_box]`, :why3:attribute:`[@vc:keep_precondition]`
  37
  38
  39
  40 VC generated for type invariants
  41 --------------------------------
  42
  43 How a VC is generated for proving that a type with invariant is
  44 inhabited. Explain also the use of the `by` keyword in this context.
  45
  46 VC generation and lemma functions
  47 ---------------------------------
  48
  49 How a VC for a program function marked as `lemma` is turned into an
  50 hypothesis for the remaining of the module.
  51
  52 Using strongest post-conditions
  53 -------------------------------
  54
  55 To avoid exponential explosion of WP computation, Why3 provides a
  56 mechanism similar to (TODO: cite papers here).
  57
  58 This can be activited locally on any program expression, by putting
  59 the :why3:attribute:`[@vc:sp]` attribute on that expression. Yet, the simplest usage
  60 is to pose this attribute on the whole body of a program function.
  61
  62 Show an example.
  63
  64
  65 .. _sec.runwithinferloop:
  66
  67 Automatic inference of loop invariants
  68 --------------------------------------
  69
  70 Why3 can be executed with support for inferring loop invariants
  71 :cite:`baudin17` (see :numref:`sec.installinferloop` for information
  72 about the compilation of Why3 with support for `infer-loop`).
  73
  74 There are two ways of enabling the inference of loop invariants: by
  75 passing the debug flag :why3:debug:`infer-loop` to Why3 or by annotating ``let``
  76 declarations with the :why3:attribute:`[@infer]` attribute.
  77
  78 Below is an example on how to invoke Why3 such that invariants are
  79 inferred for all the loops in the given file.
  80
  81 ::
  82
  83    why3 ide tests/infer/incr.mlw --debug=infer-loop
  84
  85 In this case, the *Polyhedra* default domain will be used together
  86 with the default widening value of *3*. Why3 GUI will not display the
  87 inferred invariants in the source code, but the VCs corresponding to
  88 those invariants will be displayed and labeled with the ``infer-loop``
  89 keyword as shown in :numref:`fig.gui.infer`.
  90
  91 .. _fig.gui.infer:
  92
  93 .. figure:: images/gui-infer.png
  94    :alt: The GUI with inferred invariants (after split).
  95
  96    The GUI with inferred invariants (after split).
  97
  98 Alternatively, attributes can be used in ``let`` declarations so that
  99 invariants are inferred for all the loops in that declaration. In this
 100 case, it is possible to select the desired domain and widening
 101 value. In the example below, invariants will be inferred using the
 102 *Polyhedra* domain and a widening value of *4*. These two arguments of
 103 the attribute can swapped, for instance, ``[@infer:Polyhedra:4]`` will
 104 produce exactly the same invariants.
 105
 106 .. code-block:: whyml
 107
 108   module Incr
 109
 110     use int.Int
 111     use int.MinMax
 112     use ref.Ref
 113     use ref.Refint
 114
 115     let incr[@infer:4:Polyhedra](x:int) : int
 116       ensures { result = max x 0 }
 117     = let i = ref 0 in
 118       while !i < x do
 119         variant { x - !i }
 120         incr i;
 121       done;
 122       !i
 123   end
 124
 125
 126 There are a few debugging flags that can be passed to Why3 to output
 127 additional information about the inference of loop invariants. Flag
 128 :why3:debug:`infer-print-cfg` will print the Control Flow Graph (CFG) used for
 129 abstract interpretation in a file with the name :file:`inferdbg.dot`;
 130 :why3:debug:`infer-print-ai-result` will print to the standard output the
 131 computed abstract values at each point of the CFG;
 132 :why3:debug:`print-inferred-invs` will print the inferred invariants to the
 133 standard output (note that the displayed identifiers names might not
 134 be consistent with those in the initial program); finally,
 135 :why3:debug:`print-domains-loop` will print for each loop the
 136 loop expression, the domain at that point, and its translation into a
 137 Why3 term.
 138
 139 Current limitations
 140 """""""""""""""""""
 141
 142 1. Loop invariants can only be inferred for loops inside
 143    (non-recursive) ``let`` declarations.