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
