equal
deleted
inserted
replaced
18 consts |
18 consts |
19 C :: com => com_den |
19 C :: com => com_den |
20 |
20 |
21 primrec |
21 primrec |
22 C_skip "C(SKIP) = Id" |
22 C_skip "C(SKIP) = Id" |
23 C_assign "C(x := a) = {(s,t). t = s[x:=a(s)]}" |
23 C_assign "C(x :== a) = {(s,t). t = s[x::=a(s)]}" |
24 C_comp "C(c0 ; c1) = C(c1) O C(c0)" |
24 C_comp "C(c0 ; c1) = C(c1) O C(c0)" |
25 C_if "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un |
25 C_if "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un |
26 {(s,t). (s,t) : C(c2) & ~ b(s)}" |
26 {(s,t). (s,t) : C(c2) & ~ b(s)}" |
27 C_while "C(WHILE b DO c) = lfp (Gamma b (C c))" |
27 C_while "C(WHILE b DO c) = lfp (Gamma b (C c))" |
28 |
28 |