Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / doc / lustre_spec.org @ 1b683c9a

History | View | Annotate | Download (12 KB)

1 7bd3416a ploc
Lustre annotation/specification language
2 a2d97a3e ploc
#+AUTHORS: Pierre-Loic Garoche, Rémi Delmas, Temesghen Kahsai
3 7bd3416a ploc
#+LATEX_HEADER: \usepackage{tikz,listings,stmaryrd,pgfplots,mathrsfs,syntax}
4
#+LATEX_HEADER: \input{lustre_lst}
5
6
This document intends to define the bases of a specification language for
7
Lustre. Such specifications' role are threefold:
8
1. Precise the required behavior of a Lustre model, ie. the behavior of Lustre
9
   nodes. Those specifications could then ease the application of tools.
10
2. Enrich the Lustre code itself with non functionnal annotations; for example
11
   parametrization of tools to be applied on the Lustre model, or for
12
   documentation purpose.
13
3. Enable the compilation of the annotation/specification as C code ACSL
14
   annotations.
15
16
* Syntax
17
18
** Comments
19
All specifications and annotations are expressed within lustre comments starting
20
with the character "@".
21
22
#+begin_latex
23
\begin{lstlisting}[language=lustre]
24
--@ line comment
25
(*@ multi line 
26
    block comment
27
*)
28
\end{lstlisting}
29
#+end_latex
30
31
** Extended lustre/arithmethic expressions
32
33
We introduce here an extended flavour of lustre expressions: lustre expressions extended with quantification over basic datatypes and
34
  string constants.
35
36
These expressions will be used to express preconditions and
37
postconditions over nodes input and output flows. Those conditions have to apply
38
on any non nil value of the flow ie. when the flow is defined.
39
40
The figure\ref{fig:expr} gives a BNF for such extended expressions 
41
42
#+begin_latex
43
\begin{figure}
44
\begin{grammar}
45
<expression> ::= <constant> 
46
\alt <ident>
47
\alt <int> | <float> | <bool> | <string>
48
\alt <unop> <expression>
49
\alt if <expression> then <expression> else <expression>
50
\alt <expression> <binop> <expression>
51
\alt '(' <expression> ( ',' <expression> )*')'
52
\alt <ident> '(' <expression> ( ',' <expression> )* ')'
53
\alt <quantifier> <var decl> ';' <expression> 
54
55
<int> ::= ['0'-'9']+
56
57
<float> ::= ['0'-'9']+'.'['0'-'9']+
58
59
<bool> ::= 'true' | 'false'
60
61
<string> ::= '\"' .* '\"' 
62
63
<unop> ::= '-' | 'pre' | 'current' | 'not'
64
65
<binop> ::= <temporal ops> | <logical ops> | <arithm ops>
66
67
<temporal ops> ::= '->' | 'when' 
68
69
<logical ops> ::= 'xor' | '=>' | 'or' | 'and' | '=' | '\textless\textgreater' | '\textless' | '\textless =' | '\textgreater' | '\textgreater =' 
70
71
<arithm ops> ::= '*' | '/' | 'mod' | 'div' | '+' | '-'
72
73
<quantifier> ::= 'forall' | 'exists'
74
75
<var decl> ::= 'const'? <ident> (',' <ident>)* ':' <type> ( ';' 'const'? <ident> ':' <type> )*
76
77
<type> ::= 'int' | 'bool' | 'float'
78
\end{grammar}
79
\caption{Definition of extended lustre expressions}
80
\label{fig:expr}
81
\end{figure}
82
#+end_latex
83
84
*** String constants
85
86
String constants are part of the language. A valid expression could then be the
87
tuple
88
89
#+begin_latex
90
\begin{lstlisting}[language=lustre]
91
"blue", if x then y + 1 else node1 (x, y, z), 3.2 + z
92
\end{lstlisting}
93
#+end_latex
94
95
Those new string constants will be used to define parameters within annotations.
96
97
*** Quantifications
98
99
Lustre expression are lift to first order. The syntax to declare quantified
100
variables follow the variable declaration in node inputs and outputs:
101
102
#+begin_latex
103
\begin{lstlisting}[language=lustre]
104
ident: type
105
\end{lstlisting}
106
#+end_latex
107
108
The keywork const express the additional constraint: 
109
#+begin_latex
110
\begin{lstlisting}[language=lustre]
111
ident = pre ident
112
\end{lstlisting}
113
#+end_latex
114
115
Quantified variables denote typed flows.
116
117
118
** Annotation identifiers
119
120
Annotation identifiers are usual alphanumeric identifiers extended with '.'.
121
122
** Key paths in annotation bindings
123
124
Keys in annotation declaration are either simple identifier or sequence of them
125
separated by "/":
126
127
/key/(key/)+ or key
128
129
* Node specification
130
131
Node specification are inspired from ACSL function contracts. A node will be
132
associated to a set of requirements and expected properties on the resulting
133
flows. 
134
135
Scope: inputs, outputs
136
137
** Basic contracts
138
Requirements are expressed on input flows using the keyword /requires/
139
while expected behavior can either be defined
140
- with a first order boolean expression over the input flows and the output flows using the
141
  keyword /ensures/ or
142
- with a synchronous observer specified in a separate lustre node, using the
143
  keyword /observer/.
144
145
Synchronous observers allow more complex behavior specification since they
146
usually encode a safety property (or bounded liveness) composed with the system
147
state machine. For example, the use of observers allow to declare new variables
148
to express the property.
149
150
** Synchronous observers
151
152
The node associated to the keywork /observer/ should only produce boolean
153
output flows. The specification /oberver observer\_node(...)/ should be
154
interpreted as
155
\(
156
\bigwedge_{1 \leq i \leq n} o_i
157
\)
158
where /observer\_node/ is defined as 
159
\[
160
observer\_node (...) \ returns\ (o_1, .., o_n); 
161
\]
162
163
** Multiple definitions
164
Multiple definitions of /requires/ or /ensures/ / /observer/ are interpreted as
165
syntactic sugar for conjunctions.
166
Eg, the following function specification 
167
#+begin_latex
168
\begin{lstlisting}[language=lustre]
169
--@ requires e1(...);
170
--@ requires e2(...);
171
--@ ensures e3(...);
172
--@ ensures e4(...);
173
node node1 (...) returns (...);
174
\end{lstlisting}
175
#+end_latex
176
 is equivalent to
177
#+begin_latex
178
\begin{lstlisting}[language=lustre]
179
--@ requires e1(...) and e2(...);
180
--@ ensures e3(...) and e4(...);
181
node node1 (...) returns (...);
182
\end{lstlisting}
183
#+end_latex
184
185
** Clocks
186
 Those pre- and post-conditions are only defined for the node
187
clock.  Those conditions have to apply on any non nil value of the flow ie. when
188
the flow is defined.
189
190
TODO: give an example using when/current
191
192
** Extension: Behaviors
193
194
Similarly to ACSL function contracts, the node specifications could be defined
195
with sub behaviors. 
196
197
TODO: expliquer context du assumes
198
199
TODO: concrete example with forall
200
 
201
#+begin_latex
202
\begin{figure}
203
\begin{lstlisting}[language=lustre]
204
--@ requires lustre_expression(i1, ..., in);
205
--@ ensures lustre_expression(i1, ..., in,o1, .., om);
206
--@ behavior b_name1:
207
--@   assumes lustre_expression(i1, ..., in);
208
--@   ensures lustre_expression(i1, ..., in,o1, .., om);
209
--@ behavior b_name2:
210
--@   assumes lustre_expression(i1, ..., in);
211
--@   ensures lustre_expression(i1, ..., in,o1, .., om);
212
node lustre_node_name (i1: t_i1, ..., in: tn) 
213
     returns (o1: t1, ..., om: t_o m));
214
let
215
...
216
tel
217
218
--@ requires lustre_expression(i1, ..., in);
219
--@ observer lustre_node(i1, ..., in, o1, .., om);
220
--@ behavior b_name1:
221
--@   assumes lustre_expression(i1, ..., in);
222
--@   observer lustre_node(i1, ..., in,o1, .., om);
223
--@ behavior b_name2:
224
--@   assumes lustre_expression(i1, ..., in);
225
--@   observer lustre_node(i1, ..., in,o1, .., om);
226
node lustre_node_name (i1: t_i1, ..., in: tn) 
227
     returns (o1: t1, ..., om: t_o m));
228
let
229
...
230
tel
231
\end{lstlisting}
232
\end{figure}
233
#+end_latex
234
235
** Grammar
236
237
TODO
238
239
* Local node annotations
240
241
Annotations could denote functionnal properties such as invariants or non
242
functional ones, eg. heuristics, tool specific parameters ...
243
244
Scope: inputs, outputs, local variables, locally defined variables, internal
245
flows.
246
247
** Assigning names to subexpression
248
249
Annotations could be used within expression to allocate a new
250
identifier to a sub-expression using the keyword /id/.
251
252
For example, in the equation defining $z$:
253
254
#+begin_latex
255
\begin{lstlisting}[language=lustre]
256
z = pre y and b and ((*@ id -> subexpr1 *)c or x >= y)
257
\end{lstlisting}
258
#+end_latex
259
260
This new identifier /subexpr1/ will be associated to the data flow expression (c
261
or x >= y) and could be used within other annotations.
262
263
One can also use single annotations
264
#+begin_latex
265
\begin{lstlisting}[language=lustre]
266
z = pre y and b and ( --@ id -> subexpr1
267
      c or x >= y)
268
\end{lstlisting}
269
#+end_latex
270
271
** Assigning identifiers to node instances
272
273
A node /foo/ can be used multiple times in a given node. It can appear in
274
different equations:
275
#+begin_latex
276
\begin{lstlisting}[language=lustre]
277
x = foo(...);
278
y = 2 + foo(...);
279
\end{lstlisting}
280
#+end_latex
281
282
Or multiple times in the same equation:
283
#+begin_latex
284
\begin{lstlisting}[language=lustre]
285
x = foo(2) + (if g then foo(3) else (foo(4) + foo(1)))
286
\end{lstlisting}
287
#+end_latex
288
289
Names could be associated to a subexpression denoting a node instance:
290
291
#+begin_latex
292
\begin{lstlisting}[language=lustre]
293
x = foo(2) + 
294
     (if g then ( (*@ id foo_instance_1 *) foo(3) ) 
295
           else ( foo(4) + foo(1) ) 
296
     )     
297
\end{lstlisting}
298
#+end_latex
299
300
Numerical identifier could also be assigned to specific instances using the "#"
301
key
302
303
#+begin_latex
304
\begin{lstlisting}[language=lustre]
305
x = foo(2) + (if g then ( (*@ # 1 *) foo(3) ) 
306
                   else (( (*@ # 2 *) foo(4) ) + foo(1))
307
             )
308
\end{lstlisting}
309
#+end_latex
310
311
In the expression above and in all the current node, the identifier "foo1" will
312
refer to the instance defined as foo(3) and "foo2" to the instance defined as
313
foo(4).
314
315
316
** Generic Tree based annotations
317
318
Annotations can be defined in function body between the /let/ and the /tel/
319
construct. They can either be associated to the node when placed between
320
flow definitions, ie. equations, or locally to a sub-expression.
321
Similarly to node specification, annotations are defined using single line
322
comments "--@ ...." or multi-lines ones "(*@ .... *)"
323
324
Annotations are defined as pairs key -> value where key denotes a path in a tree
325
of alphanumeric identifiers and value is an extended lustre expression (cf
326
section syntax). The key denotes a path in a hierarchy of identifiers. Values
327
are accumulated through annotation definitions and associated to key paths.
328
329
#+begin_latex
330
\begin{lstlisting}[language=lustre]
331
node node_name (...) returns (...);
332
var ...
333
let
334
--@ /key1/key2/key3/ -> value1
335
eq1 = ...;
336
(*@ /key1/key2/key4/ -> value2
337
    /key5/key6/ -> value3
338
    /key1/key2/key3/ -> value4
339
*)
340
eq2 = ...;
341
342
tel
343
\end{lstlisting}
344
#+end_latex
345
346
In the example above, annotations are not specifically linked to their nearest
347
equation but rather summarized at node level. Together, they define the
348
following tree of values
349
350
#+begin_latex
351
\begin{figure}
352
\begin{tikzpicture}
353
\node (n1) {key1};
354
\node [right of=n1] (n2) {key5};
355
\node [below of=n1] (n3) {key2};
356
\node [right of=n3] (n9) {key6};
357
358
\node [below of=n3,,xshift=-.5cm] (n4) {key3};
359
\node [right of=n4] (n5) {key4};
360
361
362
\node [below of=n4] (n6) {[value1, value4]};
363
\node [right of=n6,xshift=1.2cm] (n7) {[value2]};
364
\node [right of=n7,xshift=.8cm] (n8) {[value3]};
365
366
\path (n1) edge (n3) 
367
      (n3) edge (n4) edge (n5)
368
      (n4) edge (n6) 
369
      (n5) edge (n7) 
370
      (n2) edge (n9) 
371
      (n9) edge (n8);
372
\end{tikzpicture}
373
\end{figure}
374
#+end_latex
375
376
Multiple annotations assigning a value to the same key will be gathered. 
377
The value is extended lustre expression as introduced in Section syntax. It can
378
range from the simpliest string value, eg. the pair color -> "blue" to complex
379
tuples of extended lustre expressions.
380
381
** Default keys
382
383
Key are not pre-specified and can be associated to each Lustre tool feature.
384
However the keywords /invariant/ and /observers/ should be used to define proof objectives or
385
rely on existing expected properties. They act as the /ensures/ contract of
386
node specifications but allow to access local flows and internal ones.
387
388
* Advanced features
389
390
** Addressing internal flows
391
392
Internal flows are usually innaccessible in Lustre. However in order to ease
393
some annotation definition, the value of all local flow of a node instance are
394
available through named paths.
395
396
Let us consider a node foo with a local variable x, and the following expression
397
#+begin_latex
398
\begin{lstlisting}[language=lustre]
399
z = 3 + ( (*@ # 5 *) foo(4) )
400
\end{lstlisting}
401
#+end_latex
402
403
Then the variable x of this specific instance of the node foo could be accessed
404
through the identifier expression foo5.x
405
406
Recursively, if the node foo relies on an instance of node bar, identified as
407
"bar3", the local variable y of the instance bar3 of the node bar used in the
408
instance foo5 of node foo could be accessed through the expression:
409
410
#+begin_latex
411
\begin{lstlisting}[language=lustre]
412
foo5.bar3.y
413
\end{lstlisting}
414
#+end_latex
415
416
Either numerical identifiers of node instances bound with '#' or names defined
417
with the 'id' key - again only for node instances - could be used to describe
418
such internal flows.
419
420
421
Example 1
422
423
Example 2
424
425
426
427
428
429
* Grammar