lustrec / doc / lustre_spec.org @ b38ffff3
History  View  Annotate  Download (12 KB)
1 
Lustre annotation/specification language 

2 
#+AUTHORS: PierreLoic 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 postconditions 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 subexpression 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 subexpression. 
321 
Similarly to node specification, annotations are defined using single line 
322 
comments "@ ...." or multilines 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 prespecified 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 