Diff of /trunk/semantics/semantics

Parent Directory | Revision Log | Patch

	revision 491, Wed Jan 26 15:31:09 2011 UTC	revision 492, Wed Jan 26 17:42:05 2011 UTC
#	Line 5	Line 5
5	id ::= integer	id ::= integer
6
7	Arithmetic expression (Aexp)	Arithmetic expression (Aexp)
8	e ::=  n       for n ∈ R or n ∈ Z	e ::=  n       for n ∈ R
9	| x       for x = variable	| x       for x = variable
10	| e1 + e2 for e1,e2 ∈ Aexp, Aexp	| e1 + e2 for e1,e2 ∈ Aexp, Aexp
11	| e1 - e2 for e1,e2 ∈ Aexp, Aexp	| e1 - e2 for e1,e2 ∈ Aexp, Aexp
#	Line 32	Line 32
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 * env | Dead * env | Stablized * env
36	env = variable → value	env = variable → value
37	Σ = id -> Strand_Env
38		/** Global Environment Functions **/
39	Strand_Env = Strand_Status * id * commands * env	Strand_Env = Strand_Status * id * commands * env
40		Γ = id -> Strand_Env  dom(Γ) = all Active & Stablized Strand Environments
41		newId = Γ * id -> id
42
43		/** Arithmetic & Relational Expressions Evaluation Functions**/
44	expr_value = Aexpr * env -> value	expr_value = Aexpr * env -> value
45	rel_op = Rexpr * env -> value	rel_op = Rexpr * env -> value
46
47
48	comm_eval: status * commands * env -> status * env	comm_eval: Strand_Status * commands  -> status * env
	Rules
49
50		Rules
51	(1)  ------------------------------------------------------	(1)  ------------------------------------------------------
52	comm_eval(status,Stablized,env) ⇓ (Stablized,env)	comm_eval((s, env),stabalize) ⇓ (Stablized, env)
53
54
55		(2)  ------------------------------------------------------
56		comm_eval((s, env),die) ⇓ (Dead, env)
57
58
59	expr_eval(e,env) ⇓ v	expr_eval(e,env) ⇓ v
60	(2) ----------------------------------------------------------	(3) ----------------------------------------------------------
61	comm_eval(status,x:=e,env) ⇓ (status,env[x:=v])	comm_eval((s,env),x:=e) ⇓ (s,env[x:=v])
62
	comm_eval(s,c1,env) ⇓ (s',env')   comm_eval(s',c2,env') ⇓ (s'',env'')
	(3) -------------------------------------------------------------------------
	comm_eval(s,c1;c2,env) ⇓ (s'',env'')
63
64		comm_eval((s, env),c1) ⇓ (s', env')   comm_eval((s', env),c2) ⇓ (s'',env'')
65		(4) ---------------------------------------------------------------------------------------
66		comm_eval((s, env),c1;c2) ⇓ (s', env'')
67
	rel_op(b,env) ⇓ true   comm_eval(s,c1,env) ⇓ (s',env')
	(4) -------------------------------------------------------------------------
	comm_eval(s,if b then c1 else c2,env) ⇓ (s',env')
68
69	rel_op(b,env) ⇓ false   comm_eval(s,c2,env) ⇓ (s',env')	rel_op(b, env) ⇓ true   comm_eval((s, env),c1) ⇓ (s',env')
70	(5) -------------------------------------------------------------------------	(5) -------------------------------------------------------------------------
71	comm_eval(s,if b then c1 else c2,env) ⇓ (s',env')	comm_eval((s, env),if b then c1 else c2) ⇓ (s', env')
72
73
74		rel_op(b,env) ⇓ false   comm_eval((s,env),c2) ⇓ (s', env')
75		(6) -------------------------------------------------------------------------
76		comm_eval((s, env),if b then c1 else c2) ⇓ (s', env')
77
78
79
80	update: Strand_Env -> Strand_Env	update: Strand_Env -> Strand_Env
81	Rules	Rules
	(1) -------------------------------------------------------------
	update(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env>
82
83		(1) -------------------------------------------------------------
84		update(((Stabalized,env),id,comm>)) ⇓ ((Stabalized,env),id,comm)
85
	(2)     (Doubt this will ever happen...?)
	-------------------------------------------------------------
	Update(<Dead,id,comm,env>) ⇓ <Dead,id,comm,env>
86
87	comm_eval(Comm,env) ⇓ <new_status,env'>	comm_eval((Active,env),comm) ⇓ (new_status,env')
88	(3)  -------------------------------------------------------------	(2)  -------------------------------------------------------------
89	Update(<Active,_,x:=e,env>) ⇓ <new_status,id,comm,env'>	Update(((Active,env),_,comm>)) ⇓ ((new_status,env'),id,comm)
90

---

Colored Diff Long Colored Diff Unidiff Context Diff Side by Side

Legend: Removed from v.491   changed lines   Added in v.492

---

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