msem : code -> mem -> mem distr dsem : code -> mem distr -> mem distr munit : 'a -> 'a distr. axiom munit_def : $[f | munit a] = f a. mlet : 'a distr -> ('a -> 'b distr) -> 'b distr. axiom mlet_def : $[f | mlet d F] = $[fun a => $[f | F a] | d] dsem c mu = mlet mu (mem c) msem c m = dsem (munit a) [ P ] c {phi} {$[1_P] = 1%r} c {phi} (* -------------------------------------------------------------- *) muf (fun x => b2r (! f)) d = 0 --> $@[x: f | mu] si x : memory alors active_mem x si mu : active_distr alors --> $@[x: f] muf (fun x => f) d = 0 --> $[x: f | mu] si x : memory alors active_mem x si mu : active_distr alors --> $[x: f] il faudrait avoir des variables de range comme ca on peut faire ce que l'on veut. Il y a les memoires globales memoire = memoire global + record type upd { var -> form glob -> form } upd_mem : form -> upd -> form |- m : memory mt ||- upd : mt --------------------------------- |- upd_mem m upd : memory mt get_mem : form -> pvar -> form |- m : memory mt mt |- x : t ------------------------------ |- get_mem m x : t Remarque on a besoin de faire deux type de substitution de variables: Remplacement d'une variable: m[x := f] pour le wp et random, Regles de simplification: m[x := f][x] --> f m[x := f][y] --> m[y] if x <> y m[x := f][glob A] --> m[glob A] if disjoint glob A x. m[x := f][y:=f'] --> m[y:= f'][x:= f] if x <> y m[x := f][x:=f'] --> m[x:=f'] Remplacement d'un ensemble de variables par variables universellement quantifiees: m [x1,....,xn, glob A1, glob An ::= m'] Regles de simplification: m[vars ::= m'][x] --> m'[x] if x in vars m[vars ::= m'][x] --> m[x] if x not in vars m[vars ::= m'][glob A] --> m'[glob A] if glob A included in vars m[vars ::= m'][glob A] --> m[glob A] if glob A disjoint vars m[vars ::= m'][glob A] --> m[vars' := m'][glob A] where vars' { x(resp glob B) in vars | not glob A disjoint x(resp glob) } Explanation on x in vars = x1, ..., xn, glob A1, ... glob An - x in xi then x in vars - x not in xi and x not in glob Ai then x not in vars - glob A included in vars if A in Ai - glob A disjoint vars if A can not read/write xi and glob Ai On peut exprimer qu'une formule est invariante par upd forall (g:glob A) (m: mt mem), P m => P (m[glob A <- g]) Idem pour les relations: forall (g:glob A) (m1: mt1 mem) (m2:mt2 mem), R m1 m2 => R (m1[glob A <- g]) (m2[glob A <- g]) Regle de reduction: x{m[x<-t; other]} -> t si other disjoint x x{m[upd]} -> x{m[remove x upd]} remove x upd = upd [glob A clone with theory T1 <- T2 with module M1 <- M2 with lemma l1 <- l2 rename regexp by regexp clone include T1 as T2 pour faciliter les clones futurs. rename : renomage des lemmes, operateurs, types, modules, variables globales, variables locales. c'est quoi : { 'a support | wf_support<:'a> }