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