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 


14 
datatype bexp = B bool  Not bexp  And bexp bexp  Less aexp aexp


15 


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


17 
"bval (B bv) _ = bv" 


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 


52 


53 
text{* Examples: *}


54 


55 
definition


56 
"array_sum =


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


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


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


60 


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


62 
definition


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


64 


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


66 


67 
definition


68 
"linked_list_sum =


69 
WHILE Less (N 0) (!(N 0))


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


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


72 


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


74 


75 
definition


76 
"array_init =


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


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


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


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


81 


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


83 


84 
definition


85 
"linked_list_init =


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


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


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


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


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


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


92 


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


94 


95 
end
