7 datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp |
7 datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp |
8 |
8 |
9 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where |
9 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where |
10 "aval (N n) s = n" | |
10 "aval (N n) s = n" | |
11 "aval (!a) s = s(aval a s)" | |
11 "aval (!a) s = s(aval a s)" | |
12 "aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s" |
12 "aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" |
13 |
13 |
14 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp |
14 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp |
15 |
15 |
16 primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
16 primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
17 "bval (Bc v) _ = v" | |
17 "bval (Bc v) _ = v" | |
18 "bval (Not b) s = (\<not> bval b s)" | |
18 "bval (Not b) s = (\<not> bval b s)" | |
19 "bval (And b\<^isub>1 b\<^isub>2) s = (if bval b\<^isub>1 s then bval b\<^isub>2 s else False)" | |
19 "bval (And b\<^sub>1 b\<^sub>2) s = (if bval b\<^sub>1 s then bval b\<^sub>2 s else False)" | |
20 "bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)" |
20 "bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)" |
21 |
21 |
22 |
22 |
23 datatype |
23 datatype |
24 com = SKIP |
24 com = SKIP |
25 | Assign aexp aexp ("_ ::= _" [61, 61] 61) |
25 | Assign aexp aexp ("_ ::= _" [61, 61] 61) |
32 big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool" (infix "\<Rightarrow>" 55) |
32 big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool" (infix "\<Rightarrow>" 55) |
33 where |
33 where |
34 Skip: "(SKIP,sn) \<Rightarrow> sn" | |
34 Skip: "(SKIP,sn) \<Rightarrow> sn" | |
35 Assign: "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" | |
35 Assign: "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" | |
36 New: "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)" | |
36 New: "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)" | |
37 Seq: "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2; (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow> |
37 Seq: "\<lbrakk> (c\<^sub>1,sn\<^sub>1) \<Rightarrow> sn\<^sub>2; (c\<^sub>2,sn\<^sub>2) \<Rightarrow> sn\<^sub>3 \<rbrakk> \<Longrightarrow> |
38 (c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3" | |
38 (c\<^sub>1;c\<^sub>2, sn\<^sub>1) \<Rightarrow> sn\<^sub>3" | |
39 |
39 |
40 IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow> |
40 IfTrue: "\<lbrakk> bval b s; (c\<^sub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow> |
41 (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" | |
41 (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s,n) \<Rightarrow> tn" | |
42 IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow> |
42 IfFalse: "\<lbrakk> \<not>bval b s; (c\<^sub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow> |
43 (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" | |
43 (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s,n) \<Rightarrow> tn" | |
44 |
44 |
45 WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)" | |
45 WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)" | |
46 WhileTrue: |
46 WhileTrue: |
47 "\<lbrakk> bval b s\<^isub>1; (c,s\<^isub>1,n) \<Rightarrow> sn\<^isub>2; (WHILE b DO c, sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow> |
47 "\<lbrakk> bval b s\<^sub>1; (c,s\<^sub>1,n) \<Rightarrow> sn\<^sub>2; (WHILE b DO c, sn\<^sub>2) \<Rightarrow> sn\<^sub>3 \<rbrakk> \<Longrightarrow> |
48 (WHILE b DO c, s\<^isub>1,n) \<Rightarrow> sn\<^isub>3" |
48 (WHILE b DO c, s\<^sub>1,n) \<Rightarrow> sn\<^sub>3" |
49 |
49 |
50 code_pred big_step . |
50 code_pred big_step . |
51 |
51 |
52 declare [[values_timeout = 3600]] |
52 declare [[values_timeout = 3600]] |
53 |
53 |