Commit 81a0d5d9 authored by MARCHE Claude's avatar MARCHE Claude

documentation

parent 0ac3a7ec
......@@ -286,3 +286,28 @@ Limitations
~~~~~~~~~~~
Python lists are modeled as arrays, whose size cannot be modified.
.. index:: CFG
.. _format.CFG:
CFG: Control-Flow-Graph style function bodies
---------------------------------------------
CFG is an experimental extension of the regular WhyML language, in
which the body of program functions can optionally be coded using
labelled blocks and `goto` statements. CFG can be used to encoded
algorithms which are presented in an unstructured fashion. It can be
also used as a target for encoding unstructured programming languages
in Why3, for example assembly code.
Syntax of CFG
~~~~~~~~~~~~~
The syntax is an extension of the regular WhyML syntax. The additional rules are as follows
.. productionlist:: CFG
file: `module`*
module: "module" `ident` `decl`* "end"
decl: "let" "cfg" `cfg_fundef` ("with" `cfg_fundef`)*
cfg_fundef: `ident` `binders` : `type` `spec` "=" `vardecl`* `block` `labelblock`*
......@@ -597,6 +597,11 @@ collection. The former can be done simultaneously on a tuple of values:
of the ternary bracket operator ``([]<-)`` and cannot be used in a
multiple assignment.
.. index:: auto-dereference
.. rubric:: Auto-dereference: Simplified Usage of Mutable variables
TODO: put here what is currently in the release notes.
.. index:: evaluation order
.. rubric:: Evaluation order
......
......@@ -26,6 +26,13 @@ where :math:`WP(e,Q)` is a formula computed automatically using rules defined re
TODO: Refer to `A Pragmatic Type System for Deductive Verification <https://hal.archives-ouvertes.fr/hal-01256434v3>`_
Attributes: :why3:attribute:`[@vc:divergent]` disables generation of VC for termination
Other attributes: :why3:attribute:`[@vc:annotation]`, :why3:attribute:`[@vc:sp]`, :why3:attribute:`[@vc:wp]`, :why3:attribute:`[@vc:white_box]`, :why3:attribute:`[@vc:keep_precondition]`
VC generated for type invariants
--------------------------------
......@@ -50,6 +57,7 @@ is to pose this attribute on the whole body of a program function.
Show an example.
.. _sec.runwithinferloop:
Automatic inference of loop invariants
......
......@@ -16,9 +16,6 @@
let floc s e = Loc.extract (s,e)
(*
let mk_cfgexpr d s e = { cfg_expr_desc = d; cfg_expr_loc = floc s e }
*)
let mk_cfginstr d s e = { cfg_instr_desc = d; cfg_instr_loc = floc s e }
%}
......
......@@ -49,9 +49,8 @@ let next_pos =
incr counter;
Loc.user_position "" !counter 0 0
let todo fmt _str =
fprintf fmt "__todo__"
(* fprintf fmt "<NOT IMPLEMENTED: %s>" str *)
let todo fmt str =
fprintf fmt "<Mlw_printer:not implemented> %s" str
let pp_sep f fmt () =
fprintf fmt f
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment