8 inductive |
8 inductive |
9 small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55) |
9 small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55) |
10 where |
10 where |
11 Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" | |
11 Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" | |
12 |
12 |
13 Seq1: "(SKIP;;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
13 Seq1: "(SKIP;;c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" | |
14 Seq2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';;c\<^isub>2,s')" | |
14 Seq2: "(c\<^sub>1,s) \<rightarrow> (c\<^sub>1',s') \<Longrightarrow> (c\<^sub>1;;c\<^sub>2,s) \<rightarrow> (c\<^sub>1';;c\<^sub>2,s')" | |
15 |
15 |
16 IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" | |
16 IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>1,s)" | |
17 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
17 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" | |
18 |
18 |
19 While: "(WHILE b DO c,s) \<rightarrow> |
19 While: "(WHILE b DO c,s) \<rightarrow> |
20 (IF b THEN c;; WHILE b DO c ELSE SKIP,s)" |
20 (IF b THEN c;; WHILE b DO c ELSE SKIP,s)" |
21 text_raw{*}%endsnip*} |
21 text_raw{*}%endsnip*} |
22 |
22 |