What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

CAESAR.ADT : Un Compilateur pour les Types Algébriques du Langage LOTOS

Hubert Garavel and Philippe Turlier

Actes du Colloque Francophone pour l'Ingénierie des Protocoles CFIP'93 (Montréal, Canada), 1993

Abstract:

Cet article présente le compilateur CAESAR.ADT dont le rôle est de traduire en langage C les définitions de types abstraits algébriques présents dans les programmes LOTOS. Grâce à ce compilateur, il est possible d'exécuter une spécification algébrique, ce qui autorise des applications immédiates pour le prototypage et la vérification formelle. La rapidité de la traduction et l'efficacité du code engendré permettent de traiter des programmes de taille significative avec des performances réalistes.

15 pages, in French

PDF

PostScript

Slides of H. Garavel's lecture at CFIP'93

PDF

Slides of H. Garavel's lecture at the COST 247 meeting (Evry, France) September 19-20, 1994

PDF

---

ERRATUM [May 15, 2003]

Wendelin Serwe reported a mistake in one example given on page 13. For the second "reduction in force" rule, the optimized code generated for:

if E₁ then I₁ else if E₂ then I₁ else I₂ should be:

if E₁ or_else E₂ then I₁ else I₂ instead of:

if E₁ and_then E₂ then I₁ else I₂

---