Diff of /trunk/semantics/semantics

Parent Directory | Revision Log | Patch

	revision 489, Wed Jan 19 17:13:29 2011 UTC	revision 490, Wed Jan 19 19:49:01 2011 UTC
#	Line 25	Line 25
25	c ::=   x := e                           for x = variable, e ∈ Aexp	c ::=   x := e                           for x = variable, e ∈ Aexp
26	| c1; c2                               for c1,c2  ∈ Comm	| c1; c2                               for c1,c2  ∈ Comm
27	| if b then c1 else c2 for c1,c2  ∈ Comm and b  ∈ Rexp	| if b then c1 else c2 for c1,c2  ∈ Comm and b  ∈ Rexp
28		| stabalize
29
30
31	Values	Values
32	v := Num(n) | Bool(b) | String(s) | tensor...??	v := Num(n) | Bool(b) | String(s) | tensor...??
33
34
35	Strand_Status := Active | Dead | Stablized	Strand_Status := Active | Dead | Stablized
36
37	env = variable → value	env = variable → value
38		Σ = id -> Strand_Env
39	Strand_Env = Strand_Status * id * commands * env	Strand_Env = Strand_Status * id * commands * env
40		expr_value = Aexpr * env -> value
41		rel_op = Rexpr * env -> value
42
43
44		comm_eval: status * commands * env -> status * env
45		Rules
46
47		(1)  ------------------------------------------------------
48		comm_eval(status,Stablized,env) ⇓ (Stablized,env)
49
50		expr_eval(e,env) ⇓ v
51		(2) ----------------------------------------------------------
52		comm_eval(status,x:=e,env) ⇓ (status,env[x:=v])
53
54		comm_eval(s,c1,env) ⇓ (s',env')   comm_eval(s',c2,env') ⇓ (s'',env'')
55		(3) -------------------------------------------------------------------------
56		comm_eval(s,c1;c2,env) ⇓ (s'',env'')
57
58
59	Update: Strand_Env -> Strand_Env	rel_op(b,env) ⇓ true   comm_eval(s,c1,env) ⇓ (s',env')
60		(4) -------------------------------------------------------------------------
61		comm_eval(s,if b then c1 else c2,env) ⇓ (s',env')
62
63	Rules:	rel_op(b,env) ⇓ false   comm_eval(s,c2,env) ⇓ (s',env')
64		(5) -------------------------------------------------------------------------
65		comm_eval(s,if b then c1 else c2,env) ⇓ (s',env')
66
67		update: Strand_Env -> Strand_Env
68		Rules
69	(1) -------------------------------------------------------------	(1) -------------------------------------------------------------
70	Update(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env>	update(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env>
71
72
73	(2)     (Doubt this will ever happen...?)	(2)     (Doubt this will ever happen...?)
74	-------------------------------------------------------------	-------------------------------------------------------------
75	Update(<Dead,id,comm,env>) ⇓ <Dead,id,comm,env>	Update(<Dead,id,comm,env>) ⇓ <Dead,id,comm,env>
76
77	Update(<Active,_,e,env>) ⇓ v	comm_eval(Comm,env) ⇓ <new_status,env'>
78	(3)  -------------------------------------------------------------	(3)  -------------------------------------------------------------
79	Update(<Active,_,x:=e,env>) ⇓ env[x:=v]	Update(<Active,_,x:=e,env>) ⇓ <new_status,id,comm,env'>
80

---

Colored Diff Long Colored Diff Unidiff Context Diff Side by Side

Legend: Removed from v.489   changed lines   Added in v.490

---

root@smlnj-gforge.cs.uchicago.edu	ViewVC Help
Powered by ViewVC 1.0.0