Chandelle ─ A Mini─Lustre to WhyML Compiler

Chandelle aims to translate core Lustre programs with assertions to WhyML code with appropriate contracts, allowing users to make use of the Why3 platform to prove properties on their Lustre programs.

Structure

Chandelle is decomposed into multiple analyses, most of them classical ones. The main addition here is the generation of function contracts from the set of assertions of each node.

               [Lustre]
                  │
            ┌─────┴─────┐            ┌───────────┐
            │ Parse AST ├──(Typing)──┤ Typed AST │
            └───────────┘            └─────┬─────┘
                                           │
                                       (Clocking)
                                           │
                                     ┌─────┴───────┐
                                     │ Clocked AST │
                                     └─────┬───────┘
                                           │
                                      (Contracts)
┌─(Initialization)─┐                       │
│   ┌──────────────┴─┐                   ┌─┴────────────┐
└───┤ Normalized AST ├──(Normalization)──┤ Contract AST │
    └────────┬───────┘                   └──────────────┘
             │
        (Causality)
             │
       ┌─────┴──────────┐             ┌───────────┐
       │ Sequential AST ├──(Codegen)──┤ WhyML AST │
       └────────────────┘             └─────┬─────┘
                                            │
                                         [WhyML]