A refinement-based compiler development for synchronous languages | Zendy

Jean-Paul Bodeveix | Zendy; Mamoun Filali-Amine | Zendy; Shuanglong Kan | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A refinement-based compiler development for synchronous languages

Author(s) -

Jean-Paul Bodeveix,

Mamoun Filali-Amine,

Shuanglong Kan

Publication year - 2017

Publication title -

hal (le centre pour la communication scientifique directe)

Language(s) - English

Resource type - Conference proceedings

DOI - 10.1145/3127041.3127056

Subject(s) - computer science , programming language , compiler , semantics (computer science) , code generation , event (particle physics) , formal semantics (linguistics) , code (set theory) , formal methods , theoretical computer science , operating system , physics , set (abstract data type) , quantum mechanics , key (lock)

In this paper, we are concerned by the elaboration of generic development steps for the code generation for synchronous languages. Our aim is to provide a correct by construction solution. For that purpose, we adopt a refinement-based approach where proof obligations for each step guarantee properties preservation. We use the Event-B formal method. We start with a big step semantics specified by an Event-B machine. Through a sequence of refinements, expressed as Event-B refinement machines, we end up with a code generation step which implements a small step semantics preserving the properties of the big step semantics.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research