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.