Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / doc / lustre_spec.org @ b38ffff3

History | View | Annotate | Download (12 KB)

1
Lustre annotation/specification language
2
#+AUTHORS: Pierre-Loic Garoche, Rémi Delmas, Temesghen Kahsai
3
#+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