<S, t> et <S', t'> sont bisimilaires par la relation R appartenant à S x S' ssi :
R(s1, s1') et t(s1, s2) => il existe s2' : R(s2, s2') et t'(s1', s2')
et R(s1, s1') et t'(s1', s2') => il existe s2 : R(s2, s2') et t(s1, s2)
<S, t> et <S', t'> sont bisimilaires par la relation R
alors <S, (t)*> et <S', (t')*> sont bisimilaires par la relation R
| s1 | s1' | s2 | s2' |
| <n, m> | <N[n], e, m> | <N[n], m> = <i, m> | <e, i, m> = <e, N[n], m> |
| <v, m> | <v, e, m> | <m(v), m> | <e, m(v), m> |
| <?, m> | <?, e, m> | <i, m> | <e, i, m> |
| <W - p2, m> | <C[p2] . -, W, m> | <W, m> | <e, W, m> |
| <i - W, m> | <-, W . i, m> | <W, m> | <e, W, m> |
| <i - j, m> | <-, j . i, m> | <i-j, m> | <e, i-j, m> |
| <e1, m> | <C1, s, m> | <e1', m'> | <C1', s', m'> |
| <e1 - p2, m> | <C1 . C[p2] . -, s, m> | <e1' - p2, m'> | <C1' . C[p2] .-, s', m'> |
| <e2, m> | <C2, s, m> | <e2', m'> | <C2', s', m'> |
| <i - e2, m> | <C2 . -, s . i, m> | <i - e2', m'> | <C2' . -, s' . i, m'> |
| <v := W, m> | <:=v, W, m> | <W, m> | <e, W, m> |
| <v := i, m> | <:=v, i, m> | <i, m[v := i]> | <e, i, m[v := i]> |
| <e, m> | <C, s, m> | <e', m'> | <C', s', m'> |
| <v := e, m> | <C . :=v, s, m> | <v := e', m'> | <C' . :=v, s', m'> |
| <if W then p2 else p3, m> | <(if C[p2] C[p3]), W, m> | <W, m> | <e, W, m> |
| <if 0 then p2 else p3, m> | <(if C[p2] C[p3]), 0, m> | <p2, m> | <C[p2], e, m> |
| <if i then p2 else p3, m> | <(if C[p2] C[p3]), i, m> | <p3, m> | <C[p3], e, m> |
| <e1, m> | <C1, s, m> | <e1', m'> | <C1', s', m'> |
| <if e1 then p2 else p3, m> | <C1 . (if C[p2] C[p3]), s, m> | <if e1' then p2 else p3, m'> | <C1' . (if C[p2] C[p3]), s', m'> |
| <W ; p2, m> | <pop . C[p2], W, m> | <W, m> | <e, W, m> |
| <i ; p2, m> | <pop . C[p2], i, m> | <p2, m> | <C[p2], e, m> |
| <e1, m> | <C1, s, m> | <e1', m'> | <C1', s', m'> |
| <e1 ; p2, m> | <C1 . pop . C[p2], s, m> | <e1' ; p2, m'> | <C1' . pop . C[p2], s', m'> |
| <repeat p1 until p2 , m> | <(repeat C[p1] C[p2]), e, m> | <repetition <p1, p2, rp>, m> | <C[p1] . C[p2] . (until C[p1] C[p2]) , e, m> |
| <e1, m> | <C1, s, m> | <e1', m'> | <C1', s', m'> |
| <repetition <e1, p2, rp>, m> | <C1 . C[p2] . (until C[p1] C[p2]) , s, m> | <repetition <e1', p2, rp>, m'> | <C1' . C[p2] . (until C[p1] C[p2]) , s', m'> |
| <repetition <W, p2, rp>, m> | <C[p2] . (until C[p1] C[p2]) , W , m> | <W, m> | <e, W, m> |
| <e2, m> | <C2, s, m> | <e2', m'> | <C2', s', m'> |
| <repetition <i, e2, rp>, m> | <C2 . (until C[p1] C[p2]) , s . i, m> | <repetition <i, e2', rp>, m'> | <C2' . (until C[p1] C[p2]) , s' . i, m'> |
| <repetition <i, W, rp>, m> | <(until C[p1] C[p2]) , W . i, m> | <W, m> | <e, W, m> |
| <repetition <i, 0, rp>, m> | <(until C[p1] C[p2]) , 0 . i, m> | <i, m> | <e, i, m> |
| <repetition <i, j, rp>, m> | <(until C[p1] C[p2]) , j . i, m> | < repeat p1 until p2, m> | <(repeat C[p1] C[p2]), e, m> |
| Etat initial : <p, m> | Etat initial : <C[p] , e, m> | Etat final : <r, m> | Etat final : <e, r, m> |
rp : repeat p1 until p2
Erreure : W
conditions sur i, j selon les cours 4 et 5