equal
deleted
inserted
replaced
31 |
31 |
32 Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t" |
32 Proc: "(p,cp)#pe \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow> pe \<turnstile> ({PROC p = cp;; c}, s) \<Rightarrow> t" |
33 |
33 |
34 code_pred big_step . |
34 code_pred big_step . |
35 |
35 |
|
36 values "{map t [''x'', ''y'', ''z''] |t. |
|
37 [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}" |
36 |
38 |
37 (* FIXME: example state syntax *) |
39 values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}" |
38 values "{map t [''x'', ''y'', ''z''] |t. |
|
39 [] \<turnstile> (CALL ''p'', (%_. 0)(''x'' := 42, ''y'' := 43)) \<Rightarrow> t}" |
|
40 |
|
41 values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, (%_. 0) ) \<Rightarrow> t}" |
|
42 |
40 |
43 end |
41 end |