Home My Page Projects Code Snippets Project Openings diderot

# SCM Repository

[diderot] Diff of /trunk/semantics/semantics
 [diderot] / trunk / semantics / semantics

# Diff of /trunk/semantics/semantics

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...?)
-------------------------------------------------------------