Personnes présentes
- Hai Nguyen Van
- Chantal Keller
- Frédéric Boulanger
- Safouan Taha
- Benoît Valiron
- Burkhart Wolff
- Lina Ye
Liste de choses intéressantes
- LTL
- CSP
- Eisbar
- Proc Models
- UTP (Unified Programming Techniques)
- Simulink
- Implémentation de Hai
- TESL comme langage glu: LTL, CSP, UTP, ...
Présentation de ce qu'est UTP
Burkhart Wolff
- Shallow language
- Deal with the notion of variable in a consistent manner
- Variables are defined incrementally
Originally described in a book by T. Hoare: "Theory of Unified Program".
Bu's slogan: "denotational semantics toolkit"
An alphabet of variables, with a syntactic theory built on top.
- concept design : start / ok
- reactive design : start / ok / enabled
with a trace semantics
lense
An algebraic structure (a Galois connection):
get : U -> alpha put : U -> alpha -> U
One does not speak about variables anymore, but about lenses: a variable is a lense in the sense that one can manipulate some of its properties (the one that are currently under scrutiny), but it might have more properties hidden as of yet.
Use
Universe with "holes":
- Prove some properties for a "rough" universe seen through a lense
- Refine later on by going on the other side of the lense
UTP in Isabelle
Done by Bu
Uses extensible records
design = record start ok :: bool end reactive_design = design + record enabled ... end
Status of Hai's implementation
Hai
Gave a demo of his Isabelle implementation in SML.