author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45200  1f1897ac7877 
child 47818  151d137f1095 
permissions  rwrr 
43158  1 
theory C_like imports Main begin 
2 

3 
subsection "A Clike Language" 

4 

5 
type_synonym state = "nat \<Rightarrow> nat" 

6 

7 
datatype aexp = N nat  Deref aexp ("!")  Plus aexp aexp 

8 

9 
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where 

10 
"aval (N n) s = n"  

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" 

13 

45200  14 
datatype bexp = Bc bool  Not bexp  And bexp bexp  Less aexp aexp 
43158  15 

16 
primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where 

45200  17 
"bval (Bc v) _ = v"  
43158  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)"  

20 
"bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)" 

21 

22 

23 
datatype 

24 
com = SKIP 

25 
 Assign aexp aexp ("_ ::= _" [61, 61] 61) 

26 
 New aexp aexp 

27 
 Semi com com ("_;/ _" [60, 61] 60) 

28 
 If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) 

29 
 While bexp com ("(WHILE _/ DO _)" [0, 61] 61) 

30 

31 
inductive 

32 
big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool" (infix "\<Rightarrow>" 55) 

33 
where 

34 
Skip: "(SKIP,sn) \<Rightarrow> sn"  

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)"  

37 
Semi: "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2; (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow> 

38 
(c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3"  

39 

40 
IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow> 

41 
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn"  

42 
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow> 

43 
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn"  

44 

45 
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)"  

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> 

48 
(WHILE b DO c, s\<^isub>1,n) \<Rightarrow> sn\<^isub>3" 

49 

50 
code_pred big_step . 

51 

43738
e40d2eddf2c0
adding a very liberal timeout for values after a test case failed due to the restricted timeout
bulwahn
parents:
43158
diff
changeset

52 
declare [[values_timeout = 3600]] 
43158  53 

54 
text{* Examples: *} 

55 

56 
definition 

57 
"array_sum = 

58 
WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1)) 

59 
DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0))); 

60 
N 0 ::= Plus (!(N 0)) (N 1) )" 

61 

62 
text {* To show the first n variables in a @{typ "nat \<Rightarrow> nat"} state: *} 

63 
definition 

64 
"list t n = map t [0 ..< n]" 

65 

66 
values "{list t n t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}" 

67 

68 
definition 

69 
"linked_list_sum = 

70 
WHILE Less (N 0) (!(N 0)) 

71 
DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0))); 

72 
N 0 ::= !(Plus(!(N 0))(N 1)) )" 

73 

74 
values "{list t n t n. (linked_list_sum, nth[4,0,3,0,7,2],6) \<Rightarrow> (t,n)}" 

75 

76 
definition 

77 
"array_init = 

78 
New (N 0) (!(N 1)); N 2 ::= !(N 0); 

79 
WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1))) 

80 
DO ( !(N 2) ::= !(N 2); 

81 
N 2 ::= Plus (!(N 2)) (N 1) )" 

82 

83 
values "{list t n t n. (array_init, nth[5,2,7],3) \<Rightarrow> (t,n)}" 

84 

85 
definition 

86 
"linked_list_init = 

87 
WHILE Less (!(N 1)) (!(N 0)) 

88 
DO ( New (N 3) (N 2); 

89 
N 1 ::= Plus (!(N 1)) (N 1); 

90 
!(N 3) ::= !(N 1); 

91 
Plus (!(N 3)) (N 1) ::= !(N 2); 

92 
N 2 ::= !(N 3) )" 

93 

94 
values "{list t n t n. (linked_list_init, nth[2,0,0,0],4) \<Rightarrow> (t,n)}" 

95 

96 
end 