Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / doc / lustre_spec.org @ 7bd3416a

History | View | Annotate | Download (11.9 KB)

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