Project

General

Profile

Revision 7bd3416a

View differences:

doc/lustre_spec.org
1
Lustre annotation/specification language
2
#+LATEX_HEADER: \usepackage{tikz,listings,stmaryrd,pgfplots,mathrsfs,syntax}
3
#+LATEX_HEADER: \input{lustre_lst}
4

  
5
This document intends to define the bases of a specification language for
6
Lustre. Such specifications' role are threefold:
7
1. Precise the required behavior of a Lustre model, ie. the behavior of Lustre
8
   nodes. Those specifications could then ease the application of tools.
9
2. Enrich the Lustre code itself with non functionnal annotations; for example
10
   parametrization of tools to be applied on the Lustre model, or for
11
   documentation purpose.
12
3. Enable the compilation of the annotation/specification as C code ACSL
13
   annotations.
14

  
15
* Syntax
16

  
17
** Comments
18
All specifications and annotations are expressed within lustre comments starting
19
with the character "@".
20

  
21
#+begin_latex
22
\begin{lstlisting}[language=lustre]
23
--@ line comment
24
(*@ multi line 
25
    block comment
26
*)
27
\end{lstlisting}
28
#+end_latex
29

  
30
** Extended lustre/arithmethic expressions
31

  
32
We introduce here an extended flavour of lustre expressions: lustre expressions extended with quantification over basic datatypes and
33
  string constants.
34

  
35
These expressions will be used to express preconditions and
36
postconditions over nodes input and output flows. Those conditions have to apply
37
on any non nil value of the flow ie. when the flow is defined.
38

  
39
The figure\ref{fig:expr} gives a BNF for such extended expressions 
40

  
41
#+begin_latex
42
\begin{figure}
43
\begin{grammar}
44
<expression> ::= <constant> 
45
\alt <ident>
46
\alt <int> | <float> | <bool> | <string>
47
\alt <unop> <expression>
48
\alt if <expression> then <expression> else <expression>
49
\alt <expression> <binop> <expression>
50
\alt '(' <expression> ( ',' <expression> )*')'
51
\alt <ident> '(' <expression> ( ',' <expression> )* ')'
52
\alt <quantifier> <var decl> ';' <expression> 
53

  
54
<int> ::= ['0'-'9']+
55

  
56
<float> ::= ['0'-'9']+'.'['0'-'9']+
57

  
58
<bool> ::= 'true' | 'false'
59

  
60
<string> ::= '\"' .* '\"' 
61

  
62
<unop> ::= '-' | 'pre' | 'current' | 'not'
63

  
64
<binop> ::= <temporal ops> | <logical ops> | <arithm ops>
65

  
66
<temporal ops> ::= '->' | 'when' 
67

  
68
<logical ops> ::= 'xor' | '=>' | 'or' | 'and' | '=' | '\textless\textgreater' | '\textless' | '\textless =' | '\textgreater' | '\textgreater =' 
69

  
70
<arithm ops> ::= '*' | '/' | 'mod' | 'div' | '+' | '-'
71

  
72
<quantifier> ::= 'forall' | 'exists'
73

  
74
<var decl> ::= 'const'? <ident> (',' <ident>)* ':' <type> ( ';' 'const'? <ident> ':' <type> )*
75

  
76
<type> ::= 'int' | 'bool' | 'float'
77
\end{grammar}
78
\caption{Definition of extended lustre expressions}
79
\label{fig:expr}
80
\end{figure}
81
#+end_latex
82

  
83
*** String constants
84

  
85
String constants are part of the language. A valid expression could then be the
86
tuple
87

  
88
#+begin_latex
89
\begin{lstlisting}[language=lustre]
90
"blue", if x then y + 1 else node1 (x, y, z), 3.2 + z
91
\end{lstlisting}
92
#+end_latex
93

  
94
Those new string constants will be used to define parameters within annotations.
95

  
96
*** Quantifications
97

  
98
Lustre expression are lift to first order. The syntax to declare quantified
99
variables follow the variable declaration in node inputs and outputs:
100

  
101
#+begin_latex
102
\begin{lstlisting}[language=lustre]
103
ident: type
104
\end{lstlisting}
105
#+end_latex
106

  
107
The keywork const express the additional constraint: 
108
#+begin_latex
109
\begin{lstlisting}[language=lustre]
110
ident = pre ident
111
\end{lstlisting}
112
#+end_latex
113

  
114
Quantified variables denote typed flows.
115

  
116

  
117
** Annotation identifiers
118

  
119
Annotation identifiers are usual alphanumeric identifiers extended with '.'.
120

  
121
** Key paths in annotation bindings
122

  
123
Keys in annotation declaration are either simple identifier or sequence of them
124
separated by "/":
125

  
126
/key/(key/)+ or key
127

  
128
* Node specification
129

  
130
Node specification are inspired from ACSL function contracts. A node will be
131
associated to a set of requirements and expected properties on the resulting
132
flows. 
133

  
134
Scope: inputs, outputs
135

  
136
** Basic contracts
137
Requirements are expressed on input flows using the keyword /requires/
138
while expected behavior can either be defined
139
- with a first order boolean expression over the input flows and the output flows using the
140
  keyword /ensures/ or
141
- with a synchronous observer specified in a separate lustre node, using the
142
  keyword /observer/.
143

  
144
Synchronous observers allow more complex behavior specification since they
145
usually encode a safety property (or bounded liveness) composed with the system
146
state machine. For example, the use of observers allow to declare new variables
147
to express the property.
148

  
149
** Synchronous observers
150

  
151
The node associated to the keywork /observer/ should only produce boolean
152
output flows. The specification /oberver observer\_node(...)/ should be
153
interpreted as
154
\(
155
\bigwedge_{1 \leq i \leq n} o_i
156
\)
157
where /observer\_node/ is defined as 
158
\[
159
observer\_node (...) \ returns\ (o_1, .., o_n); 
160
\]
161

  
162
** Multiple definitions
163
Multiple definitions of /requires/ or /ensures/ / /observer/ are interpreted as
164
syntactic sugar for conjunctions.
165
Eg, the following function specification 
166
#+begin_latex
167
\begin{lstlisting}[language=lustre]
168
--@ requires e1(...);
169
--@ requires e2(...);
170
--@ ensures e3(...);
171
--@ ensures e4(...);
172
node node1 (...) returns (...);
173
\end{lstlisting}
174
#+end_latex
175
 is equivalent to
176
#+begin_latex
177
\begin{lstlisting}[language=lustre]
178
--@ requires e1(...) and e2(...);
179
--@ ensures e3(...) and e4(...);
180
node node1 (...) returns (...);
181
\end{lstlisting}
182
#+end_latex
183

  
184
** Clocks
185
 Those pre- and post-conditions are only defined for the node
186
clock.  Those conditions have to apply on any non nil value of the flow ie. when
187
the flow is defined.
188

  
189
TODO: give an example using when/current
190

  
191
** Extension: Behaviors
192

  
193
Similarly to ACSL function contracts, the node specifications could be defined
194
with sub behaviors. 
195

  
196
TODO: expliquer context du assumes
197

  
198
TODO: concrete example with forall
199
 
200
#+begin_latex
201
\begin{figure}
202
\begin{lstlisting}[language=lustre]
203
--@ requires lustre_expression(i1, ..., in);
204
--@ ensures lustre_expression(i1, ..., in,o1, .., om);
205
--@ behavior b_name1:
206
--@   assumes lustre_expression(i1, ..., in);
207
--@   ensures lustre_expression(i1, ..., in,o1, .., om);
208
--@ behavior b_name2:
209
--@   assumes lustre_expression(i1, ..., in);
210
--@   ensures lustre_expression(i1, ..., in,o1, .., om);
211
node lustre_node_name (i1: t_i1, ..., in: tn) 
212
     returns (o1: t1, ..., om: t_o m));
213
let
214
...
215
tel
216

  
217
--@ requires lustre_expression(i1, ..., in);
218
--@ observer lustre_node(i1, ..., in, o1, .., om);
219
--@ behavior b_name1:
220
--@   assumes lustre_expression(i1, ..., in);
221
--@   observer lustre_node(i1, ..., in,o1, .., om);
222
--@ behavior b_name2:
223
--@   assumes lustre_expression(i1, ..., in);
224
--@   observer lustre_node(i1, ..., in,o1, .., om);
225
node lustre_node_name (i1: t_i1, ..., in: tn) 
226
     returns (o1: t1, ..., om: t_o m));
227
let
228
...
229
tel
230
\end{lstlisting}
231
\end{figure}
232
#+end_latex
233

  
234
** Grammar
235

  
236
TODO
237

  
238
* Local node annotations
239

  
240
Annotations could denote functionnal properties such as invariants or non
241
functional ones, eg. heuristics, tool specific parameters ...
242

  
243
Scope: inputs, outputs, local variables, locally defined variables, internal
244
flows.
245

  
246
** Assigning names to subexpression
247

  
248
Annotations could be used within expression to allocate a new
249
identifier to a sub-expression using the keyword /id/.
250

  
251
For example, in the equation defining $z$:
252

  
253
#+begin_latex
254
\begin{lstlisting}[language=lustre]
255
z = pre y and b and ((*@ id -> subexpr1 *)c or x >= y)
256
\end{lstlisting}
257
#+end_latex
258

  
259
This new identifier /subexpr1/ will be associated to the data flow expression (c
260
or x >= y) and could be used within other annotations.
261

  
262
One can also use single annotations
263
#+begin_latex
264
\begin{lstlisting}[language=lustre]
265
z = pre y and b and ( --@ id -> subexpr1
266
      c or x >= y)
267
\end{lstlisting}
268
#+end_latex
269

  
270
** Assigning identifiers to node instances
271

  
272
A node /foo/ can be used multiple times in a given node. It can appear in
273
different equations:
274
#+begin_latex
275
\begin{lstlisting}[language=lustre]
276
x = foo(...);
277
y = 2 + foo(...);
278
\end{lstlisting}
279
#+end_latex
280

  
281
Or multiple times in the same equation:
282
#+begin_latex
283
\begin{lstlisting}[language=lustre]
284
x = foo(2) + (if g then foo(3) else (foo(4) + foo(1)))
285
\end{lstlisting}
286
#+end_latex
287

  
288
Names could be associated to a subexpression denoting a node instance:
289

  
290
#+begin_latex
291
\begin{lstlisting}[language=lustre]
292
x = foo(2) + 
293
     (if g then ( (*@ id foo_instance_1 *) foo(3) ) 
294
           else ( foo(4) + foo(1) ) 
295
     )     
296
\end{lstlisting}
297
#+end_latex
298

  
299
Numerical identifier could also be assigned to specific instances using the "#"
300
key
301

  
302
#+begin_latex
303
\begin{lstlisting}[language=lustre]
304
x = foo(2) + (if g then ( (*@ # 1 *) foo(3) ) 
305
                   else (( (*@ # 2 *) foo(4) ) + foo(1))
306
             )
307
\end{lstlisting}
308
#+end_latex
309

  
310
In the expression above and in all the current node, the identifier "foo1" will
311
refer to the instance defined as foo(3) and "foo2" to the instance defined as
312
foo(4).
313

  
314

  
315
** Generic Tree based annotations
316

  
317
Annotations can be defined in function body between the /let/ and the /tel/
318
construct. They can either be associated to the node when placed between
319
flow definitions, ie. equations, or locally to a sub-expression.
320
Similarly to node specification, annotations are defined using single line
321
comments "--@ ...." or multi-lines ones "(*@ .... *)"
322

  
323
Annotations are defined as pairs key -> value where key denotes a path in a tree
324
of alphanumeric identifiers and value is an extended lustre expression (cf
325
section syntax). The key denotes a path in a hierarchy of identifiers. Values
326
are accumulated through annotation definitions and associated to key paths.
327

  
328
#+begin_latex
329
\begin{lstlisting}[language=lustre]
330
node node_name (...) returns (...);
331
var ...
332
let
333
--@ /key1/key2/key3/ -> value1
334
eq1 = ...;
335
(*@ /key1/key2/key4/ -> value2
336
    /key5/key6/ -> value3
337
    /key1/key2/key3/ -> value4
338
*)
339
eq2 = ...;
340

  
341
tel
342
\end{lstlisting}
343
#+end_latex
344

  
345
In the example above, annotations are not specifically linked to their nearest
346
equation but rather summarized at node level. Together, they define the
347
following tree of values
348

  
349
#+begin_latex
350
\begin{figure}
351
\begin{tikzpicture}
352
\node (n1) {key1};
353
\node [right of=n1] (n2) {key5};
354
\node [below of=n1] (n3) {key2};
355
\node [right of=n3] (n9) {key6};
356

  
357
\node [below of=n3,,xshift=-.5cm] (n4) {key3};
358
\node [right of=n4] (n5) {key4};
359

  
360

  
361
\node [below of=n4] (n6) {[value1, value4]};
362
\node [right of=n6,xshift=1.2cm] (n7) {[value2]};
363
\node [right of=n7,xshift=.8cm] (n8) {[value3]};
364

  
365
\path (n1) edge (n3) 
366
      (n3) edge (n4) edge (n5)
367
      (n4) edge (n6) 
368
      (n5) edge (n7) 
369
      (n2) edge (n9) 
370
      (n9) edge (n8);
371
\end{tikzpicture}
372
\end{figure}
373
#+end_latex
374

  
375
Multiple annotations assigning a value to the same key will be gathered. 
376
The value is extended lustre expression as introduced in Section syntax. It can
377
range from the simpliest string value, eg. the pair color -> "blue" to complex
378
tuples of extended lustre expressions.
379

  
380
** Default keys
381

  
382
Key are not pre-specified and can be associated to each Lustre tool feature.
383
However the keywords /invariant/ and /observers/ should be used to define proof objectives or
384
rely on existing expected properties. They act as the /ensures/ contract of
385
node specifications but allow to access local flows and internal ones.
386

  
387
* Advanced features
388

  
389
** Addressing internal flows
390

  
391
Internal flows are usually innaccessible in Lustre. However in order to ease
392
some annotation definition, the value of all local flow of a node instance are
393
available through named paths.
394

  
395
Let us consider a node foo with a local variable x, and the following expression
396
#+begin_latex
397
\begin{lstlisting}[language=lustre]
398
z = 3 + ( (*@ # 5 *) foo(4) )
399
\end{lstlisting}
400
#+end_latex
401

  
402
Then the variable x of this specific instance of the node foo could be accessed
403
through the identifier expression foo5.x
404

  
405
Recursively, if the node foo relies on an instance of node bar, identified as
406
"bar3", the local variable y of the instance bar3 of the node bar used in the
407
instance foo5 of node foo could be accessed through the expression:
408

  
409
#+begin_latex
410
\begin{lstlisting}[language=lustre]
411
foo5.bar3.y
412
\end{lstlisting}
413
#+end_latex
414

  
415
Either numerical identifiers of node instances bound with '#' or names defined
416
with the 'id' key - again only for node instances - could be used to describe
417
such internal flows.
418

  
419

  
420
Example 1
421

  
422
Example 2
423

  
424

  
425

  
426

  
427

  
428
* Grammar

Also available in: Unified diff