## 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 |