| blob | d0d8e6495cf3f7346e032c33140296d85aa52c5c |
1 Release Notes
2 =============
4 .. _auto-dereference:
6 Release Notes for Version 1.2: New Syntax for “Auto-dereference”
7 ----------------------------------------------------------------
9 .. index:: auto-dereference
11 Version 1.2 introduces a simplified syntax for reference variables, to
12 avoid the somehow heavy OCaml syntax using bang character. In short, this
13 is syntactic sugar summarized in the following table. An example using
14 this new syntax is in :file:`examples/isqrt.mlw`.
16 +-------------------------+-------------------------------+
17 | auto-dereference syntax | desugared to |
18 +=========================+===============================+
19 | ``let &x = ... in`` | ``let (x: ref ...) = ... in`` |
20 +-------------------------+-------------------------------+
21 | ``f x`` | ``f x.contents`` |
22 +-------------------------+-------------------------------+
23 | ``x <- ...`` | ``x.contents <- ...`` |
24 +-------------------------+-------------------------------+
25 | ``let ref x = ...`` | ``let &x = ref ...`` |
26 +-------------------------+-------------------------------+
28 Notice that
30 - the ``&`` marker adds the typing constraint ``(x: ref ...)``;
31 - top-level ``let/val ref`` and ``let/val &`` are allowed;
32 - auto-dereferencing works in logic, but such variables
33 cannot be introduced inside logical terms.
35 That syntactic sugar is further extended to pattern matching, function
36 parameters, and reference passing, as follows.
38 +----------------------------------+-----------------------------------------------------+
39 | auto-dereference syntax | desugared to |
40 +==================================+=====================================================+
41 | ``match e with (x,&y) -> y end`` | ``match e with (x,(y: ref ...)) -> y.contents end`` |
42 +----------------------------------+-----------------------------------------------------+
43 | .. code-block:: whyml | .. code-block:: whyml |
44 | | |
45 | let incr (&x: ref int) = | let incr (x: ref int) = |
46 | x <- x + 1 | x.contents <- x.contents + 1 |
47 | | |
48 | let f () = | let f () = |
49 | let ref x = 0 in | let x = ref 0 in |
50 | incr x; | incr x; |
51 | x | x.contents |
52 +----------------------------------+-----------------------------------------------------+
53 | ``let incr (ref x: int) ...`` | ``let incr (&x: ref int) ...`` |
54 +----------------------------------+-----------------------------------------------------+
56 The type annotation is not required. Let-functions with such formal
57 parameters also prevent the actual argument from auto-dereferencing when
58 used in logic. Pure logical symbols cannot be declared with such
59 parameters.
61 Auto-dereference suppression does not work in the middle of a relation
62 chain: in ``0 < x :< 17``, ``x`` will be dereferenced even if ``(:<)``
63 expects a ref-parameter on the left.
65 Finally, that syntactic sugar applies to the caller side:
67 +-------------------------+-----------------------+
68 | auto-dereference syntax | desugared to |
69 +=========================+=======================+
70 | .. code-block:: whyml | .. code-block:: whyml |
71 | | |
72 | let f () = | let f () = |
73 | let ref x = 0 in | let x = ref 0 in |
74 | g &x | g x |
75 +-------------------------+-----------------------+
77 The ``&`` marker can only be attached to a variable. Works in logic.
79 Ref-binders and ``&``-binders in variable declarations, patterns, and
80 function parameters do not require importing ``ref.Ref``. Any example
81 that does not use references inside data structures can be rewritten by
82 using ref-binders, without importing ``ref.Ref``.
84 Explicit use of type symbol ``ref``, program function ``ref``, or field
85 ``contents`` require importing ``ref.Ref`` or ``why3.Ref.Ref``.
86 Operations ``(:=)`` and ``(!)`` require importing ``ref.Ref``.
88 Operation ``(:=)`` is fully subsumed by direct assignment ``(<-)``.
90 Release Notes for Version 1.0: Syntax Changes w.r.t. 0.88
91 ---------------------------------------------------------
93 The syntax of WhyML programs changed in release 1.0.
94 The following table summarizes the changes.
96 +---------------------------------------------+---------------------------------------------------------------+
97 | version 0.88 | version 1.0 |
98 +=============================================+===============================================================+
99 | ``function f ...`` | ``let function f ...`` if called in programs |
100 +---------------------------------------------+---------------------------------------------------------------+
101 | ``'L:`` | ``label L in`` |
102 +---------------------------------------------+---------------------------------------------------------------+
103 | ``at x 'L`` | ``x at L`` |
104 +---------------------------------------------+---------------------------------------------------------------+
105 | ``\ x. e`` | ``fun x -> e`` |
106 +---------------------------------------------+---------------------------------------------------------------+
107 | ``use HighOrd`` | not needed anymore |
108 +---------------------------------------------+---------------------------------------------------------------+
109 | ``HighOrd.pred ty`` | ``ty -> bool`` |
110 +---------------------------------------------+---------------------------------------------------------------+
111 | ``type t model ...`` | ``type t = abstract ...`` |
112 +---------------------------------------------+---------------------------------------------------------------+
113 | ``abstract e ensures { Q }`` | ``begin ensures { Q } e end`` |
114 +---------------------------------------------+---------------------------------------------------------------+
115 | ``namespace N`` | ``scope N`` |
116 +---------------------------------------------+---------------------------------------------------------------+
117 | ``use import M`` | ``use M`` |
118 +---------------------------------------------+---------------------------------------------------------------+
119 | ``"attribute"`` | ``[@attribute]`` |
120 +---------------------------------------------+---------------------------------------------------------------+
121 | ``meta M prop P`` | ``meta M lemma P`` or ``meta M axiom P`` or ``meta M goal P`` |
122 +---------------------------------------------+---------------------------------------------------------------+
123 | ``loop ... end`` | ``while true do ... done`` |
124 +---------------------------------------------+---------------------------------------------------------------+
125 | ``type ... invariant { ... self.foo ... }`` | ``type ... invariant { ... foo ... }`` |
126 +---------------------------------------------+---------------------------------------------------------------+
128 Note also that logical symbols can no longer be used in non-ghost code;
129 in particular, there is no polymorphic equality in programs anymore, so
130 equality functions must be declared/defined on a per-type basis (already
131 done for type ``int`` in the standard library). The :file:`CHANGES.md` file
132 describes other potential sources of incompatibility.
134 Here are a few more semantic changes.
136 Proving only partial correctness:
138 In versions 0.xx of Why3, when a program function is recursive but not
139 given a variant, or contains a while loop not given a variant, then it
140 was assumed that the user wants to prove partial correctness only.
141 A warning was issued, recommending to add an extra ``diverges`` clause
142 to that function's contract. It was also possible to disable that
143 warning by adding the label ``"W:diverges:N"`` to the function's name.
144 Version 1.0 of Why3 is more aggressively requiring the user to prove
145 the termination of functions which are not given the ``diverges``
146 clause, and the previous warning is now an error. The possibility of
147 proving only partial correctness is now given on a more fine-grain
148 basis: any expression for which one wants to prove partial correctness
149 only, must by annotated with the attribute :why3:attribute:`[@vc:divergent]`.
151 In other words, if one was using the following structure in Why3 0.xx:
153 ::
155 let f "W:diverges:N" <parameters> <contract> = <body>
157 then in 1.0 it should be written as
159 ::
161 let f <parameters> <contract> = [@vc:divergent] <body>
163 Semantics of the ``any`` construct:
165 The ``any`` construct in Why3 0.xx was introducing an arbitrary value
166 satisfying the associated post-condition. In some sense, this construct
167 was introducing some form of an axiom stating that such a value exists.
168 In Why3 1.0, it is now mandatory to prove the existence of such
169 a value, and a VC is generated for that purpose.
171 To obtain the effect of the former semantics of the ``any`` construct,
172 one should use instead a local ``val`` function. In other words, if one
173 was using the following structure in Why3 0.xx:
175 ::
177 any t ensures { P }
179 then in 1.0 it should be written as
181 ::
183 val x:t ensures { P } in x
185 Release Notes for Version 0.80: Syntax Changes w.r.t. 0.73
186 ----------------------------------------------------------
188 The syntax of WhyML programs changed in release 0.80. The following table
189 summarizes the changes.
191 +---------------------------------+---------------------------------+
192 | version 0.73 | version 0.80 |
193 +=================================+=================================+
194 | ``type t = {| field: int |}`` | ``type t = { field~:~int }`` |
195 +---------------------------------+---------------------------------+
196 | ``{| field = 5 |}`` | ``{ field = 5 }`` |
197 +---------------------------------+---------------------------------+
198 | ``use import module M`` | ``use import M`` |
199 +---------------------------------+---------------------------------+
200 | .. code-block:: whyml | .. code-block:: whyml |
201 | | |
202 | let rec f (x:int) (y:int): t | let rec f (x:int) (y:int): t |
203 | variant { t } with rel = | variant { t with rel } |
204 | { P } | requires { P } |
205 | e | ensures { Q } |
206 | { Q } | raises { Exc1 -> R1 |
207 | | Exc1 -> { R1 } | | Exc2 n -> R2 } |
208 | | Exc2 n -> { R2 } | = e |
209 +---------------------------------+---------------------------------+
210 | .. code-block:: whyml | .. code-block:: whyml |
211 | | |
212 | val f (x:int) (y:int): | val f (x:int) (y:int): t |
213 | { P } | requires { P } |
214 | t | writes { a, b } |
215 | writes a b | ensures { Q } |
216 | { Q } | raises { Exc1 -> R1 |
217 | | Exc1 -> { R1 } | | Exc2 n -> R2 } |
218 | | Exc2 n -> { R2 } | |
219 +---------------------------------+---------------------------------+
220 | ``abstract e { Q }`` | ``abstract e ensures { Q }`` |
221 +---------------------------------+---------------------------------+
223 Summary of Changes w.r.t. Why 2
224 -------------------------------
226 The main new features with respect to Why 2.xx
227 are the following.
229 1. Completely redesigned input syntax for logic declarations
231 - new syntax for terms and formulas
232 - enumerated and algebraic data types, pattern matching
233 - recursive definitions of logic functions and predicates, with
234 termination checking
235 - inductive definitions of predicates
236 - declarations are structured in components called “theories”,
237 which can be reused and instantiated
239 2. More generic handling of goals and lemmas to prove
241 - concept of proof task
242 - generic concept of task transformation
243 - generic approach for communicating with external provers
245 3. Source code organized as a library with a documented API, to
246 allow access to Why3 features programmatically.
248 4. GUI with new features with respect to the former GWhy
250 - session save and restore
251 - prover calls in parallel
252 - splitting, and more generally applying task transformations,
253 on demand
254 - ability to edit proofs for interactive provers (Coq only for
255 the moment) on any subtask
257 5. Extensible architecture via plugins
259 - users can define new transformations
260 - users can add connections to additional provers